proposition: Lemma pointfree_is_equiv: Comonad_laws_pointfree <-> disp_Comonad_laws T.
proof: Proof. split. - intro H. induction H as [[H1 H2] H3]. split. + split. * intro c. apply (maponpaths pr1) in H1. apply toforallpaths in H1. apply H1. * intro c. apply (maponpaths pr1) in H2. apply toforallpaths in H2. apply H2. + intro c. apply (maponpaths pr1) in H3. apply toforallpaths in H3. apply H3. - intro H. induction H as [[H1 H2] H3]. split. + split. * apply nat_trans_eq_alt. exact H1. * apply nat_trans_eq_alt. exact H2. + apply nat_trans_eq; try apply homset_property. exact H3. 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