Definition weq_iso_z_iso {C : category} {b c : C} : iso b c ≃ z_iso b c. Proof. exists iso_to_z_iso. use isweq_iso. - apply z_iso_to_iso. - apply roundtrip1_iso_z_iso. - apply roundtrip2_iso_z_iso. 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.