Definition z_iso_comp_left_weq {C : precategory} {a b : C} (h : z_iso a b) (c : C) : (c --> a) ≃ (c --> b) := make_weq _ (z_iso_comp_left_isweq h c).
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.