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).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.