Zulip Chat Archive

Stream: Is there code for X?

Topic: concrete limits in Type


view this post on Zulip Kevin Buzzard (Nov 02 2020 at 16:08):

Working in the concrete category of types, I find myself with two morphisms XYX\to Y and a proof that ZXZ\to X is an equalizer of this diagram. I have a term of type XX and a proof that the two corresponding terms of type YY are equal. I want to make the corresponding term of type ZZ. 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Bhavik Mehta (Nov 02 2020 at 19:10):

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

view this post on Zulip Bhavik Mehta (Nov 02 2020 at 19:10):

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

view this post on Zulip Kenny Lau (Nov 02 2020 at 19:21):

we can make an API for equalizers in Type

view this post on Zulip Kevin Buzzard (Nov 02 2020 at 19:22):

I am definitely coming round to this idea.

view this post on Zulip Bhavik Mehta (Nov 02 2020 at 19:24):

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

view this post on Zulip Kevin Buzzard (Nov 02 2020 at 20:30):

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

view this post on Zulip 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