Proposition dfl_ext_identity_sub_mor_eq {Γ Δ : C} (s : Δ --> Γ) {A : ty Γ} (t₁ t₂ : comp_cat_tm Γ A) : dfl_ext_identity_sub_mor_mor s t₁ t₂ · # (fiber_functor_from_cleaving (disp_cat_of_types C) (cleaving_of_types C) s) (dfl_full_comp_cat_tm_to_mor t₁) = dfl_ext_identity_sub_mor_mor s t₁ t₂ · # (fiber_functor_from_cleaving (disp_cat_of_types C) (cleaving_of_types C) s) (dfl_full_comp_cat_tm_to_mor t₂). Proof. unfold dfl_ext_identity_sub_mor_mor. rewrite !assoc'. pose (EqualizerEqAr (dfl_ext_identity (sub_comp_cat_tm t₁ s) (sub_comp_cat_tm t₂ s))) as p. refine (_ @ p @ _) ; apply maponpaths ; clear p. - use (invmaponpathsweq (dfl_full_comp_cat_tm_weq_mor _)). refine (_ @ !(homotweqinvweq (dfl_full_comp_cat_tm_weq_mor _) _)). use eq_comp_cat_tm. cbn. rewrite comprehension_functor_mor_transportf. rewrite comprehension_functor_mor_comp. use (MorphismsIntoPullbackEqual (isPullback_Pullback (cartesian_to_pullback _ _))). + rewrite !assoc'. rewrite comprehension_functor_mor_factorisation_pr1. rewrite comprehension_functor_mor_transportf. rewrite comprehension_functor_mor_comp. rewrite PullbackArrow_PullbackPr1. etrans. { do 3 apply maponpaths. exact (maponpaths pr1 (FF_disp_functor_ff_inv (full_comp_cat_comprehension_fully_faithful C) _)). } cbn. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite comprehension_functor_mor_comm. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. rewrite !assoc'. rewrite comprehension_functor_mor_comm. rewrite id_right. apply z_iso_after_z_iso_inv. + rewrite !assoc'. etrans. { do 2 apply maponpaths. apply comprehension_functor_mor_factorisation_pr2. } rewrite id_right. rewrite comprehension_functor_mor_comm. rewrite id_right. rewrite PullbackArrow_PullbackPr2. apply z_iso_after_z_iso_inv. - use (invmaponpathsweq (dfl_full_comp_cat_tm_weq_mor _)). refine (homotweqinvweq (dfl_full_comp_cat_tm_weq_mor _) _ @ _). use eq_comp_cat_tm. cbn. rewrite comprehension_functor_mor_transportf. rewrite comprehension_functor_mor_comp. use (MorphismsIntoPullbackEqual (isPullback_Pullback (cartesian_to_pullback _ _))). + rewrite !assoc'. rewrite comprehension_functor_mor_factorisation_pr1. rewrite comprehension_functor_mor_transportf. rewrite comprehension_functor_mor_comp. rewrite PullbackArrow_PullbackPr1. refine (!_). etrans. { do 3 apply maponpaths. exact (maponpaths pr1 (FF_disp_functor_ff_inv (full_comp_cat_comprehension_fully_faithful C) _)). } cbn. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite comprehension_functor_mor_comm. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. rewrite !assoc'. rewrite comprehension_functor_mor_comm. rewrite id_right. apply z_iso_after_z_iso_inv. + rewrite !assoc'. refine (!_). etrans. { do 2 apply maponpaths. apply comprehension_functor_mor_factorisation_pr2. } rewrite id_right. rewrite comprehension_functor_mor_comm. rewrite id_right. rewrite PullbackArrow_PullbackPr2. apply z_iso_after_z_iso_inv. 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.Preservation. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. 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.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.CategoryTheory.Monics. 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.