Equalizer in Type

Stream: Is there code for X?

[Kenny Lau]

Do we have explicit equalizer in Type? Specifically:

def Equalizer {α : Type u} {β : Type v} (f g : α → β) : Type u :=
  { x // f x = g x }

I would assume the answer is no because we have AlgHom.equalizer whose underlying set is defined explicitly.

But I would also assume yes because surely at some point we would have proved that the category Type u has equaliser...

[Kenny Lau]

Ok I did further digging on the last sentence,

import Mathlib

open CategoryTheory Limits

variable {X Y : Type u} (f g : X ⟶ Y)
#check (inferInstance : HasEqualizer f g)
#check Types.hasLimit

and it seems that it was proved abstractly that Type u has all small limits (remember that Has[...] is a Prop), so... they might have avoided explicitly constructing it for the equaliser diagram explicitly

[Kenny Lau]

and I did more digging https://github.com/leanprover-community/mathlib4/blob/02c6431ffe61ac7571e0281242e025e54638ad42/Mathlib/CategoryTheory/Limits/Types/Limits.lean#L101-L108

noncomputable def limitCone : Cone F where
  pt := Shrink F.sections

[Kenny Lau]

so in conclusion I don't think this has been explicitly done in Type u and people probably thought "but who needs the concrete construction"

[Markus Himmel]

We have the dual as docs#Function.Coequalizer

[Adam Topaz]

We probably have some general API about limits in concrete categories that will allow you to view the equalizer as the set $\{(x,y) \ | \ f x = g x = y \}$. What do you need this for?

[Kenny Lau]

@Adam Topaz I have two corepresentable functors F, G: C => Type and an equaliser diagram F ->->G and a third functor H isomorphic to the equaliser and I want to show (i.e. construct data) that H is also corepresentable

[Markus Himmel]

There is docs#CategoryTheory.Limits.Types.equalizerIso. There are also things like docs#CategoryTheory.Limits.pullbackObjIso, but the analogous equalizerObjIso doesn't exist yet I believe.