Proposition comprehension_functor_mor_factorisation_pr1 {C : comp_cat} {Γ₁ Γ₂ Γ₃ : C} {s₁ : Γ₁ --> Γ₂} {s₂ : Γ₂ --> Γ₃} {A₁ : ty Γ₁} {A₂ : ty Γ₂} {A₃ : ty Γ₃} (t : A₂ -->[ s₂ ] A₃) (Ht : is_cartesian t) (t' : A₁ -->[ s₁ · s₂ ] A₃) : comprehension_functor_mor (comp_cat_comprehension C) (cartesian_factorisation Ht _ t') · PullbackPr1 (cartesian_to_pullback t Ht) = comprehension_functor_mor (comp_cat_comprehension C) t'. Proof. cbn. refine (!(comprehension_functor_mor_comp _ _ _) @ _). apply maponpaths. apply cartesian_factorisation_commutes. Qed.
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.