Tags: containers References. Notions of Anonymous Existence in Martin-Lof Type Theory (Kraus, Escardó, Coquand, Altenkirch) Datatypes with Symmetries in Homotopy Type Theory (Joram, 2026)