Definition trivial_lift_2cell {w : B₁} {z : B₂} {h h' : w --> x₁} {k k' : z --> y₂} (γ : h ==> h') (δ : k ==> k') (Lh : lift_1cell_factor (trivial_displayed_bicat B₁ B₂) g k) (Lh' : lift_1cell_factor (trivial_displayed_bicat B₁ B₂) g k') : lift_2cell_factor (trivial_displayed_bicat B₁ B₂) g (δ := γ) δ Lh Lh'. Proof. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; induction φ₁ as [ φ₁ ψ₁ ] ; induction φ₂ as [ φ₂ ψ₂ ] ; use subtypePath ; [ intro ; apply cellset_property | ] ; cbn in * ; rewrite transportf_const in ψ₁, ψ₂ ; cbn in * ; apply (fully_faithful_1cell_faithful (adj_equiv_fully_faithful Hg)) ; pose (p₂ := trivial_disp_invertible_to_invertible_2cell (pr2 Lh')) ; use (vcomp_rcancel p₂) ; [ apply p₂ | ] ; exact (ψ₁ @ !ψ₂)). - simple refine (_ ,, _) ; cbn. + exact (fully_faithful_1cell_inv_map (adj_equiv_fully_faithful Hg) (pr12 Lh • δ • trivial_disp_invertible_to_invertible_2cell (pr2 Lh')^-1)). + abstract (rewrite transportf_const ; cbn ; etrans ; [ apply maponpaths_2 ; apply (fully_faithful_1cell_inv_map_eq (adj_equiv_fully_faithful Hg)) | ] ; cbn in * ; rewrite !vassocl ; apply maponpaths ; refine (_ @ id2_right _) ; apply maponpaths ; apply (vcomp_linv (trivial_disp_invertible_to_invertible_2cell (pr2 Lh')))). 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.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. 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.Cartesians. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Trivial.