Third symmetric product construction preserves set property in HoTT
The third symmetric product of a set is a set in HoTT
Logic in Computer Science
Summary
This paper shows that a mathematical construction called the third symmetric product, when applied to a set, results in another set within Homotopy Type Theory (HoTT). The authors build on earlier work that proved this for the second symmetric product and extend the method using a specific proof strategy known as encode-decode. Their work helps confirm how certain structured combinations of elements behave in this modern logical framework.
What this means in practice
- •For proof assistants developers: Support formal verification tools by confirming structural properties of complex type constructions in Homotopy Type Theory.
- •For programming language designers: Design type systems that reliably handle higher-order constructions by using this result to ensure type well-behavior in dependent types.
A theory result. No direct application yet.
Authors
Wojciech Paupa
Abstract
We deformalize an LLM-generated proof within the formalism of Homotopy Type Theory that an iterated pushout construction for $\operatorname{SP}^3(X)$ is a set whenever $X$ is a set. The proof expands on a similar proof by Buchholtz for $\operatorname{SP}^2(X)$, employing a similar encode-decode strategy and the same formal machinery.