Definition dfl_ext_identity_sub_tm {Γ Δ : C} (s : Δ --> Γ) {A : ty Γ} {t₁ t₂ : comp_cat_tm Γ A} (p : comp_cat_tm Δ (dfl_ext_identity_type (sub_comp_cat_tm t₁ s) (sub_comp_cat_tm t₂ s))) : comp_cat_tm Δ ((dfl_ext_identity_type t₁ t₂) [[ s ]]). Proof. use make_comp_cat_tm. - exact (p · comp_cat_comp_mor (dfl_ext_identity_sub_mor s t₁ t₂)). - abstract (rewrite !assoc' ; unfold comp_cat_comp_mor ; refine (maponpaths (λ z, _ · z) (comprehension_functor_mor_comm _ _) @ _) ; rewrite id_right ; apply comp_cat_tm_eq). Defined.
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.