fact: Definition comp_cat_functor_extension_mor {C₁ C₂ : comp_cat} (F : comp_cat_functor C₁ C₂) {Γ : C₁} {A₁ A₂ : ty Γ} (f : A₁ -->[ identity _ ] A₂) : F Γ & comp_cat_type_functor F Γ A₁ --> F Γ & comp_cat_type_functor F Γ A₂ := comprehension_functor_mor (comp_cat_comprehension C₂) ((♯ (comp_cat_type_functor F) f)%mor_disp).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.Limits.Pullbacks UniMath.Bicategories.ComprehensionCat.BicatOfCompCat