proposition: Proposition bicat_of_enriched_cat_duality_unit_inv_is_pstrans : is_pstrans bicat_of_enriched_cat_duality_unit_inv_data.
proof: Proof. simple refine (_ ,, _ ,, _). - intros E₁ E₂ F G α ; simpl. use eq_enriched_nat_trans. intro x ; cbn. rewrite id_left, id_right. apply idpath. - intros E. Opaque comp_psfunctor. use eq_enriched_nat_trans. Transparent comp_psfunctor. intros x ; cbn. rewrite !id_left. apply idpath. - intros E₁ E₂ E₃ F G. Opaque comp_psfunctor. use eq_enriched_nat_trans. Transparent comp_psfunctor. intros x ; cbn. rewrite !id_left, !id_right. exact (!(functor_id _ _)). Opaque comp_psfunctor. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Examples.OpCellBicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.Examples.EnrichedCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.PseudoFunctors.Examples.Composition UniMath.Bicategories.PseudoFunctors.Examples.Op2OfPseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.OpFunctorEnriched UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.OtherStructure.DualityInvolution