Proposition transportf_enriched_arr_l {V : monoidal_cat} {C : category} (E : enrichment C V) {x₁ x₂ : C} (p : x₁ = x₂) (y : C) (f : I_{V} --> E ⦃ x₁ , y ⦄) : transportf (λ (x : C), I_{V} --> E ⦃ x , y ⦄) p f = enriched_from_arr E (idtoiso (!p) · enriched_to_arr E f). Proof. induction p ; cbn. rewrite id_left. 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.