fact: 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).
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories