proposition: Lemma Comonad_eq_raw_data (C : category) (T T' : Comonad C) : Comonad_to_raw_data T = Comonad_to_raw_data T' -> T = T'.
proof: Proof. intro e. apply (invmaponpathsweq (_,, (isweq_iso _ _ (@Comonad_to_Comonad'_to_Comonad C) (@Comonad'_to_Comonad_to_Comonad' C)))). now apply (Comonad'_eq_raw_data C). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Core.Univalence