Definition precomp_arr_is_z_iso {V : monoidal_cat} {C : category} (E : enrichment C V) (z : C) {x y : C} (f : x --> y) (Hf : is_z_isomorphism f) : is_z_isomorphism (precomp_arr E z f). Proof. pose (f_iso := make_z_iso _ _ Hf). use make_is_z_isomorphism. - exact (precomp_arr E z (inv_from_z_iso f_iso)). - split. + abstract (rewrite <- precomp_arr_comp ; rewrite <- precomp_arr_id ; apply maponpaths ; apply (z_iso_after_z_iso_inv f_iso)). + abstract (rewrite <- precomp_arr_comp ; rewrite <- precomp_arr_id ; apply maponpaths ; apply (z_iso_inv_after_z_iso f_iso)). 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.