PreprintCC BY 4.0arXiv
The third symmetric product of a set is a set in HoTT
Abstract
We deformalize an LLM-generated proof within the formalism of Homotopy Type Theory that an iterated pushout construction for SP3(X) is a set whenever X is a set. The proof expands on a similar proof by Buchholtz for SP2(X), employing a similar encode-decode strategy and the same formal machinery.
Related
- The Comon Rank Gap of a Third-Order Symmetric Tensor Can Exceed One
- Upper Bounds on the Strassen CP Rank Gap and Symmetric Rank Gap of Third-Order Tensors
- Upper Bounds on the Comon Rank Gap of Real Symmetric Third-Order Tensors
- Product structures and decompositions of ℤ2×ℤ2-symmetric spaces
- Zeros in The Character Table of The Wreath Product of The Symmetric Group
BibTeX
@misc{paupa2026third,
title = {{The third symmetric product of a set is a set in HoTT}},
author = {Wojciech Paupa},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.32816},
eprint = {2609.32816},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.32816},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - The third symmetric product of a set is a set in HoTT
AU - Wojciech Paupa
PY - 2026
DA - 2026/09/26
PB - arXiv
DO - 10.48550/arxiv.2609.32816
UR - https://arxiv.org/abs/2609.32816
AB - We deformalize an LLM-generated proof within the formalism of Homotopy Type Theory that an iterated pushout construction for SP^3(X) is a set whenever X is a set. The proof expands on a similar proof by Buchholtz for SP^2(X), employing a similar encode-decode strategy and the same formal machinery.
ER -