proposition: Proposition functor_enrichment_to_arr {x y : C₁} (f : I_{V} --> E₁ ⦃ x , y ⦄) : enriched_to_arr E₂ (f · FE x y) = #F (enriched_to_arr E₁ f).
proof: Proof. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E₂ _ _))) ; cbn. rewrite functor_enrichment_from_arr. rewrite !enriched_from_to_arr. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.Limits.Terminal