Library UniMath.CategoryTheory.Categories.Type.MonoEpiIso
Characterizations of monos, epis, and isos in type_precat
Contents
- Injective functions are monic InjectivesAreMonic_type
- Isomorphisms and weak equivalences
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.Categories.Type.Core.
Local Open Scope cat.