Equivalence relations

We define internal equivalence relations (sometimes called congruences) in any category C, as a structure on pairs of parallel morphisms p₁, p₂ : R ⟶ X . We also define effective and universally effective equivalence relations.

We prove that equivalence relations on types provide internal equivalence relation structures in the category of types. In general, kernel pairs in any category are internal equivalence relations.

References

• https://ncatlab.org/nlab/show/congruence

class CategoryTheory.JointlyMono₂ {C : Type u_1} [Category.{v_1, u_1} C] {R X₁ X₂ : C} (p₁ : R ⟶ X₁) (p₂ : R ⟶ X₂) : Prop

A typeclass for pairs of morphisms that are jointly monic.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g

structure CategoryTheory.ReflexiveRelation {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} (p₁ p₂ : R ⟶ X) extends CategoryTheory.JointlyMono₂ p₁ p₂ : Type v_1

A reflexive relation is a jointly monic pair of parallel morphisms p₁, p₂ : R ⟶ X, together with a section r : X ⟶ R of both p₁ and p₂.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g
• r : X ⟶ R

  r is the morphism witnessing reflexivity

• reflexivity₁ : CategoryStruct.comp self.r p₁ = CategoryStruct.id X
• reflexivity₂ : CategoryStruct.comp self.r p₂ = CategoryStruct.id X

@[simp]

theorem CategoryTheory.ReflexiveRelation.reflexivity₁_assoc {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : ReflexiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.r (CategoryStruct.comp p₁ h) = h

@[simp]

theorem CategoryTheory.ReflexiveRelation.reflexivity₂_assoc {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : ReflexiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.r (CategoryStruct.comp p₂ h) = h

@[simp]

theorem CategoryTheory.ReflexiveRelation.reflexivity₂_apply {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : ReflexiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : carrier X) : (ConcreteCategory.hom p₂) ((ConcreteCategory.hom self.r) x) = x

@[simp]

theorem CategoryTheory.ReflexiveRelation.reflexivity₁_apply {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : ReflexiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : carrier X) : (ConcreteCategory.hom p₁) ((ConcreteCategory.hom self.r) x) = x

structure CategoryTheory.SymmetricRelation {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} (p₁ p₂ : R ⟶ X) extends CategoryTheory.JointlyMono₂ p₁ p₂ : Type v_1

A symmetric relation is a jointly monic pair of parallel morphisms p₁, p₂ : R ⟶ X together with a morphism s : R ⟶ R which interchanges p₁ and p₂.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g
• s : R ⟶ R

  s is the morphism witnessing symmetry

• symmetry₁ : CategoryStruct.comp self.s p₁ = p₂
• symmetry₂ : CategoryStruct.comp self.s p₂ = p₁

@[simp]

theorem CategoryTheory.SymmetricRelation.symmetry₁_assoc {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : SymmetricRelation p₁ p₂) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.s (CategoryStruct.comp p₁ h) = CategoryStruct.comp p₂ h

@[simp]

theorem CategoryTheory.SymmetricRelation.symmetry₂_assoc {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : SymmetricRelation p₁ p₂) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.s (CategoryStruct.comp p₂ h) = CategoryStruct.comp p₁ h

@[simp]

theorem CategoryTheory.SymmetricRelation.symmetry₂_apply {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : SymmetricRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : carrier R) : (ConcreteCategory.hom p₂) ((ConcreteCategory.hom self.s) x) = (ConcreteCategory.hom p₁) x

@[simp]

theorem CategoryTheory.SymmetricRelation.symmetry₁_apply {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : SymmetricRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : carrier R) : (ConcreteCategory.hom p₁) ((ConcreteCategory.hom self.s) x) = (ConcreteCategory.hom p₂) x

structure CategoryTheory.TransitiveRelation {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} (p₁ p₂ : R ⟶ X) extends CategoryTheory.JointlyMono₂ p₁ p₂ : Type (max u_1 v_1)

A transitive relation is a jointly monic pair of parallel morphisms p₁, p₂ : R ⟶ X, together with a limiting pullback cone c for p₁ and p₂ and a map c.pt ⟶ R which factors the two projections c.pt ⟶ X through R.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g
• c : Limits.PullbackCone p₂ p₁

  c is a pullback cone for p₁ and p₂

• isLimit : Limits.IsLimit self.c

  c is limiting

• t : self.c.pt ⟶ R

  t is the morphism witnessing transitivity

• transitivity₁ : CategoryStruct.comp self.t p₁ = CategoryStruct.comp self.c.fst p₁
• transitivity₂ : CategoryStruct.comp self.t p₂ = CategoryStruct.comp self.c.snd p₂

@[simp]

theorem CategoryTheory.TransitiveRelation.transitivity₁_assoc {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : TransitiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.t (CategoryStruct.comp p₁ h) = CategoryStruct.comp self.c.fst (CategoryStruct.comp p₁ h)

@[simp]

theorem CategoryTheory.TransitiveRelation.transitivity₂_assoc {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : TransitiveRelation p₁ p₂) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.t (CategoryStruct.comp p₂ h) = CategoryStruct.comp self.c.snd (CategoryStruct.comp p₂ h)

@[simp]

theorem CategoryTheory.TransitiveRelation.transitivity₁_apply {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : TransitiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : carrier self.c.pt) : (ConcreteCategory.hom p₁) ((ConcreteCategory.hom self.t) x) = (ConcreteCategory.hom p₁) ((ConcreteCategory.hom self.c.fst) x)

@[simp]

theorem CategoryTheory.TransitiveRelation.transitivity₂_apply {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (self : TransitiveRelation p₁ p₂) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : carrier self.c.pt) : (ConcreteCategory.hom p₂) ((ConcreteCategory.hom self.t) x) = (ConcreteCategory.hom p₂) ((ConcreteCategory.hom self.c.snd) x)

structure CategoryTheory.EquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} (p₁ p₂ : R ⟶ X) extends CategoryTheory.ReflexiveRelation p₁ p₂, CategoryTheory.SymmetricRelation p₁ p₂, CategoryTheory.TransitiveRelation p₁ p₂ : Type (max u_1 v_1)

An equivalence relation is a reflexive, symmetric and transitive relation.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g
• r : X ⟶ R
• reflexivity₁ : CategoryStruct.comp self.r p₁ = CategoryStruct.id X
• reflexivity₂ : CategoryStruct.comp self.r p₂ = CategoryStruct.id X
• s : R ⟶ R
• symmetry₁ : CategoryStruct.comp self.s p₁ = p₂
• symmetry₂ : CategoryStruct.comp self.s p₂ = p₁
• c : Limits.PullbackCone p₂ p₁
• isLimit : Limits.IsLimit self.c
• t : self.c.pt ⟶ R
• transitivity₁ : CategoryStruct.comp self.t p₁ = CategoryStruct.comp self.c.fst p₁
• transitivity₂ : CategoryStruct.comp self.t p₂ = CategoryStruct.comp self.c.snd p₂

class CategoryTheory.IsEquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} (p₁ p₂ : R ⟶ X) : Prop

The typeclass associated with the structure EquivalenceRelation.

• nonempty_equivalenceRelation : Nonempty (EquivalenceRelation p₁ p₂)

theorem CategoryTheory.EquivalenceRelation.isEquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} (h : EquivalenceRelation p₁ p₂) : IsEquivalenceRelation p₁ p₂

