Definition postcomp_arr_z_iso {V : monoidal_cat} {C : category} (E : enrichment C V) (w : C) {x y : C} (f : z_iso x y) : z_iso (E ⦃ w , x ⦄) (E ⦃ w , y ⦄). Proof. refine (postcomp_arr E w f ,, _). use postcomp_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.