Definition functors_into_cat_nat_iso_is_cartesian_1cell {C₁ C₂ : bicat_of_strict_cats} {F : C₁ --> C₂} {G₁ : disp_bicat_of_functors_into_cat C₁} {G₂ : disp_bicat_of_functors_into_cat C₂} (α : G₁ -->[ F ] G₂) (Hα : is_nat_z_iso (pr1 α)) : cartesian_1cell disp_bicat_of_functors_into_cat α. Proof. split. - intros C₃ G₃ H HF. simple refine (_ ,, _). + exact (nat_trans_comp _ _ _ HF (pre_whisker _ (nat_z_iso_inv (make_nat_z_iso _ _ α Hα)))). + simple refine (_ ,, _). * abstract (intro x ; cbn ; etrans ; [ apply maponpaths ; apply (functor_id G₂) | ] ; refine (id_right (pr1 HF x · _ · _) @ _) ; refine (_ @ id_right _) ; rewrite assoc' ; apply maponpaths ; apply Hα). * apply functors_into_cat_disp_locally_groupoid. - intros C₃ G₃ F₁ F₂ β γ δ p ℓ₁ ℓ₂. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply disp_bicat_of_functors_into_cat | ] ; apply functors_into_cat_disp_2cells_isaprop). + simple refine (_ ,, _). * abstract (intro x ; pose (pr12 ℓ₁ x) as q₁ ; pose (pr12 ℓ₂ x @ !(p x) @ maponpaths (λ z, z · _) (!q₁)) as q₂ ; rewrite !(functor_id G₂) in q₂ ; pose (!(id_right (pr11 ℓ₂ x · pr1 α (pr1 F₂ x))) @ q₂) as q₃ ; pose (q₃ @ maponpaths (λ z, z · # (pr1 G₂) _) (id_right _) @ assoc' _ _ _) as q₄ ; pose (q₄ @ maponpaths (λ z, _ · z) (!(nat_trans_ax α _ _ (pr1 δ x)))) as q₅ ; pose (maponpaths (λ z, z · nat_z_iso_inv (make_nat_z_iso _ _ _ Hα) (pr1 F₂ x)) q₅) as q₆ ; refine (_ @ !q₆ @ _) ; [ refine (_ @ assoc (pr11 ℓ₁ x) _ _) ; apply maponpaths ; refine (_ @ assoc _ _ _) ; refine (!(id_right _) @ _) ; apply maponpaths ; refine (!_) ; apply Hα | refine (assoc' (pr11 ℓ₂ x) _ _ @ _) ; refine (_ @ id_right _) ; apply maponpaths ; apply Hα ]). * apply functors_into_cat_disp_2cells_isaprop. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Examples.StrictCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FunctorsIntoCat.