Definition representable1_data : pstrans_data (representable C_is_univalent_2_1 X) (representable C_is_univalent_2_1 Y). Proof. use make_pstrans_data. - intro Z. cbn. use make_functor. + use make_functor_data. -- intro g. exact (g · f). -- intros g h η. exact (rwhisker f η). + split. -- intro g. apply id2_rwhisker. -- intros g h k η φ. symmetry. apply rwhisker_vcomp. - intros Z W h. cbn. use make_invertible_2cell. + use make_nat_trans. -- intro k. apply lassociator. -- intros k l η. cbn in *. apply rwhisker_lwhisker. + use is_nat_z_iso_to_is_invertible_2cell. intro g. apply is_inv2cell_to_is_z_iso. simpl. is_iso. 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.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification.