Open solomon-b opened 1 year ago
The free monad Free p satisfies the inductive formula Free p = y + (p \tri (Free p)) and the cofree comonad Cofree p satisfies the coinductive formula Cofree p = y x (p \tri (Cofree p)). Is this enough to define them in the type theory?
The free monad Free p satisfies the inductive formula Free p = y + (p \tri (Free p)) and the cofree comonad Cofree p satisfies the coinductive formula Cofree p = y x (p \tri (Cofree p)). Is this enough to define them in the type theory?