Definition is_cartesian_in_reindex_disp_cat {C₁ C₂ : category} (F : C₁ ⟶ C₂) (D : disp_cat C₂) {x y : C₁} {f : x --> y} {xx : D (F x)} {yy : D (F y)} (ff : xx -->[ #F f ] yy) (Hff : is_cartesian ff) : @is_cartesian _ (reindex_disp_cat F D) y x f yy xx ff. Proof. intros z g zz gg ; cbn in *. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply D | ] ; use (cartesian_factorisation_unique Hff) ; rewrite (transportf_transpose_right (pr2 φ₁)) ; rewrite (transportf_transpose_right (pr2 φ₂)) ; apply idpath). - simple refine (_ ,, _). + refine (cartesian_factorisation Hff (#F g) (transportf (λ z, _ -->[ z ] _) _ gg)). abstract (apply functor_comp). + abstract (cbn ; rewrite cartesian_factorisation_commutes ; unfold transportb ; rewrite transport_f_f ; apply transportf_set ; apply homset_property). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Section IsCartesianFromReindexDispCat. End IsCartesianFromReindexDispCat. Section IsOpCartesianFromReindexDispCat. End IsOpCartesianFromReindexDispCat.