Definition nat_z_iso_comp {C : precategory_data} {D : precategory} {F G H: C ⟶ D} (μ: nat_z_iso F G) (ν: nat_z_iso G H) : nat_z_iso F H. Proof. use make_nat_z_iso. - exact (nat_trans_comp F G H μ ν). - exact (is_nat_z_iso_comp (pr2 μ) (pr2 ν)). 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.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.