Proposition comprehension_eso_inv_mor_mor : comprehension_eso_inv_mor · comprehension_eso_mor = identity _. Proof. unfold comprehension_eso_mor, comprehension_eso_inv_mor. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite z_iso_inv_after_z_iso. apply id_left. } unfold comprehension_eso_mor_help, comprehension_eso_inv_mor_help. unfold sub_to_extension. unfold dfl_ext_identity_sub_tm. simpl. rewrite !assoc'. etrans. { apply maponpaths. etrans. { apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. exact (PullbackSqrCommutes (comp_cat_pullback comprehension_eso_ty_help comprehension_eso_inv_mor_help_sub)). } rewrite !assoc. etrans. { do 3 apply maponpaths_2. unfold comp_cat_comp_mor. apply comprehension_functor_mor_comm. } rewrite id_right. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply comprehension_eso_inv_mor_help_sub_pr1. } rewrite z_iso_inv_after_z_iso. apply id_right. } apply comp_cat_tm_eq. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCatNotations.