cocartesian cartesian iso coproducts Coalgebras adjunctions coalgebras Adjunctions Lambek endofunctor pointful Kleisli functoriality formalizations Agda Coq agda-categories setoids sym-assoc setoid-enriched extensionality Setoid Moggi Cockett Bucalo equational coinductive corecursion coinduction coalgebra Capretta monic monicity intensional Fixpoint Elgot exponentials Pre-Elgot pre-Elgot quotiented quotients-as-setoid setoid Setoids Coproducts iff Quotienting bisimilarity corecursively coproduct adjunction counit epi F-coalgebra F-coalgebras F-Coalgebras terminality coinductively monos epis isos Corecursion subobject isomorphisms epicness fixpoint Martin-Löf Set₀ Set₁ bisimilar copatterns epimorphisms monomorphisms expressivity Friedrich-Alexander-Universität Erlangen-Nürnberg Goncharov denotational Plotkin monadic