Definition total_disp_left_universal_arrow (dLURu : disp_left_universal_arrow_universality) : left_universal_arrow (total_psfunctor D1 D2 R RR). Proof. exists (λ x, L (pr1 x),, LL _ (pr2 x)). exists (λ x, η (pr1 x) ,, ηη _ (pr2 x)). intros [x xx] [y yy]. use nat_iso_adj_equivalence_of_cats. - exact (total_functor (disp_left_universal_arrow_functor xx yy)). - apply nat_trans_id. - use is_nat_z_iso_nat_trans_id. - exact (total_adj_equivalence_of_cats (dLURu x xx y yy)). 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.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.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.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.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.