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