Lemma pointfree_is_equiv: Comonad_laws_pointfree <-> disp_Comonad_laws T. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence.