Zulip Chat Archive

Stream: Is there code for X?

Topic: concrete limits in Type

Kevin Buzzard (Nov 02 2020 at 16:08):

Working in the concrete category of types, I find myself with two morphisms $X\to Y$ and a proof that $Z\to X$ is an equalizer of this diagram. I have a term of type $X$ and a proof that the two corresponding terms of type $Y$ are equal. I want to make the corresponding term of type $Z$ . Should I do this by creating a map punit -> X and then applying category-theory mumbo-jumbo or is there a less "primitive" way to do this?

Bhavik Mehta (Nov 02 2020 at 18:30):

Ha I was playing with this too today, it's more awkward than I'd like! I think it might be a good idea to have a lemma saying:

lemma type_equalizer {X Y Z : Type v} (f : X ⟶ Y) (g h : Y ⟶ Z) (w : f ≫ g = f ≫ h) :
  (∀ (y : Y), g y = h y → ∃! (x : X), f x = y) ↔ nonempty (is_limit (fork.of_ι _ w)) := sorry

What do you and others think about this?

Bhavik Mehta (Nov 02 2020 at 18:32):

The proof of course goes via the map punit -> X like you suggest but I think it's just a bit too painful needing to go through this messiness in the middle of a bigger proof, so I think something like this lemma would help