proposition: Lemma Comonad'_eq_raw_data (C : category) (T T' : Comonad' C) : pr1 (pr1 T) = pr1 (pr1 T') -> T = T'.
proof: Proof. intro e. apply subtypePath. - intro. now apply isaprop_disp_Comonad_laws. - apply subtypePath. + intro. apply isapropdirprod. * apply isapropdirprod. -- apply (isaprop_is_functor C C), homset_property. -- apply (isaprop_is_nat_trans C C), homset_property. * apply (isaprop_is_nat_trans C C), homset_property. + apply e. 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