Inductive family of types
(Higher inductive types・・・と言いたいがそれはまた別物らしい。)
Family of inductive types
たとえば、Free monad - PS:
は、 をfixed pointとするinitial algebraが族になっているだけ(で問題ない)。
Inductive family of types
一方、free applicativeになると、
となっており困ってしまったが、これはendofunctorをobjectと考えて
なるinitial algebraと考えればいいだけらしい。つまり、fixed pointは となる。
実際に、これだけからapplicative functorを作れるのかは分からない。*1
参考文献
*1:primitive recursionではない模様