Zulip Chat Archive

Stream: general

Topic: singleton


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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:06):

do you need one?

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:07):

You can just assume both classes if you need

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:08):

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:08):

for what?

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:09):

universal properties

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:10):

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:10):

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

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:10):

my current design just says these things separately

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:11):

You will have to unpack it all the time

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

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:12):

uniqueness can be stated with one fewer pi btw

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:12):

you mean don't name witness?

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:12):

just say a = witness at the end

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:12):

sure

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:12):

the other witness

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:13):

oh, I see

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:13):

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:13):

er, I mean a = map something something

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:14):

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

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:15):

that was Reid's design

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:16):

I just want to avoid packing the data in too

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:16):

I see.

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:17):

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

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:18):

(a = x) iff p a

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:18):

right, with a abstracted

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:20):

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

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:21):

the definition might be gratuitous

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:21):

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

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:21):

I'll try with and without. :-)

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:21):

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

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:22):

it's ∃! with the witness free

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

view this post on Zulip Scott Morrison (Aug 12 2018 at 02:23):

okay, kids need lunch!

view this post on Zulip Mario Carneiro (Aug 12 2018 at 02:23):

I'm open to slick binder notations for that


Last updated: May 16 2021 at 05:21 UTC