Definition opcleaving_of_opcleaving_is_opcartesian_2cell {C₁ C₂ : bicat_of_univ_cats} {F₁ F₂ : C₁ --> C₂} {α : F₁ ==> F₂} {D₁ : disp_bicat_of_opcleaving C₁} {D₂ : disp_bicat_of_opcleaving C₂} {FF₁ : D₁ -->[ F₁ ] D₂} {FF₂ : D₁ -->[ F₂ ] D₂} (αα : FF₁ ==>[ α ] FF₂) (Hαα : ∏ (x : (C₁ : univalent_category)) (xx : (pr1 D₁ : disp_univalent_category _) x), is_opcartesian (pr11 αα x xx)) : is_opcartesian_2cell disp_bicat_of_opcleaving αα. Proof. intros G GG β βα. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply disp_cellset_property | ] ; use subtypePath ; [ intro ; apply isapropunit | ] ; use disp_nat_trans_eq ; intros x xx ; assert (p₁ := maponpaths (λ z, (pr11 z) x xx) (pr2 φ₁)) ; assert (p₂ := maponpaths (λ z, (pr11 z) x xx) (pr2 φ₂)) ; cbn in p₁, p₂ ; pose (r := p₁ @ !p₂) ; use (opcartesian_factorisation_unique (Hαα x xx)) ; exact r). - simple refine ((_ ,, tt) ,, _). + exact (opcartesian_factorisation_disp_nat_trans (pr1 αα) (pr1 βα) Hαα). + abstract (use subtypePath ; [ intro ; apply isapropunit | ] ; use subtypePath ; [ intro ; apply isaprop_disp_nat_trans_axioms| ] ; use funextsec ; intro x ; use funextsec ; intro xx ; apply opcartesian_factorisation_commutes). 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.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats.