Relation between mono/epi and pullback/pushout squares

In this file, monomorphisms and epimorphisms are characterized in terms of pullback and pushout squares. For example, we obtain mono_iff_isPullback which asserts that a morphism f : X ⟶ Y is a monomorphism iff the obvious square

X ⟶ X
|   |
v   v
X ⟶ Y

is a pullback square.

theorem CategoryTheory.mono_iff_fst_eq_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono f ↔ c.fst = c.snd

theorem CategoryTheory.mono_iff_isIso_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.fst

theorem CategoryTheory.mono_iff_isIso_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd

theorem CategoryTheory.mono_iff_isPullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) f f

theorem CategoryTheory.epi_iff_inl_eq_inr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PushoutCocone f f} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Epi f ↔ c.inl = c.inr

theorem CategoryTheory.epi_iff_isIso_inl {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PushoutCocone f f} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inl

theorem CategoryTheory.epi_iff_isIso_inr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PushoutCocone f f} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inr

theorem CategoryTheory.epi_iff_isPushout {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ CategoryTheory.IsPushout f f (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)