Coequilizers

Stream: maths

[Dean Young]

How might one construct the coequalizer of two parallel functions between types X and Y?

def coeq {X : Type} {Y : Type} (f : X → Y) (g : X → Y) := by
sorry

[Adam Topaz]

One approach is to use a quotient

[Adam Topaz]

That gives the concrete type. You can also use the category theory library and use colimits

[Dean Young]

Do you know where the documentation for an equivalence relation is? How might I fill these in?

variable {X : Type}
variable {p : X → X → Prop}
variable {reflexivity : (x : X) → (p x x)}
variable {symmetry : (x : X) → (p x y) → (p y x)}
variable {transitivity : (x : X) → (y : X) → (z : X) → (p x y)  → (p y z)  → (p x z)}

def R : equivalence_relation X := by
sorry

def XmodR := by
sorry

[Kyle Miller]

docs4#Equivalence (I searched for "equivalence" in the mathlib4 docs to see what it's called now)

[Kyle Miller]

docs4#Quotient takes a docs4#Setoid (which is what equivalence relation with its Equivalence proof is called) and gives the quotient.