Definition make_disp_left_universal_arrow_if_contr_CAT_from_weak_equiv : disp_left_universal_arrow LUR RR. Proof. use make_disp_left_universal_arrow_if_contr_CAT. - intros C CC. use (weak_equiv_preserve_struct _ _ _ (η C)). + apply (pr1 LUR C). + apply η_weak_equiv. + exact CC. - exact η_preserves_structs. - intros C1 CC1 C2 CC2 F FF. use (extension_preserves_struct C1 (LL0' C1) C2 F (η C1) _ _ CC1). + set (t := counit_nat_z_iso_from_adj_equivalence_of_cats (pr22 LUR C1 C2)). set (tg := nat_z_iso_pointwise_z_iso t F). exact (nat_z_iso_from_z_iso (homset_property _) tg). + apply η_weak_equiv. + exact FF. 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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Adjunctions. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.TotalAdjunction. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBiadjunction. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrow. Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOnCatToUniv. Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.