Zulip Chat Archive

Stream: general

Topic: Name for a pair of distinct points?

Kyle Miller (Jan 29 2022 at 18:59):

There is a PR introducing a type for a pair of distinct points (#11648), and the proposed name seems fine, but I just wanted to see if the creativity of the community might turn up some more ideas.

Some ideas so far:

  • two_pointing since it's two points
  • dpair for "distinct pair" (though it might be confused for a "dependent pair")
  • conf2 since it's the configuration space for two points, and it could relate to a conf similar to sym2 and sym.

Kyle Miller (Jan 29 2022 at 18:59):

/poll Name for pair of distinct terms?
two_pointing
dpair
conf2

Yaël Dillies (Jan 29 2022 at 19:00):

The reference I'm following

Adam Topaz (Jan 29 2022 at 19:16):

Are you going to formalize the theorem of Freyd in that link?

Adam Topaz (Jan 29 2022 at 19:18):

If so, I might consider changing the definition to use maps from docs#pbool or docs#category_theory.limits.walking_pair (which are further injective if you want the points to be distinct)

Reid Barton (Jan 29 2022 at 19:19):

Maybe something like alt2 or choose2?

Bhavik Mehta (Jan 29 2022 at 19:20):

Also cf http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/terminal%20coalgebra%20for%20an%20endofunctor#UnitIntervalm where the category is more restricted

Yaël Dillies (Jan 29 2022 at 19:23):

Adam Topaz said:

Are you going to formalize the theorem of Freyd in that link?

Trying to!

Adam Topaz (Jan 29 2022 at 19:29):

If you want another fun categorical-ish analysis-ish construction, you can construct the Lebesgue integral as well, e.g.
https://www.maths.ed.ac.uk/~tl/cambridge_ct14/cambridge_ct14_talk.pdf

Yaël Dillies (Jan 29 2022 at 19:30):

Please stop nerdsniping me, people :rofl:

Yaël Dillies (Jan 29 2022 at 19:30):

I'm already formalizing a big chunk of lattice representation theory by fault of Bhavik.

Bhavik Mehta (Jan 29 2022 at 19:55):

Adam Topaz said:

If you want another fun categorical-ish analysis-ish construction, you can construct the Lebesgue integral as well, e.g.
https://www.maths.ed.ac.uk/~tl/cambridge_ct14/cambridge_ct14_talk.pdf

Yeah I love this construction!

Yaël Dillies (Feb 02 2022 at 08:52):

I might consider changing the definition to use maps from docs#pbool or docs#category_theory.limits.walking_pair (which are further injective if you want the points to be distinct)

What's the advantage of that?

Last updated: Dec 20 2023 at 11:08 UTC