Zulip Chat Archive

Stream: general

Topic: singleton


Scott Morrison (Aug 12 2018 at 02:05):

Am I just missing a singleton class, the pushout of inhabited and subsingleton? Am I meant to define my own?

Mario Carneiro (Aug 12 2018 at 02:06):

do you need one?

Mario Carneiro (Aug 12 2018 at 02:07):

You can just assume both classes if you need

Scott Morrison (Aug 12 2018 at 02:08):

just seems wordy: I was about to use this a whole bunch of times

Mario Carneiro (Aug 12 2018 at 02:08):

for what?

Scott Morrison (Aug 12 2018 at 02:09):

universal properties

Scott Morrison (Aug 12 2018 at 02:10):

I wanted to try out a design for equalizers/products/pushouts based on a class is_equalizer, which would have a singleton ... field that expresses that there's a map with some property, and that map is unique.

Mario Carneiro (Aug 12 2018 at 02:10):

hm, I would say that's a bit too clever

Mario Carneiro (Aug 12 2018 at 02:10):

just state the map and state a separate field asserting it is unique

Scott Morrison (Aug 12 2018 at 02:10):

my current design just says these things separately

Mario Carneiro (Aug 12 2018 at 02:11):

You will have to unpack it all the time

Scott Morrison (Aug 12 2018 at 02:11):

structure Equalizer (f g : X ⟶ Y) :=
(equalizer     : C)
(inclusion     : equalizer ⟶ X)
(map           : ∀ {Z : C} (k : Z ⟶ X) (w : k ≫ f = k ≫ g), Z ⟶ equalizer)
(witness       : inclusion ≫ f = inclusion ≫ g . obviously)
(factorisation : ∀ {Z : C} (k : Z ⟶ X) (w : k ≫ f = k ≫ g), (map k w) ≫ inclusion = k . obviously)
(uniqueness    : ∀ {Z : C} (a b : Z ⟶ equalizer) (witness : a ≫ inclusion = b ≫ inclusion), a = b . obviously)

Scott Morrison (Aug 12 2018 at 02:12):

the alternative would be to pack map, witness, factorisation, and uniqueness all into one singleton instance, with an appropriate subtype

Mario Carneiro (Aug 12 2018 at 02:12):

uniqueness can be stated with one fewer pi btw

Scott Morrison (Aug 12 2018 at 02:12):

you mean don't name witness?

Mario Carneiro (Aug 12 2018 at 02:12):

just say a = witness at the end

Scott Morrison (Aug 12 2018 at 02:12):

sure

Mario Carneiro (Aug 12 2018 at 02:12):

the other witness

Scott Morrison (Aug 12 2018 at 02:13):

oh, I see

Scott Morrison (Aug 12 2018 at 02:13):

yeah, I've gone back and forth on that a few times

Mario Carneiro (Aug 12 2018 at 02:13):

er, I mean a = map something something

Mario Carneiro (Aug 12 2018 at 02:14):

Also, you can pack witness and factorisation and uniqueness into one field with an iff

Scott Morrison (Aug 12 2018 at 02:15):

that was Reid's design

Scott Morrison (Aug 12 2018 at 02:15):

I feel like that has the same objection to using singleton, but the unpacking and packing required is even less intuitive

Mario Carneiro (Aug 12 2018 at 02:16):

I just want to avoid packing the data in too

Scott Morrison (Aug 12 2018 at 02:16):

I see.

Mario Carneiro (Aug 12 2018 at 02:17):

Would you like a way to quickly say {a | p a} = {x}?

Scott Morrison (Aug 12 2018 at 02:18):

(a = x) iff p a

Mario Carneiro (Aug 12 2018 at 02:18):

right, with a abstracted

Scott Morrison (Aug 12 2018 at 02:19):

Ok. This is exactly how Reid did things in the category theory he has in his homotopy library. At first I didn't like it much, but I'm coming around. :-)

Mario Carneiro (Aug 12 2018 at 02:20):

like def is_the {α} (p : α → Prop) (x : α) := ∀ a, x = a ↔ p a

Scott Morrison (Aug 12 2018 at 02:20):

I will see if I can do something that feels uniform across product/equalizer/pullback, and makes things sufficiently obvious.

Mario Carneiro (Aug 12 2018 at 02:21):

the definition might be gratuitous

Scott Morrison (Aug 12 2018 at 02:21):

perhaps something like universal_property instead of is_the? Longer, but friendlier to the mathematicians.

Scott Morrison (Aug 12 2018 at 02:21):

I'll try with and without. :-)

Mario Carneiro (Aug 12 2018 at 02:21):

the name is based on the the sometimes used for definite description

Mario Carneiro (Aug 12 2018 at 02:22):

it's ∃! with the witness free

Scott Morrison (Aug 12 2018 at 02:22):

Yeah; just a note that this is how you talk about universal properties will be good enough for the mathematicians.

Scott Morrison (Aug 12 2018 at 02:23):

okay, kids need lunch!

Mario Carneiro (Aug 12 2018 at 02:23):

I'm open to slick binder notations for that


Last updated: Dec 20 2023 at 11:08 UTC