Genuine pairs and the trouble with triples in homotopy type theory

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)

by Ulrik Buchholtz

Leave a Comment

Your email address will not be published. Required fields are marked *