noncomputable def CategoryTheory.IsKernelPair.equivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) {R : C} (p₁ p₂ : R ⟶ X) {t : Limits.PullbackCone p₂ p₁} (ht : Limits.IsLimit t) (h : IsKernelPair f p₁ p₂) : EquivalenceRelation p₁ p₂

A kernel pair gives rise to an equivalence relation.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.ReflexiveRelation.map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {R X : C} {p₁ p₂ : R ⟶ X} (e : ReflexiveRelation p₁ p₂) (F : Functor C D) [JointlyMono₂ (F.map p₁) (F.map p₂)] : ReflexiveRelation (F.map p₁) (F.map p₂)

Given a functor F : C ⥤ D, if F.map p₁ and F.map p₂ form a jointly monic pair of morphisms, then F preserves reflexive relations.

Equations

• e.map F = { toJointlyMono₂ := inst✝, r := F.map e.r, reflexivity₁ := ⋯, reflexivity₂ := ⋯ }

def CategoryTheory.SymmetricRelation.map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {R X : C} {p₁ p₂ : R ⟶ X} (e : SymmetricRelation p₁ p₂) (F : Functor C D) [JointlyMono₂ (F.map p₁) (F.map p₂)] : SymmetricRelation (F.map p₁) (F.map p₂)

Given a functor F : C ⥤ D, if F.map p₁ and F.map p₂ form a jointly monic pair of morphisms, then F preserves symmetric relations.

Equations

• e.map F = { toJointlyMono₂ := inst✝, s := F.map e.s, symmetry₁ := ⋯, symmetry₂ := ⋯ }

noncomputable def CategoryTheory.TransitiveRelation.map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {R X : C} {p₁ p₂ : R ⟶ X} (e : TransitiveRelation p₁ p₂) (F : Functor C D) [JointlyMono₂ (F.map p₁) (F.map p₂)] [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] : TransitiveRelation (F.map p₁) (F.map p₂)

Given a functor F : C ⥤ D, if F.map p₁ and F.map p₂ form a jointly monic pair of morphisms, and if F preserves pullbacks, then F preserves reflexive relations.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev TypeCat.ROfRel {X : Type w} (φ : X → X → Prop) : Type w

