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


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

Kevin Buzzard (Nov 02 2020 at 18:39):

The reason I didn't suggest that is because today it's equalizers, and then tomorrow it's products, the day after it's something else. But I agree!

Adam Topaz (Nov 02 2020 at 19:03):

I think it's worthwhile to have concrete representations for the (co)limits that can be easily represented with type theory (+ quotients). E.g.:

1. Equalizers (as a subtype) / coequalizers (as quotient)
2. Fibered (fibred?) products / pullbacks (as a subtype of the product)
3. Binary coproducts (as a type-level sum)
4. Products (as a Pi type)

Are there any others that might be useful?

Bhavik Mehta (Nov 02 2020 at 19:10):

They're already present for binary and arbitrary products and coproducts and terminal and initial objects

Bhavik Mehta (Nov 02 2020 at 19:10):

I think that combined with your list is everything I can think is helpful

Kenny Lau (Nov 02 2020 at 19:21):

we can make an API for equalizers in Type

Kevin Buzzard (Nov 02 2020 at 19:22):

I am definitely coming round to this idea.

Bhavik Mehta (Nov 02 2020 at 19:24):

https://github.com/leanprover-community/mathlib/pull/4880

Kevin Buzzard (Nov 02 2020 at 20:30):

Oh nice! Yeah this is perfect for my use case :D Thanks!

Bhavik Mehta (Nov 02 2020 at 20:37):

I think that might be because my use case is very similar to yours :)

Last updated: May 17 2021 at 14:12 UTC