Proposition transportf_enriched_arr_r {V : monoidal_cat} {C : category} (E : enrichment C V) (x : C) {y₁ y₂ : C} (p : y₁ = y₂) (f : I_{ V} --> E ⦃ x , y₁ ⦄) : transportf (λ (y : C), I_{V} --> E ⦃ x , y ⦄) p f = enriched_from_arr E (enriched_to_arr E f · idtoiso p). Proof. induction p ; cbn. rewrite id_right. rewrite enriched_from_to_arr. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.