Lemma ComonadCoalg_disp_is_Coalgebra {C : category} (T : Comonad C) : ComonadCoalg_tot T = ComonadCoalg T. Proof. apply catiso_to_category_path. use tpair. - exact (ComonadCoalg_disp_Coalgebra_functor T). - split. * intros a b. use isweq_iso. + exact (idfun _). + intros. apply idpath. + intros. apply idpath. * use isweq_iso. + intros [[x α] laws]. use tpair. -- exact x. -- exact (α,, laws). + intro. apply idpath. + intro. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.MonadAlgebras. Require Import UniMath.CategoryTheory.Monads.Comonads. Require Import UniMath.CategoryTheory.Monads.ComonadCoalgebras. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.