Hakon Robbestad Gylterud ; Elisabeth Stenholm ; Niccolò Veltri - Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

lmcs:14325 - Logical Methods in Computer Science, June 29, 2026, Volume 22, Issue 2 - https://doi.org/10.46298/lmcs-22(2:35)2026
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type TheoryArticle

Authors: Håkon Robbestad Gylterud ; Elisabeth Stenholm ; Niccolò Veltri

Non-well-founded material sets have been modelled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) where equality is interpreted as the identity type. The first model satisfies Scott's Anti-Foundation Axiom (SAFA) and dualises the construction of iterative sets. The second model satisfies Aczel's Anti-Foundation Axiom (AFA), and is constructed by adaption of Aczel-Mendler's terminal coalgebra theorem to type theory, which requires propositional resizing. In an bid to extend coalgebraic theory and anti-foundation axioms to higher type levels, we formulate generalisations of AFA and SAFA, and construct a hierarchy of models which satisfies the SAFA generalisations. These generalisations build on the framework of Univalent Material Set Theory, previously developed by two of the authors. Since the model constructions are based on M-types, the paper also includes a characterisation of the identity type of M-types as indexed M-types. Our results are formalised in the proof-assistant Agda.


Volume: Volume 22, Issue 2
Published on: June 29, 2026
Accepted on: April 26, 2026
Submitted on: September 23, 2024
Keywords: Logic, Logic in Computer Science

Consultation statistics

This page has been seen 331 times.
This article's PDF has been downloaded 65 times.