The subtype of X × X corresponding to a relation φ : X → X → Prop.

Equations

• TypeCat.ROfRel φ = Subtype (Function.uncurry φ)

@[reducible, inline]

abbrev TypeCat.p₁OfRel {X : Type w} (φ : X → X → Prop) : ROfRel φ ⟶ X

The first projection ROfRel ⟶ X.

Equations

• TypeCat.p₁OfRel φ = TypeCat.ofHom (Prod.fst ∘ Subtype.val)

@[reducible, inline]

abbrev TypeCat.p₂OfRel {X : Type w} (φ : X → X → Prop) : ROfRel φ ⟶ X

The second projection ROfRel ⟶ X.

Equations

• TypeCat.p₂OfRel φ = TypeCat.ofHom (Prod.snd ∘ Subtype.val)

theorem TypeCat.jointlyMono₂ {X : Type w} (φ : X → X → Prop) : CategoryTheory.JointlyMono₂ (p₁OfRel φ) (p₂OfRel φ)

def TypeCat.ReflexiveRelation.ofRefl {X : Type w} {φ : X → X → Prop} (hφ : Std.Refl φ) : CategoryTheory.ReflexiveRelation (p₁OfRel φ) (p₂OfRel φ)

Standard reflexive relations on types are internal reflexive relations in the category of types.

Equations

• TypeCat.ReflexiveRelation.ofRefl hφ = { toJointlyMono₂ := ⋯, r := TypeCat.ofHom fun (x : X) => ⟨(x, x), ⋯⟩, reflexivity₁ := ⋯, reflexivity₂ := ⋯ }

def TypeCat.SymmetricRelation.ofSymmetric {X : Type w} {φ : X → X → Prop} [Std.Symm φ] : CategoryTheory.SymmetricRelation (p₁OfRel φ) (p₂OfRel φ)

Standard symmetric relations on types are internal symmetric relations in the category of types.

Equations

• One or more equations did not get rendered due to their size.

def TypeCat.TransitiveRelation.ofIsTrans {X : Type w} {φ : X → X → Prop} (hφ : IsTrans X φ) : CategoryTheory.TransitiveRelation (p₁OfRel φ) (p₂OfRel φ)

Standard transitive relations on types are internal transitive relations in the category of types.

Equations

• One or more equations did not get rendered due to their size.

def TypeCat.EquivalenceRelation.ofEquivalence {X : Type w} {φ : X → X → Prop} (hφ : Equivalence φ) : CategoryTheory.EquivalenceRelation (p₁OfRel φ) (p₂OfRel φ)

Standard equivalence relations on types are internal equivalence relations in the category of types.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev TypeCat.Rel.ofPair {X R : Type w} (p₁ p₂ : R ⟶ X) (x₁ x₂ : X) : Prop

The relation on a type X coming from a pair of maps R ⟶ X.

Equations

• TypeCat.Rel.ofPair p₁ p₂ x₁ x₂ = ∃ (r : R), (CategoryTheory.ConcreteCategory.hom p₁) r = x₁ ∧ (CategoryTheory.ConcreteCategory.hom p₂) r = x₂

theorem TypeCat.refl_of_reflexiveRelation {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.ReflexiveRelation p₁ p₂) : Std.Refl (Rel.ofPair p₁ p₂)

An internal reflexive relation in the category of types gives rise to a standard reflexive relation.

theorem TypeCat.symm_of_symmetricRelation {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.SymmetricRelation p₁ p₂) : Std.Symm (Rel.ofPair p₁ p₂)

An internal symmetric relation in the category of types gives rise to a standard symmetric relation.

@[deprecated TypeCat.symm_of_symmetricRelation (since := "2026-06-10")]

theorem TypeCat.symmetric_of_symmetricRelation {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.SymmetricRelation p₁ p₂) : Std.Symm (Rel.ofPair p₁ p₂)

Alias of TypeCat.symm_of_symmetricRelation.

---

An internal symmetric relation in the category of types gives rise to a standard symmetric relation.

theorem TypeCat.isTrans_of_transitiveRelation {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.TransitiveRelation p₁ p₂) : IsTrans X (Rel.ofPair p₁ p₂)

An internal transitive relation in the category of types gives rise to a standard transitive relation.

theorem TypeCat.equivalence_of_equivalenceRelation {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.EquivalenceRelation p₁ p₂) : Equivalence (Rel.ofPair p₁ p₂)

An internal equivalence relation in the category of types gives rise to a standard equivalence relation.

structure CategoryTheory.EffectiveEquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A) extends CategoryTheory.EquivalenceRelation p₁ p₂ : Type (max u_1 v_1)

