Definition z_iso_comp {C : precategory} {a b c : C} (I1 : z_iso a b) (I2 : z_iso b c) : z_iso a c. Proof. use make_z_iso. - exact (I1 · I2). - exact ((inv_from_z_iso I2) · (inv_from_z_iso I1)). - exact (is_inverse_in_precat_comp I1 I2). Defined.
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.