Definition is_cartesian_precomp {C : category} {D : disp_cat C} {x y z : C} {f : x --> y} {g : y --> z} {h : x --> z} {xx : D x} {yy : D y} {zz : D z} {ff : xx -->[ f ] yy} {gg : yy -->[ g ] zz} {hh : xx -->[ h ] zz} (p : h = f · g) (pp : (ff ;; gg = transportf (λ z, _ -->[ z ] _) p hh)%mor_disp) (Hgg : is_cartesian gg) (Hhh : is_cartesian hh) : is_cartesian ff. Proof. intros w φ ww φφ. use iscontraprop1. - abstract (use invproofirrelevance ; intros ψ₁ ψ₂ ; use subtypePath ; [ intro ; apply D | ] ; use (cartesian_factorisation_unique Hhh) ; rewrite <- (transportb_transpose_left pp) ; unfold transportb ; rewrite !mor_disp_transportf_prewhisker ; rewrite !assoc_disp ; rewrite (pr2 ψ₁), (pr2 ψ₂) ; apply idpath). - simple refine (_ ,, _). + refine (cartesian_factorisation Hhh φ (transportf (λ z, _ -->[ z ] _) _ (φφ ;; gg)%mor_disp)). abstract (rewrite p ; rewrite assoc ; apply idpath). + abstract (simpl ; use (cartesian_factorisation_unique Hgg) ; rewrite assoc_disp_var ; rewrite pp ; rewrite mor_disp_transportf_prewhisker ; rewrite transport_f_f ; rewrite cartesian_factorisation_commutes ; rewrite transport_f_f ; apply transportf_set ; apply homset_property). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite. Section IsoCleavingFromOpcleaving. End IsoCleavingFromOpcleaving.