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. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E₂ _ _))) ; cbn. rewrite functor_enrichment_from_arr. rewrite !enriched_from_to_arr. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.Terminal. Import MonoidalNotations.