proposition: Lemma morphism_from_iso_is_incl (C : category) (a b : ob C) : isincl (@morphism_from_z_iso C a b).
proof: Proof. intro g. apply (isofhlevelweqf _ (ezweqpr1 _ _)). apply isaprop_is_z_isomorphism. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat