Definition dfl_ext_identity_sub_mor_mor {Γ Δ : C} (s : Δ --> Γ) {A : ty Γ} (t₁ t₂ : comp_cat_tm Γ A) : (disp_cat_of_types C)[{Δ}] ⟦ dfl_ext_identity_type (sub_comp_cat_tm t₁ s) (sub_comp_cat_tm t₂ s) , fiber_functor_from_cleaving (disp_cat_of_types C) (cleaving_of_types C) s (dfl_full_comp_cat_unit Γ) ⟧. Proof. refine (EqualizerArrow (dfl_ext_identity (sub_comp_cat_tm t₁ s) (sub_comp_cat_tm t₂ s)) · _). use (TerminalArrow (preserves_terminal_to_terminal _ (pr2 (fiberwise_terminal_dfl_full_comp_cat C) _ _ s) _)). 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.