Definition iso_in_subcategory_of_monics_weq (a b : subcategory_of_monics) : z_iso (pr1 a) (pr1 b) ≃ z_iso a b. Proof. use weq_iso. - intro f. use (make_z_iso _ _ (make_dirprod _ _)). + exact (is_iso_Monic _ _ (pr2 f)). + exact (is_iso_Monic _ _ (pr2 (z_iso_inv f))). + abstract apply Monic_eq, (z_iso_inv_after_z_iso f). + abstract apply Monic_eq, (z_iso_after_z_iso_inv f). - intro f. exact (_ ,, invmap (is_z_iso_in_subcategory_of_monics_weq _ _ _) (pr2 f)). - abstract ( intro f; apply z_iso_eq; reflexivity ). - abstract ( intro f; apply z_iso_eq; apply Monic_eq; reflexivity ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Subcategory.Core.