Ulrik Buchholtz
Department of Mathematics, Technische Universität Darmstadt
What is an unordered pair of groups, or of categories, or of types? In homotopy type theory, the naive answer is a pair of a two-element type K and a function from K to whatever we’re taking pairs of. This definition has the downside that the type of unordered pairs in a set is no longer a set. For example, the unordered pairs in the unit type is the infinite dimensional real projective space.
I’ll explain how to define genuine unordered pairs using ideas from equivariant homotopy theory and prove that the genuine unordered pairs in a set is still a set. Then I’ll define genuine unordered triples and relate my troubles with them. Finally, I’ll explain why genuine multisets of arbitrary cardinality are really difficult.
Chair: Nicolai Kraus
Event Timeslots (1)
Monday
-
by Ulrik Buchholtz
Leave a Comment