Martin Escardo & Tom de Jong, June 2023.

Iterative multisets, iterative sets, and iterative ordinals.

For a blog-post style exposition of what is done here, see this post:
https://mathstodon.xyz/@MartinEscardo/110912588238494225

And earlier one is here:
https://mathstodon.xyz/@MartinEscardo/110753930251021051

Feel free to ask questions or make remarks there.

Notice also that the files here also include comments.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Iterative.index where

import Iterative.Multisets
import Iterative.Sets
import Iterative.Ordinals
import Iterative.Multisets-HFLO
import Iterative.Finite -- by Alice Laroche

\end{code}

Abstract. Some of the development of "Set-Theoretic and Type-Theoretic
Ordinals Coincide" is carried out but using Gylterud's construction of
the cumulative hierarchy đ as iterative sets, instead of
(axiomatically) working with the higher inductive presentation. The
type đ of hereditarily transitive sets is the type of iterative
ordinals and corresponds to đá”Êłá” in the original development
Ordinals.CumulativeHierarchy.lagda.

References.

[1] Peter Aczel. "The Type Theoretic Interpretation of Constructive
Set Theory". Studies in Logic and the Foundations of Mathematics,
Volume 96, 1978, Pages 55-66.
https://doi.org/10.1016/S0049-237X(08)71989-X

[2] Gerald Leversha. "Formal Systems for Constructive Mathematics".
PhD Thesis, 1976, The University of Manchester (United
Kingdom). Department of Pure and Applied Mathematics.

[3] HĂ„kon Gylterud. "Multisets in type theory".  Mathematical
Proceedings of the Cambridge Philosophical Society, Volume 169,
Issue 1, 2020, pp. 1-18. https://doi.org/10.1017/S0305004119000045

[4] H. R. Gylterud, "From multisets to sets in homotopy type theory".
The Journal of Symbolic Logic, vol. 83, no. 3, pp. 1132â1146,
2018. https://doi.org/10.1017/jsl.2017.84

[5] Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and
Chuangjie Xu. "Set-Theoretic and Type-Theoretic Ordinals
Coincide". To appear at LICS 2023, June 2023.
https://arxiv.org/abs/2301.10696

[6] Elisabeth Bonnevier, HĂ„kon Robbestad Gylterud, Daniel Gratzer, and
Anders MĂ¶rtberg, "The category of iterative sets in HoTT".
Workshop on Homotopy Type Theory/ Univalent Foundations
Vienna, Austria, April 22-23, 2023
https://hott-uf.github.io/2023/

[7] W. C. Powell. "Extending GĂ¶del's negative interpretation to ZF".
The Journal of Symbolic Logic, vol. 40, no. 2, pp. 221â229, 1975.
https://doi.org/10.2307/2271902