Balanced categories

A category is called balanced if any morphism that is both monic and epic is an isomorphism.

Balanced categories arise frequently. For example, categories in which every monomorphism (or epimorphism) is strong are balanced. Examples of this are abelian categories and toposes, such as the category of types.

class CategoryTheory.Balanced (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• isIso_of_mono_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f] [inst : CategoryTheory.Epi f], CategoryTheory.IsIso f

A category is called balanced if any morphism that is both monic and epic is an isomorphism.

theorem CategoryTheory.isIso_of_mono_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.Epi f] : CategoryTheory.IsIso f

theorem CategoryTheory.isIso_iff_mono_and_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.Mono f ∧ CategoryTheory.Epi f

theorem CategoryTheory.balanced_opposite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C] : CategoryTheory.Balanced Cᵒᵖ