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} [Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y} {c : Limits.PullbackCone f f} (hc : Limits.IsLimit c) : Mono f ↔ c.fst = c.snd

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

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

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

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

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

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

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