Definition precomp_arr_z_iso {V : monoidal_cat} {C : category} (E : enrichment C V) (z : C) {x y : C} (f : z_iso x y) : z_iso (E ⦃ y , z ⦄) (E ⦃ x , z ⦄). Proof. refine (precomp_arr E z f ,, _). use precomp_arr_is_z_iso. exact (pr2 f). Defined.
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.