proposition: Proposition disp_locally_sym_enriched_cats : disp_locally_sym disp_bicat_of_enriched_cats.
proof: Proof. intros C₁ C₂ F G τ E₁ E₂ EF EG Eτ. use nat_trans_enrichment_via_comp. intros x y ; cbn. refine (!(id_right _) @ _). rewrite <- postcomp_arr_id. etrans. { do 2 apply maponpaths. exact (!(maponpaths (λ z, pr1 z y) (vcomp_rinv τ))). } cbn. rewrite postcomp_arr_comp. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite precomp_postcomp_arr. cbn. rewrite !assoc. etrans. { apply maponpaths_2. apply (!nat_trans_enrichment_to_comp Eτ x y). } rewrite !assoc'. rewrite <- precomp_arr_comp. etrans. { do 2 apply maponpaths. exact (maponpaths (λ z, pr1 z x) (vcomp_linv τ)). } cbn. rewrite precomp_arr_id. apply id_right. 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.whiskering UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.Projection