data functorを構成

Coq でやるには型合わせがとてもつらい.とてもバカな定義だができた.

いずれ polynomial functor をもうちょい賢く扱う必要があるな.別に各 polynomial functor の initial algebra の standard な実装を作って仕舞えば良いだけで,具体的な Coq の実データ型とは単に isomorphism をとれば良いだけの話な気がしてきたぞ.つーか,そう考えると「free generate は limit とる操作だから実装めんどい」とか口走った気がするけど,何も面倒なことないのではという気がする.バカですな.

久しぶりに研究の話をした気がする.もうちょい真面目にやったほうがいいっすよマジで.