Definition comp_cat_is_pullback {C : comp_cat} {Γ₁ Γ₂ : C} (A : ty Γ₁) (s : Γ₂ --> Γ₁) : @isPullback C _ _ _ _ (π A) s (comprehension_functor_mor (comp_cat_comprehension C) (cleaving_of_types C _ _ s A)) (π (A [[ s ]])) (comprehension_functor_mor_comm (comp_cat_comprehension C) (cleaving_of_types C _ _ s A)) := cartesian_isPullback_in_cod_disp _ (cartesian_disp_functor_on_cartesian (comp_cat_comprehension C) (cleaving_of_types C _ _ s A)).
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.