An effective equivalence relation is an equivalence relation p₁, p₂ : R ⟶ A together with a morphism π : A ⟶ B such that the resulting square is both a pullback square and a pushout square.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g
• r : A ⟶ R
• reflexivity₁ : CategoryStruct.comp self.r p₁ = CategoryStruct.id A
• reflexivity₂ : CategoryStruct.comp self.r p₂ = CategoryStruct.id A
• s : R ⟶ R
• symmetry₁ : CategoryStruct.comp self.s p₁ = p₂
• symmetry₂ : CategoryStruct.comp self.s p₂ = p₁
• c : Limits.PullbackCone p₂ p₁
• isLimit : Limits.IsLimit self.c
• t : self.c.pt ⟶ R
• transitivity₁ : CategoryStruct.comp self.t p₁ = CategoryStruct.comp self.c.fst p₁
• transitivity₂ : CategoryStruct.comp self.t p₂ = CategoryStruct.comp self.c.snd p₂
• B : C

  B is the "quotient" of the relation

• π : A ⟶ self.B

  π is the "quotient map" of the relation

• isKernelPair : IsKernelPair self.π p₁ p₂
• isPushout : IsPushout p₁ p₂ self.π self.π

class CategoryTheory.IsEffectiveEquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A) : Prop

The typeclass associated with the structure EffectiveEquivalenceRelation.

• nonempty_effectiveEquivalenceRelation : Nonempty (EffectiveEquivalenceRelation p₁ p₂)

noncomputable def CategoryTheory.EffectiveEquivalenceRelation.isCoequalizer {C : Type u_1} [Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A) (e : EffectiveEquivalenceRelation p₁ p₂) : Limits.IsColimit (Limits.Cofork.ofπ e.π ⋯)

Given an effective equivalence relation structure e on p₁, p₂ : R ⟶ A, the morphism e.π : A ⟶ e.B makes e.B a coequalizer of p₁ and p₂.

Equations

• CategoryTheory.EffectiveEquivalenceRelation.isCoequalizer p₁ p₂ e = ⋯.isLimitFork

instance CategoryTheory.instIsRegularEpiπ_1 {C : Type u_1} [Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A) (e : EffectiveEquivalenceRelation p₁ p₂) : IsRegularEpi e.π

structure CategoryTheory.UniversallyEffectiveEquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A) extends CategoryTheory.EffectiveEquivalenceRelation p₁ p₂ : Type (max u_1 v_1)

A universally effective equivalence relation is an effective equivalence relation p₁, p₂ : R ⟶ A such that the corresponding morphism π : A ⟶ B is a universal effective epimorphism.

• right_cancellation ⦃Y : C⦄ (f g : Y ⟶ R) : CategoryStruct.comp f p₁ = CategoryStruct.comp g p₁ → CategoryStruct.comp f p₂ = CategoryStruct.comp g p₂ → f = g
• r : A ⟶ R
• reflexivity₁ : CategoryStruct.comp self.r p₁ = CategoryStruct.id A
• reflexivity₂ : CategoryStruct.comp self.r p₂ = CategoryStruct.id A
• s : R ⟶ R
• symmetry₁ : CategoryStruct.comp self.s p₁ = p₂
• symmetry₂ : CategoryStruct.comp self.s p₂ = p₁
• c : Limits.PullbackCone p₂ p₁
• isLimit : Limits.IsLimit self.c
• t : self.c.pt ⟶ R
• transitivity₁ : CategoryStruct.comp self.t p₁ = CategoryStruct.comp self.c.fst p₁
• transitivity₂ : CategoryStruct.comp self.t p₂ = CategoryStruct.comp self.c.snd p₂
• B : C
• π : A ⟶ self.B
• isKernelPair : IsKernelPair self.π p₁ p₂
• isPushout : IsPushout p₁ p₂ self.π self.π
• universally_effectiveEpi_π : MorphismProperty.universally (fun (x x_1 : C) (f : x ⟶ x_1) => EffectiveEpi f) self.π

class CategoryTheory.IsUniversallyEffectiveEquivalenceRelation {C : Type u_1} [Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A) : Prop

The typeclass associated with the structure UniversallyEffectiveEquivalenceRelation.

• nonempty_universallyEffectiveEquivalenceRelation : Nonempty (UniversallyEffectiveEquivalenceRelation p₁ p₂)

class CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategory (C : Type u_1) [Category.{v_1, u_1} C] {R A : C} : Prop

A category C is a universally exact category if all equivalence relations in C are universally effective equivalence relations.

• isUniversallyEffectiveEquivalenceRelation (p₁ p₂ : R ⟶ A) [IsEquivalenceRelation p₁ p₂] : IsUniversallyEffectiveEquivalenceRelation p₁ p₂