Proposition dfl_ext_identity_eq {Γ : C} {A : ty Γ} (t₁ t₂ : comp_cat_tm Γ A) : π (dfl_ext_identity_type t₁ t₂) · t₁ = π (dfl_ext_identity_type t₁ t₂) · t₂. Proof. refine (_ @ maponpaths comp_cat_comp_mor (EqualizerEqAr (dfl_ext_identity t₁ t₂)) @ _). - cbn. unfold comp_cat_comp_mor. rewrite comprehension_functor_mor_transportf. rewrite comprehension_functor_mor_comp. refine (!_). etrans. { apply maponpaths. exact (maponpaths pr1 (FF_disp_functor_ff_inv (full_comp_cat_comprehension_fully_faithful C) _)). } cbn. rewrite !assoc. apply maponpaths_2. etrans. { exact (comprehension_functor_mor_comm (comp_cat_comprehension C) _). } apply id_right. - cbn. unfold comp_cat_comp_mor. rewrite comprehension_functor_mor_transportf. rewrite comprehension_functor_mor_comp. etrans. { apply maponpaths. exact (maponpaths pr1 (FF_disp_functor_ff_inv (full_comp_cat_comprehension_fully_faithful C) _)). } cbn. rewrite !assoc. apply maponpaths_2. etrans. { exact (comprehension_functor_mor_comm (comp_cat_comprehension C) _). } apply id_right. 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.