Proposition comprehension_eso_mor_inv_mor : comprehension_eso_mor · comprehension_eso_inv_mor = identity _. Proof. unfold comprehension_eso_mor, comprehension_eso_inv_mor. rewrite !assoc'. use z_iso_inv_on_right. rewrite id_right. refine (_ @ id_left _). rewrite !assoc. apply maponpaths_2. unfold comprehension_eso_mor_help, comprehension_eso_inv_mor_help. unfold sub_to_extension. use eq_sub_to_extension. - rewrite id_left. rewrite !assoc'. etrans. { do 4 apply maponpaths. exact (PullbackSqrCommutes (comp_cat_pullback comprehension_eso_ty_help comprehension_eso_inv_mor_help_sub)). } etrans. { do 3 apply maponpaths. rewrite !assoc. apply maponpaths_2. apply comp_cat_tm_eq. } rewrite id_left. unfold comprehension_eso_inv_mor_help_sub. refine (_ @ id_right _). use (MorphismsIntoPullbackEqual (isPullback_Pullback HΔ)). + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr1 HΔ). rewrite z_iso_after_z_iso_inv. rewrite id_left, id_right. apply idpath. + rewrite !assoc'. rewrite (PullbackArrow_PullbackPr2 HΔ). rewrite id_left. use (cancel_z_iso _ _ γΓ). rewrite !assoc'. pose (maponpaths (λ z, z · PullbackPr1 HΓ) (!(dfl_ext_identity_eq left_tm right_tm))) as p. cbn -[left_tm right_tm PullbackPr1] in p. rewrite !assoc' in p. rewrite left_tm_pr1, right_tm_pr1 in p. rewrite !assoc' in p. cbn in p. exact p. - apply dfl_eq_subst_equalizer_tm. 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.