singleton

Stream: general

[Scott Morrison]

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

[Mario Carneiro]

do you need one?

[Mario Carneiro]

You can just assume both classes if you need

[Scott Morrison]

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

[Mario Carneiro]

for what?

[Scott Morrison]

universal properties

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

my current design just says these things separately

[Mario Carneiro]

You will have to unpack it all the time

[Scott Morrison]

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]

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

[Mario Carneiro]

uniqueness can be stated with one fewer pi btw

[Scott Morrison]

you mean don't name witness?

[Mario Carneiro]

just say a = witness at the end

[Scott Morrison]

sure

[Mario Carneiro]

the other witness

[Scott Morrison]

oh, I see

[Scott Morrison]

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

[Mario Carneiro]

er, I mean a = map something something

[Mario Carneiro]

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

[Scott Morrison]

that was Reid's design

[Scott Morrison]

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

[Mario Carneiro]

I just want to avoid packing the data in too

[Scott Morrison]

I see.

[Mario Carneiro]

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

[Scott Morrison]

(a = x) iff p a

[Mario Carneiro]

right, with a abstracted

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

the definition might be gratuitous

[Scott Morrison]

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

[Scott Morrison]

I'll try with and without. :-)

[Mario Carneiro]

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

[Mario Carneiro]

it's ∃! with the witness free

[Scott Morrison]

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

[Scott Morrison]

okay, kids need lunch!

[Mario Carneiro]

I'm open to slick binder notations for that