November 2: Elisabeth Stenholm, Non-wellfounded sets in Homotopy Type Theory

[Angiuli, Carlo]

The HoTTEST seminar continues this Thursday at a time that may be unusual to you depending on where you live: 11:30am EDT (UTC-4) = 15:30 UTC = 16:30 CET (UTC+1). In other words, Europeans should note that the US and Canada are still observing summer time this week.

This week, Elisabeth Stenholm is speaking about "Non-wellfounded sets in Homotopy Type Theory". The talk will be 60 minutes long, followed by up to 30 minutes of discussion. The abstract is below.

The Zoom link is https://zoom.us/j/994874377

Further information, including the list of upcoming speakers, and videos and slides from past talks, is available at:

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Carlo

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)

--

Elisabeth Stenholm

Non-wellfounded sets in Homotopy Type Theory

In 1978 Aczel gave a model of constructive set theory (CZF), which includes the axiom of foundation, in Martin-Löf type theory (MLTT) [1]. Then, in 1989, Lindström gave a different model, also in MLTT, of constructive set theory, but with foundation replaced by Aczel's anti-foundation axiom (AFA) [2]. Both of these models were setoid based. Starting from Aczel's 1978 model of wellfounded sets, Gylterud defined a subtype of the type Aczel used. This subtype is in fact the initial algebra of the (restricted) powerset functor, and thus also forms a model of constructive set theory, but one where equality is interpreted as the identity type [3].

In this work, we dualise the construction of Gylterud, to obtain a model of non-wellfounded sets, where equality is interpreted as the identity type, as opposed to Lindström's model. The expectation was that the dualised construction would be the terminal coalgebra of the powerset functor, in which case it would be a model of CZF⁻ together with AFA. It turns out, however, that it is not the terminal coalgebra of the powerset functor. But all is not lost, for it is a fixed point of the functor, and in addition, it is terminal with respect to embeddings. This gives us instead a model of CZF⁻ together with Scott's anti-foundation axiom.

[1]: P. Aczel, “The Type Theoretic Interpretation of Constructive Set Theory,” in Studies in Logic and the Foundations of Mathematics, vol. 96, A. Macintyre, L. Pacholski, and J. Paris, Eds., in Logic Colloquium ’77, vol. 96. , Elsevier, 1978, pp. 55–66. doi: 10.1016/S0049-237X(08)71989-X.

[2]: I. Lindström, “A Construction of Non-Well-Founded Sets within Martin-Löf’s Type Theory,” The Journal of Symbolic Logic, vol. 54, no. 1, pp. 57–64, 1989, doi: 10.2307/2275015.

[3]: H. R. Gylterud, “From Multisets to Sets in Homotopy Type Theory,” The Journal of Symbolic Logic, vol. 83, no. 3, pp. 1132–1146, Sep. 2018, doi: 10.1017/jsl.2017.84.