Proposition comprehension_functor_mor_factorisation_pr2 {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') · π _ = π _ · s₁. Proof. rewrite comprehension_functor_mor_comm. apply idpath. 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.