1 Introduction

1.1 Why three foundations

The phrase “foundations of mathematics” is in 2026 plural by both fact and conviction. A working mathematician encountering structures up to isomorphism (vector spaces, groups, topological spaces, schemes, $\infty$ -categories) needs an underlying logic that respects the equivalence principle: isomorphic objects share their mathematical content. Classical Zermelo–Fraenkel set theory with Choice (ZFC), the de facto standard since the 1920s, supports this principle only by a sociological convention — the convention to prove only structural properties — but the formalism itself permits non-structural predicates such as “ $\emptyset \in 7$ ” (a sentence whose truth value depends on Kuratowski’s particular encoding of pairs).

The three foundational alternatives we examine in this paper each respond to that inadequacy in a different way:

ETCS (Lawvere 1964) replaces the universe of sets-with-membership by a category of sets-with-functions, axiomatised structurally as a well-pointed topos with a natural numbers object (NNO) and a choice operator;
IZF (Friedman 1973, Myhill, Aczel) keeps the membership predicate but moves to intuitionistic logic, accepting full Separation, Replacement, Powerset, and Infinity while rejecting Excluded Middle and Choice; structuralism is enforced indirectly via realisability and topos-valued models;
FOLDS (Makkai 1995) re-engineers the underlying logic so that only isomorphism-invariant predicates are expressible; the equivalence principle is a metatheorem of the syntax rather than a moral imperative.

Each is motivated by the search for a logical environment in which equivalence-invariance is built in. Each succeeds for a different reason. And each has a precise relationship to HoTT, the foundation introduced by Voevodsky (2010) in which equivalence-invariance is proven as a theorem (the Univalence Axiom and its corollary, the Structure Identity Principle).

1.2 Structural vs material set theory

Following Awodey , McLarty , and Shulman, we use the following terminology.

Definition 1 (Material set theory). A set theory is material if its primitive non-logical relation is membership $\in$ , with sets identified by extensionality (two sets are equal iff they have the same elements), and where the universe of discourse is a single class of all sets ranging over a $\in$ -tree.

Definition 2 (Structural set theory). A set theory is structural if its primitive notions are sets and functions (equivalently: the objects and morphisms of a category), with sets identified up to unique isomorphism, and where membership is a derived notion ( $x \in A$ means “ $x : 1 \to A$ is a global element”).

ZFC and IZF are material; ETCS and Lawvere’s ETCC (Elementary Theory of the Category of Categories) are structural; FOLDS is neither — it is a logic, applicable to either flavour, but designed so that even when interpreted materially, only structural sentences are syntactically expressible. HoTT is structural (in fact higher-structural: types are identified up to higher equivalence).

1.3 The univalence boundary

The methodological question that organises this paper is:

Of the principles, axioms, and metatheorems that distinguish ETCS, IZF, and FOLDS, which become theorems in HoTT (with univalence) and which do not?

A principle that becomes a theorem under HoTT+UA but not under HoTT alone (i.e. the $(- 1)$ -truncated fragment, or the propositions-as-subsingletons fragment) lies on the far side of the univalence boundary: it is conditional on univalence. A principle that holds without univalence lies on the near side: it is unconditional.

We will argue in 7 that the boundary cuts as follows:

Principle	ETCS	IZF	FOLDS	UA in HoTT?
NNO existence	axiom	thm	expr.	no
Function ext.	thm	thm	axiom	implied by UA $^{*}$
Prop. ext.	thm	thm	expr.	no
SIP	meta	—	meta	yes
FOLDS-eq. $=$ id	—	—	meta	yes
EM	axiom	reject	expr.	indep.
Choice	AC	reject	expr.	indep. (PEM+AC)
Replacement	axiom	axiom	—	thm (small)
Powerset	derived	axiom	—	impred. $Ω$

$^{*}$ Function extensionality (FE) is a theorem of HoTT + UA (Voevodsky) but is independent of MLTT alone; see 5 and 43 for the precise nuance.

1.4 Outline

2 states the eight-axiom presentation of ETCS, proves the elementary consequences (NNO, products, exponentials), and recalls McLarty’s bi-interpretation theorem with Bounded Zermelo + Replacement. 3 presents IZF, contrasts it with CZF and ZFC, and discusses the realisability and topos-valued models that connect IZF to HoTT. 4 develops Makkai’s signature theory, defines FOLDS-equivalence, and proves Makkai’s Invariance Theorem (every FOLDS-formula is invariant under FOLDS-equivalence). 5 reframes HoTT as the unifying framework: which structural principles become theorems, which need univalence. 6 surveys models: ETCS in toposes, FOLDS in fibrations, HoTT in $(\infty, 1)$ -toposes. 7 formally analyses the univalence boundary. 8 states three open problems. 12 concludes.

2 ETCS: The Elementary Theory of the Category of Sets

2.1 The eight axioms

ETCS is a first-order theory in the language of categories (objects, morphisms, composition, identity). The eight axioms below follow Lawvere’s original 1964 PNAS paper as updated by Lawvere–Rosebrugh and McLarty .

Definition 3 (ETCS axioms). A category $S$ models ETCS iff it satisfies:

$S$ has finite limits (terminal object $1$ , binary products $A \times B$ , equalisers).
$S$ is Cartesian closed: for any objects $A, B$ there is an exponential $B^{A}$ with evaluation $ev : B^{A} \times A \to B$ enjoying the universal property of $λ$ -abstraction.
$S$ has a subobject classifier: an object $Ω$ with a morphism $⊤ : 1 \to Ω$ such that every monomorphism $m : A ↪ B$ arises as the pullback of $⊤$ along a unique characteristic morphism $χ_{m} : B \to Ω$ .
$S$ has a natural numbers object: an object $N$ with maps $0 : 1 \to N$ and $s : N \to N$ such that for every $(X, x_{0} : 1 \to X, f : X \to X)$ there is a unique morphism $h : N \to X$ with $h \circ 0 = x_{0}$ and $h \circ s = f \circ h$ .
$S$ is well-pointed: if $f, g : A \to B$ are distinct morphisms, then there exists $x : 1 \to A$ with $f \circ x \neq = g \circ x$ .
(Axiom of choice) Every epimorphism $e : A ↠ B$ has a section $s : B \to A$ with $e \circ s = id_{B}$ .
(Two-valuedness; derivable from A5–A6 and A8) Any morphism $f : 1 \to Ω$ equals either $⊤$ or $⊥$ , where $⊥$ is the unique map factoring through the initial object. Listed for didactic completeness; see the remark below.
(Non-degeneracy) $0 \neq ≅ 1$ (the initial object is not isomorphic to the terminal).

Remark 4. A1+A2+A3 alone make $S$ an elementary topos in the sense of Lawvere–Tierney. Adding A4 gives a topos with NNO. Adding A5–A8 specialises to “topos behaving like classical sets”. Equivalently, an ETCS model is a well-pointed topos with NNO and choice. Two-valuedness (A7) follows from well-pointedness plus non-degeneracy when AC is present.

2.2 Elementary consequences

Proposition 5 (Function extensionality in ETCS). For $f, g : A \to B$ , if $\forall x : 1 \to A, f \circ x = g \circ x$ , then $f = g$ .

Proof. This is the contrapositive of well-pointedness (A5). ◻

Proposition 6 (Power objects). $S$ has power objects $P (A) := Ω^{A}$ , with the standard adjunction $Sub (B \times A) ≅ Hom (B, P (A))$ .

Proof. Combine A2 and A3: $P (A) = Ω^{A}$ classifies subobjects of any product $B \times A$ via $χ : B \times A \to Ω$ uncurried as $χ : B \to Ω^{A}$ . ◻

Theorem 7 (McLarty’s bi-interpretation theorem). ETCS and Bounded Zermelo set theory plus Replacement (BZ+R) are bi-interpretable: each can interpret the other, and the interpretations compose to the identity up to definable isomorphism.

Sketch. Given a model of ETCS, define a class of trees as well-founded extensional quotients of pointed graphs internalised by the NNO and powerset; this gives a model of $BZ + R$ . Conversely, given a model $V$ of $BZ + R$ , define $S_{V}$ to be the category of sets and functions inside $V$ ; one verifies A1–A8 directly. Composition produces models that are equivalent in the appropriate 2-categorical sense. Full proof in McLarty ; we return to it in 6. ◻

2.3 Encoding-free arithmetic

ETCS resolves Benacerraf’s identification problem (Paper II of our series) by making ordered pair a primitive operation (the universal property of products) rather than the Kuratowski encoding $⟨ a, b ⟩ = {{a}, {a, b}}$ . Junk theorems such as “ $3 \in 7$ ” (vacuously true under von Neumann ordinals: $3 = {0, 1, 2}$ and $7 = {0, \dots, 6}$ ) are not formulable in the ETCS language: $3 : 1 \to N$ is a global element, $7 : 1 \to N$ likewise, and there is no membership predicate between them.

Example 8. $N \times N$ in ETCS is the categorical product of $N$ with itself, characterised by the universal property; whether one uses Kuratowski pairs, Wiener pairs, or any other internal encoding to prove existence inside $BZ + R$ is irrelevant to the structural object so produced.

2.4 Worked example: arithmetic via the recursor

We illustrate how arithmetic is developed structurally in ETCS using only the universal property of the NNO. Given the NNO $(N, 0, s)$ , define addition $+ : N \times N \to N$ as follows.

Definition 9 (Addition in ETCS). The addition map $+ : N \times N \to N$ is the unique morphism satisfying:

$+ \circ ⟨ 0_{N}, id_{N} ⟩ = id_{N}$ (left zero), and
$+ \circ (s \times id_{N}) = s \circ +$ (left successor).

Proposition 10 (Existence of addition). There exists a unique morphism $+$ as in 9.

Proof. Apply the NNO universal property to the pointed endomorphism $(N^{N}, id_{N} : 1 \to N^{N}, s \circ ev : N^{N} \to N^{N})$ where the basepoint is the constant function $id_{N}$ and the endomap is post-composition with $s$ . This yields a unique $+ : N \to N^{N}$ , which uncurries to $+ : N \times N \to N$ satisfying both equations. ◻

Example 11 (Multiplication and exponentiation). Multiplication $\cdot$ is defined by the same recursion technique with $+$ in place of $s$ : $\cdot \circ ⟨ 0, id ⟩ = 0$ , $\cdot \circ (s \times id) = + \circ ⟨ id, \cdot ⟩$ . Exponentiation $↑$ similarly: $↑ \circ ⟨ 0, id ⟩ = 1$ , $↑ \circ (s \times id) = \cdot \circ ⟨ id, ↑ ⟩$ .

2.5 ETCS without choice

Removing A6 (choice) yields what is sometimes called ETCS-AC or Topos+NNO+WP (well-pointed topos with NNO). This system is consistent with both EM and $\neg$ EM in non-trivial models. McLarty’s bi-interpretation theorem extends to: ETCS-AC is bi-interpretable with $BZ + R$ -AC. The constructive variant of ETCS (replace A5 well-pointedness by Kock’s notion of subterminal-pointedness, drop A6 and A7) is bi-interpretable with appropriate fragments of IZF. We will see in 7 that AC is on the straddling side of the univalence boundary.

2.6 Comparison with Awodey–Forssell categorical structuralism

Awodey introduces a refined notion of structural foundation: a formal system whose models satisfy isomorphism-invariance internally. ETCS satisfies this in the 1-categorical sense; its only non-invariant data are the choices of products, exponentials, etc., which are determined up to (unique) isomorphism. The “isomorphism-invariance” guarantee in ETCS, however, is not a theorem of ETCS about itself; it is a metatheorem (any two products are isomorphic; any property expressible in the categorical language is invariant under isomorphism). To make the guarantee internal, one needs HoTT.

3 IZF: Intuitionistic Zermelo–Fraenkel

3.1 Axioms

IZF (Friedman 1973, Myhill, surveyed in ) is the system over intuitionistic first-order logic with equality and a binary predicate $\in$ , having the following axioms.

Definition 12 (IZF axioms). We adopt the formulation of IZF using the strong Collection schema (rather than the weaker Replacement schema); under intuitionistic logic, Collection is strictly stronger than Replacement, so this choice is significant. The remark following the definition discusses the difference.

(Extensionality) $\forall x \forall y [(\forall z (z \in x \Leftrightarrow z \in y)) \Rightarrow x = y]$ .
(Empty set) $\exists x \forall y (y \in / x)$ .
(Pairing) $\forall x \forall y \exists z \forall w (w \in z \Leftrightarrow w = x \lor w = y)$ .
(Union) $\forall x \exists y \forall z (z \in y \Leftrightarrow \exists w \in x . z \in w)$ .
(Infinity) $\exists ω (\emptyset \in ω \land \forall x \in ω . x \cup {x} \in ω)$ .
(Full Separation) For every formula $φ (z)$ , $\forall x \exists y \forall z (z \in y \Leftrightarrow z \in x \land φ (z))$ .
(Powerset) $\forall x \exists y \forall z (z \in y \Leftrightarrow z \subseteq x)$ .
(Collection) For every formula $φ (x, y)$ , if $\forall x \in a . \exists y . φ (x, y)$ , then $\exists b . \forall x \in a . \exists y \in b . φ (x, y)$ .
( $\in$ -Induction) For every $φ$ , $[\forall x ((\forall y \in x . φ (y)) \Rightarrow φ (x))] \Rightarrow \forall x . φ (x)$ .

The underlying logic is intuitionistic; Excluded Middle (EM) and Choice (AC) are not assumed.

Remark 13. A standard simplification replaces (I8) Collection by the weaker Replacement schema. Friedman’s IZF uses Collection because, under intuitionistic logic, Collection is strictly stronger than Replacement: Replacement requires uniqueness of the witness, while Collection requires only existence. In classical logic, Collection is derivable from Replacement using EM; in IZF this implication fails.

3.2 IZF and ZFC: strength and divergence

Theorem 14 (Friedman ). $ZF = IZF + EM$ , where $EM$ is the schema $φ \lor \neg φ$ over the IZF language. Consequently, IZF and ZF are equiconsistent.

Sketch. Forward direction: $IZF \subseteq ZF$ definitionally, since classical logic includes intuitionistic logic and EM gives the rest. Reverse: every ZF axiom is in IZF except those needing EM in their classical forms, but Separation in IZF is full so the classical schema follows. The equiconsistency: any model of ZF is a model of IZF+EM; any model of IZF gives a Heyting-valued model that, under EM, becomes a model of ZF. Friedman’s original proof uses double-negation translations. ◻

Remark 15 (CZF vs IZF). Aczel’s CZF (Constructive Zermelo–Fraenkel) replaces Powerset by Subset Collection (or its equivalent Fullness axiom) and Full Separation by Restricted Separation (where $φ$ is bounded). CZF is significantly weaker than IZF: $CZF ⊊ IZF$ , and CZF is interpretable in Martin-Löf type theory via Aczel’s sets-in-types translation. IZF is impredicative (Powerset and Full Separation), which puts it in tension with the predicative spirit of MLTT and HoTT.

3.3 IZF, realisability, and HoTT

Definition 16 (Realisability model). A realisability model of IZF is a category-theoretic structure $(V, ⊩)$ where $V$ is a class hierarchy and $⊩$ is a forcing relation specified by terms of an underlying calculus (e.g. untyped $λ$ -calculus, PCAs, or partial combinatory algebras) such that the IZF axioms are forced.

The connection to HoTT runs through the topos-theoretic interpretation. Hyland’s effective topos $E f f$ provides a realisability model in which IZF holds (via Full Separation, Collection, and Powerset using the lifted $Ω$ ). Inside $E f f$ , the internal language is intuitionistic higher-order logic, which embeds into HoTT once we resolve coherence at higher levels. Shulman’s results show every Grothendieck $(\infty, 1)$ -topos models HoTT; specialising to localic $(\infty, 1)$ -toposes gives realisability models of HoTT compatible with IZF.

Theorem 17 (Awodey–Warren propositions-as-types for IZF). The $(- 1)$ -truncated fragment of HoTT (i.e. HoTT restricted to mere propositions) satisfies the IZF axioms in the following sense: there is an interpretation $[[\cdot]]$ of IZF formulas into $(- 1)$ -truncated types such that $IZF ⊢ φ$ implies $HoTT ⊢ [[φ]]$ provided we add the propositional resizing axiom and the Mahlo–Universe axiom needed for Replacement.

Sketch. Each IZF set is interpreted as a well-founded $V$ -structure (Aczel’s V) inside HoTT. Full Separation translates to subtype formation under propositional resizing. Powerset translates to $A \to hProp$ . Collection requires the Mahlo-style closure on the universe. See HoTT Book §10.5 for details. ◻

3.4 Diaconescu’s theorem and IZF

Theorem 18 (Diaconescu 1975). In any topos satisfying the axiom of choice, the law of excluded middle holds. In particular, $IZF + AC$ proves $EM$ .

Sketch. Given a proposition $P$ , consider the set $A = {x \in {0, 1} : x = 0 \lor P}$ and $B = {x \in {0, 1} : x = 1 \lor P}$ . By Pairing both are sets, and their union is ${0, 1}$ . AC gives a choice function on the family of these two non-empty sets, producing $a \in A, b \in B$ . Now either $a = b$ , in which case $P$ holds (decidably), or $a \neq = b$ , in which case $\neg P$ holds. Either way $P \lor \neg P$ . ◻

Corollary 19. $IZF + AC$ is equivalent to $ZFC$ . Hence the constructive content of IZF is genuinely tied to the absence of AC.

3.5 Aczel’s CZF and predicativity

A subtle but important alternative to IZF is Aczel’s CZF (Constructive Zermelo–Fraenkel), formulated in . CZF differs from IZF in two crucial ways:

Restricted Separation: the Separation schema is restricted to bounded formulas (formulas all of whose quantifiers are restricted to a set).
Subset Collection (Fullness): replaces Powerset.

The result is a predicative theory, in the sense of Feferman: CZF can be interpreted in Martin-Löf type theory (the sets-in-types interpretation ), and hence has the proof-theoretic strength of MLTT plus a single Mahlo-like inaccessible.

Remark 20. The IZF/CZF distinction matters for the comparison with HoTT: CZF is closer to HoTT in spirit (predicative, type-theoretic), whereas IZF is closer to ZF in spirit (impredicative, set-theoretic). Both can be interpreted in HoTT, but CZF more naturally.

4 FOLDS: First-Order Logic with Dependent Sorts

4.1 Dependent signatures

Definition 21 (FOLDS signature, after Makkai ). A FOLDS signature is a small category $L$ that is:

One-way: there are no non-trivial endomorphisms or antiparallel parallel arrows.
Direct: every object has finitely many objects above it, and the order on “levels” (height in the underlying graph) is well-founded.
Equipped with a designated set of relation symbols: distinguished objects intended to be interpreted as truth-valued (i.e. subterminal).

A kind is a non-relation object; a relation is one of the designated objects.

Example 22 (FOLDS signature for categories). The signature $L_{Cat}$ has:

Kind $O$ (objects).
Kind $A$ (arrows), with two morphisms $s, t : A \to O$ (source, target). The dependency $A \to O \times O$ records that an arrow has a source and target object.
Relation $T (g, h, k)$ on composable triples $(g, h, k : A)$ (where $t (g) = s (h)$ and the common boundary types match) expressing “ $k$ is the composite $h \circ g$ ”. This relation captures composition data without committing to a function symbol.
Relation $I (f)$ on $A$ expressing “ $f$ is an identity arrow”. We list this relation explicitly because in FOLDS one cannot pick out identity arrows by equality with a chosen constant; instead, identities are designated via this relation, which is required to satisfy the laws $\forall f . I (f) \to T (f, g, g)$ and $T (g, f, g)$ for parallel $g$ .
Relation $E (f, g)$ on parallel arrows expressing arrow-equality. In FOLDS the equality predicate on each kind is itself a designated relation symbol, not a primitive of the logic; this is what guarantees isomorphism-invariance of FOLDS sentences.

A model is a category in the usual sense, where the three relations $T, I, E$ have distinct and complementary roles: $T$ records composition data, $I$ singles out the identity arrows, and $E$ provides arrow-equality. Together they suffice to express the category axioms (associativity, unit laws, identity laws) as FOLDS sentences.

4.2 FOLDS-equivalence

Definition 23 (FOLDS-equivalence, Makkai ). Two $L$ -structures $M, N$ are FOLDS-equivalent (written $M ≃_{F} N$ ) iff there exists a span of $L$ -structure homomorphisms $M p P q N$ where both $p$ and $q$ are very surjective: surjective on every kind, and on every relation symbol $R$ , the induced map $R^{P} \to R^{M} \times_{(kinds)} \dots$ is surjective.

Remark 24. For the signature $L_{Cat}$ , $M ≃_{F} N$ coincides with the classical notion of equivalence of categories $M ≃ N$ (essentially surjective and fully faithful). For higher signatures (e.g. bicategories), FOLDS-equivalence correctly generalises bi-equivalence; for $n$ -categories, $n$ -equivalence; and so on for $\infty$ -categorical signatures.

4.3 Makkai’s Invariance Theorem

Theorem 25 (Makkai’s Invariance Theorem ). For every FOLDS signature $L$ and every FOLDS sentence $φ$ in $L (L)$ , and any two $L$ -structures $M, N$ : $M ≃_{F} N ⟹ (M ⊨ φ \Leftrightarrow N ⊨ φ) .$

Sketch. By induction on $φ$ . Atomic formulas are preserved by very surjective homomorphisms, both ways, by the surjectivity on relations. Connectives and the unique quantifier $\exists x : K$ (where $K$ is a kind) preserve preservation under very surjective spans because every element on each kind in $M$ (resp. $N$ ) is hit by some element of $P$ . Full induction is given in ; an alternative homotopy-theoretic proof appears in Henry’s work on the Isomorphism Property. ◻

Corollary 26. No FOLDS sentence can distinguish two equivalent categories. In particular, the predicate “ $X$ is the $\in$ -rank-zero element of the universe” is not expressible in any FOLDS signature for ZF.

4.4 FOLDS as a fragment of dependent type theory

Palmgren showed FOLDS embeds into intensional Martin-Löf type theory. The dependence in a FOLDS signature is captured by the dependence of types in MLTT; relations become $(- 1)$ -types (mere propositions).

Theorem 27 (Palmgren ). There is a faithful translation $T$ from FOLDS signatures over a category $L$ to dependent type theories with explicit substitutions $CwF (L)$ , such that:

Every FOLDS structure $M$ on $L$ corresponds to a model of $T (L)$ .
FOLDS-equivalence corresponds to equivalence of models of $T (L)$ .

4.5 Worked FOLDS proofs

Example 28 (Categorical equivalence is FOLDS-equivalence). Take $L = L_{Cat}$ and let $F : M \to N$ be a functor. Construct the cograph (mapping cylinder) $C (F)$ : objects are $Ob (M) ⊔ Ob (N)$ , with hom-sets given by $C (F) (x, y) := ⎩ ⎨ ⎧ M (x, y) N (x, y) N (F (x), y) \emptyset x, y \in Ob (M) x, y \in Ob (N) x \in M, y \in N otherwise.$ Then both inclusions $M ↪ C (F)$ and $N ↪ C (F)$ are homomorphisms of $L_{Cat}$ -structures. The inclusion of $M$ is very surjective iff $F$ is essentially surjective and full. The inclusion of $N$ is very surjective iff $F$ is faithful. Combining, $F$ is an equivalence iff there is a zigzag of cograph cospans connecting $M$ and $N$ via very surjective maps — i.e. $M ≃_{F} N$ in the FOLDS sense.

Proposition 29 (Skeletality is not FOLDS-expressible). The predicate “ $C$ is a skeletal category” (every object is the unique representative of its isomorphism class) is not expressible by any FOLDS sentence.

Proof. Suppose $φ$ is a FOLDS sentence in $L_{Cat}$ that holds in $C$ iff $C$ is skeletal. Take a non-skeletal $C_{0}$ and a skeleton $C_{1} ↪ C_{0}$ . The inclusion is an equivalence (essentially surjective and fully faithful), hence the cograph construction yields $C_{0} ≃_{F} C_{1}$ . By Makkai’s invariance theorem (25), $C_{0} ⊨ φ \Leftrightarrow C_{1} ⊨ φ$ . But $C_{1}$ is skeletal and $C_{0}$ is not, so $φ$ cannot distinguish them. Contradiction. ◻

Remark 30. 29 is paradigmatic: any predicate referring to specific representatives of equivalence classes (rather than equivalence-classes themselves) fails to be FOLDS-expressible. This is the syntactic mechanism by which FOLDS enforces the equivalence principle: “junk” predicates cannot even be stated.

4.6 Higher signatures: bicategories and $\infty$ -categories

The signature $L_{Cat}$ for ordinary categories generalises naturally to higher signatures:

$L_{Bicat}$ : kinds $O$ , $A$ , $C$ (cells), with $s, t : A \to O$ , $s, t : C \to A$ , and relations for vertical/horizontal composition, identities, and 2-cell equality. FOLDS-equivalence on $L_{Bicat}$ is bi-equivalence of bicategories.
$L_{(\infty, 1)}$ : an infinite tower of kinds $A_{n}$ for $n$ -cells, with boundary maps and a single “hcomp” relation per dimension. FOLDS-equivalence corresponds to Joyal-style $\infty$ -equivalence (DK-equivalence).

Szumiło extends this to a hierarchy of $n$ -FOLDS logics whose syntax converges to the syntax of HoTT.

5 HoTT: The unifying frame

5.1 Univalence as the equivalence-invariance axiom

Univalence (Voevodsky 2010, HoTT Book §2.10) is the axiom: $ua : (A ≃ B) \sim (A =_{U} B)$ saying that the canonical map “ $idtoeqv$ ” from identifications between types to equivalences between them is itself an equivalence. In short: equivalent types are identical. The Structure Identity Principle (SIP) generalises this from raw types to typed structures: equivalent structures are identical.

5.2 Which structural principles become theorems

The following table summarises what passes from axiom-status (in ETCS, IZF, or as a metatheorem in FOLDS) to theorem-status in HoTT (Section 1 column reproduced for convenience):

NNO is a theorem in HoTT — the inductive type $N$ is built into the type theory and contractibility of the type of NNO structures is provable (Paper V Theorem 4.4 of our series).
Function extensionality is a theorem in HoTT given univalence: Voevodsky’s proof shows $UA \Rightarrow FE$ .
Propositional extensionality is a theorem in HoTT given univalence, restricted to mere propositions.
Structure Identity Principle is a theorem in HoTT given univalence (see Paper VI Theorems 10.3–10.4 of our series).
FOLDS-equivalence-implies-identity is a theorem in HoTT given univalence (this is the Univalence Principle of Ahrens–North–Shulman–Tsementzis 2019).

We now make this last statement precise.

5.3 The Univalence Principle (ANST 2019)

Theorem 31 (Univalence Principle, ANST ). For any FOLDS signature $L$ and any two $L$ -structures $M, N$ in HoTT, $(M ≃_{F} N) ≃ (M =_{Str (L)} N) .$ That is, FOLDS-equivalence is identification in the type of $L$ -structures.

Sketch. The dependent-sort structure of $L$ is encoded as a Reedy diagram of types in HoTT. Each relation symbol becomes a $(- 1)$ -truncated type, each kind a type of the appropriate truncation level. By induction on the Reedy structure, FOLDS-equivalence unfolds into the data of an equivalence at each level, which by repeated application of the Structure Identity Principle (a consequence of univalence) gives an identification. The full proof requires careful management of the level structure of $L$ and the Reedy fibrant replacement; see ANST. ◻

Remark 32. 31 subsumes Makkai’s Invariance Theorem: indeed if $M ≃_{F} N$ then $M = N$ in HoTT, hence any predicate is preserved (by transport along the identification). But 31 is stronger: it gives an equivalence, not just an implication. The strength comes from univalence.

5.4 Internalising ETCS in HoTT

We now sketch how ETCS is recovered as a theorem inside HoTT, given univalence and sufficient choice/EM where needed.

Theorem 33 (Sets in HoTT form a model of ETCS-AC). Within HoTT, define $Set$ to be the type of $0$ -truncated types (sets in the sense of HoTT §3.1): $Set := Σ_{X : U} isSet (X) .$ Then $Set$ , with the obvious morphism structure (functions between sets) and identity and composition, is an elementary topos with NNO. Adding propositional resizing and the (provably independent) axioms EM and AC produces a model of ETCS.

Sketch. Finite limits: Sigma-types and product types are sets when their components are sets; equalisers are $Σ_{x : A} (f (x) = g (x))$ , also a set. Cartesian closure: function types $A \to B$ are sets when $B$ is a set (by FE). Subobject classifier: $Ω := hProp$ , the type of mere propositions; truth is the standard map. NNO: the inductive type $N$ . Well-pointedness: function extensionality. AC: axiom (independent in HoTT). Two-valuedness: requires EM (axiom). Non-degeneracy: $0 \neq ≃ 1$ holds in any non-trivial model. ◻

5.5 Internalising IZF in HoTT

Aczel’s $V$ -construction inside HoTT:

Definition 34 (The HoTT cumulative hierarchy). Define the higher inductive type $V$ with:

Constructor $set : (A : U) \to (A \to V) \to V$ .
Path constructor: extensionality, $set (A, f) =_{V} set (B, g)$ iff there is a bisimulation between the trees $(A, f)$ and $(B, g)$ .
$0$ -truncation.

Theorem 35 (HoTT Book §10.5). $V$ is a model of IZF in the following sense: every IZF axiom (Extensionality, Pairing, Union, Powerset, Infinity, Collection, Full Separation, $\in$ -Induction) translates to a provable HoTT statement about $V$ , given propositional resizing.

5.6 Internalising FOLDS in HoTT via the Univalence Principle

The key observation: FOLDS signatures, qua small categories, are themselves objects of HoTT. FOLDS-structures qua functors are objects of HoTT. The Univalence Principle (31) is the statement that the type of $L$ -structures has the expected identity type. So FOLDS is not just representable in HoTT; the FOLDS metatheorem (Makkai’s Invariance Theorem) becomes an internal HoTT theorem.

6 Models

6.1 ETCS in toposes

A model of ETCS is a well-pointed elementary topos with NNO and AC. The category $Set$ in ZFC is the prototype. Other models include:

$Set_{ZF + AC}$ : classical sets in ZF + AC.
$Set_{IZF + AC}$ : intuitionistic sets in IZF + AC (where AC implies EM via Diaconescu, hence equivalent to ZFC).
$FinSet$ : finite sets satisfy A1–A6, fail A4 (no NNO), so not ETCS.
Forcing extensions of $Set$ : ETCS+CH and ETCS+ $\neg$ CH.

6.2 IZF and topos-valued models

Friedman–Aczel construction: in any cocomplete elementary topos $E$ with NNO and a Mahlo-style universe object, the internal $V$ -structure (the “cumulative hierarchy” inside $E$ ) gives a model of IZF.

Theorem 36 (Friedman–Aczel–Joyal). The internal hierarchy $V_{E}$ in a cocomplete topos with universe object satisfies all axioms of IZF.

The proof reduces each axiom (Extensionality, Pairing, Union, Powerset, Infinity, Collection, Full Separation, $\in$ -Induction) to a property of $E$ that holds by definition of cocomplete elementary topos with universe.

6.3 FOLDS in fibrations

A FOLDS signature $L$ corresponds to a discrete Conduché fibration over $L^{op}$ . Models of $L$ are categories of elements/sections of this fibration.

Theorem 37 (Makkai ). The category $Mod (L)$ of $L$ -structures and homomorphisms is the slice $Set / L^{op}$ when $L$ is direct (with appropriate naturality), with FOLDS-equivalence being the localisation along very-surjective maps.

6.4 HoTT in $(\infty, 1)$ -toposes

Theorem 38 (Shulman ). Every Grothendieck $(\infty, 1)$ -topos models HoTT with univalent universes.

Sketch. Shulman’s strategy: use simplicial categories of fibrant types to build an interpretation of MLTT in any presentable $(\infty, 1)$ -topos $X$ , then use Reedy fibrant replacement and the local universe construction (Lumsdaine–Warren) to produce a univalent universe object. ◻

6.5 The square of interpretations

with FOLDS sitting orthogonal to all three (FOLDS is a logic, not a set theory; it specifies which sentences are admissible). HoTT sits “above” the diagram: any model of ETCS, IZF, or FOLDS yields a model of HoTT after passage through the $(\infty, 1)$ -topos completion.

6.6 Reverse-mathematical strengths

We summarise the proof-theoretic strength of each system:

System	Strength (consistency)	Reference
ETCS	ZFC $-$ Replacement	McLarty 2004
ETCS+R (ETCS with Replacement)	ZFC	McLarty 2004
IZF	ZF	Friedman 1973
IZF+AC	ZFC	Diaconescu 1975
CZF	MLTT $+$ universes	Aczel 1978
CZF $+$ Mahlo	ZFC	Rathjen
HoTT (with UA)	ZFC $+$ inaccessibles	Shulman 2019
HoTT (without UA)	MLTT	MLTT proof theory
FOLDS (as logic)	—	—

The interesting feature: ETCS minus Replacement is strictly weaker than ZFC; recovering full ZFC strength requires a Replacement schema, in either material or structural form. HoTT with univalence and propositional resizing matches ZFC + countably many inaccessibles (Shulman ), since each universe behaves as a Grothendieck universe.

7 The univalence boundary

7.1 Definition

Definition 39 (Univalence boundary). A structural principle $P$ lies on the far side of the univalence boundary if $P$ holds in HoTT + UA but not in HoTT alone (i.e. in MLTT plus the assumption that identity types are well-behaved but without the univalence axiom). A principle lies on the near side if it holds in HoTT without UA. We say $P$ straddles the boundary if it is independent of UA in HoTT.

7.2 Far-side principles

Theorem 40 (Far-side: SIP needs UA). The Structure Identity Principle (SIP) is provably equivalent to univalence in HoTT.

Sketch. $UA \Rightarrow SIP$ : the standard structure-identity proof (HoTT Book §9.8) constructs the identification of structures using univalence applied to the underlying types and transport for the operations. $SIP \Rightarrow UA$ : instantiate SIP at the trivial signature (structure-free) to extract univalence as the special case where the only operation is the identity. ◻

Theorem 41 (Far-side: FOLDS-equivalence-implies-identity needs UA). The principle “ $M ≃_{F} N \Rightarrow M =_{Str (L)} N$ ” for arbitrary FOLDS signatures $L$ is equivalent to univalence (over MLTT with FE and PE).

Sketch. $UA \Rightarrow$ statement: this is 31. Statement $\Rightarrow UA$ : take $L$ to be the signature with one kind and no relations. A model is just a type. FOLDS-equivalence on this signature is type equivalence. The conclusion that equivalence is identification is exactly UA. ◻

7.3 Near-side principles

Theorem 42 (Near-side: NNO existence is near). The existence of an NNO in HoTT (as the inductive type $N$ ) does not require UA.

Proof. $N$ is generated by the constructors $0 : N$ and $s : N \to N$ together with the universal property given by the recursor; this is the elimination rule of MLTT inductive types and does not invoke UA. ◻

Theorem 43 (Near-side: function extensionality is near, given univalence is far). Function extensionality (FE) holds in HoTT + UA but is independent of MLTT alone. However, FE itself does not imply UA.

Sketch. $UA \Rightarrow FE$ : Voevodsky’s proof. $FE \neq \Rightarrow UA$ : the simplicial set model satisfies FE but without univalent universes (univalence requires more structure). ◻

7.4 Straddlers

Theorem 44 (Straddler: EM, AC are independent). The law of excluded middle EM and the axiom of choice AC are independent of UA in HoTT.

Sketch. EM: the classical model (sets) satisfies EM and UA; the topological model satisfies UA but not EM. Similarly AC. ◻

7.5 The boundary as a square

	Without UA	With UA
NNO	yes	yes
FE	independent	yes
PE	independent	yes
SIP	no	yes
FOLDS-eq=id	no	yes
EM	independent	independent
AC	independent	independent
Replacement	yes (small)	yes (small)

7.6 Diagnostic principles

Given an arbitrary structural principle $P$ , how can one test whether $P$ lies on the near or far side of the boundary? We propose the following heuristic.

Proposition 45 (Diagnostic for far-side principles). A principle $P$ lies on the far side of the univalence boundary if and only if $P$ asserts that two equivalent structures are equal, where equality is in the sense of HoTT’s identity type.

Heuristic argument. The forward direction is clear: such principles are precisely instances of the SIP schema (or the more general Univalence Principle), and we showed in [thm:sipneedsua,thm:foldsneedsua] that these need UA. The reverse direction relies on a meta-theoretic observation: principles that are not about identification are about existence or construction, and these are unaffected by UA’s content (which is about identity). A detailed proof requires formalisation of the schema, deferred to . ◻

7.7 What is on the boundary?

A principle is on the boundary if it is equivalent to UA in HoTT. Examples:

SIP (40).
Univalence Principle for FOLDS (41).
Function extensionality + propositional extensionality + Voevodsky’s “equivalence-induction” rule (a known characterisation of UA, due to Voevodsky).
Equivalence of $Π$ -types respecting equivalence of arguments (a partial characterisation).

Principles strictly weaker than UA (i.e. near side or straddle):

FE alone is strictly weaker than UA (the simplicial model with non-univalent universes satisfies FE).
PE alone is strictly weaker than UA.
NNO existence (theorem of MLTT, no UA needed).

8 Open problems

8.1 Problem 1: Contractibility of the type of ETCS structures

Conjecture 46. In HoTT + UA, the type $ETCS -Str := Σ_{S : Cat_{\infty}} Π_{i = 1}^{8} Ax_{i} (S)$ is contractible up to a fixed choice of universe parameter.

A proof would mirror Paper V Theorem 4.4 (contractibility of the NNO type) but at the level of the entire categorical universe. Tools needed: SIP for $\infty$ -toposes, internal $\infty$ -Yoneda (Riehl–Shulman directed type theory).

8.2 Problem 2: Cubical Agda formalisation of FOLDS

Conjecture 47. There is a Cubical Agda library implementing FOLDS signatures, FOLDS-equivalence, and $n$ -level FOLDS (Szumiło 2019), and proving 31 formally for $n \leq 2$ (equivalence of FOLDS-equivalence and HoTT-identification at $n = 0, 1, 2$ ).

Partial work exists in the agda-categories library and in Tsementzis’s formalisation of the SIP. Full FOLDS in Cubical Agda would close the gap between Makkai 1995 and ANST 2019 syntactically.

8.3 Problem 3: Identifying IZF axioms with HoTT principles

Conjecture 48. There is a precise correspondence between the IZF axioms and HoTT principles of the following form:

Extensionality $\leftrightarrow$ FE + PE.
Pairing/Union $\leftrightarrow$ Sigma/Coproduct.
Powerset $\leftrightarrow$ $A \to hProp$ (with propositional resizing).
Collection $\leftrightarrow$ Mahlo universe axiom.
$\in$ -Induction $\leftrightarrow$ accessibility predicate.
Full Separation $\leftrightarrow$ subtype formation under propositional resizing.

Partial work: HoTT Book §10.5; Awodey–Warren; Rathjen–Tupailo on CZF.

9 Discussion

9.1 What does “foundation” mean today?

The three-way comparison reveals that “foundations” has split into three orthogonal axes:

Material vs structural: ZFC (material) vs ETCS (structural).
Classical vs constructive: ZFC vs IZF/CZF.
0-categorical vs higher: ETCS (1-categorical) vs HoTT ( $\infty$ -categorical).

FOLDS is orthogonal to all three: it is a logic, applicable in any of the combinations.

9.2 Practical recommendations

For the working mathematician:

Pure category theory, classical: ETCS+AC.
Pure category theory, constructive: well-pointed Heyting topos.
Higher category theory, classical: HoTT+UA+AC (= simplicial sets model).
Higher category theory, constructive: HoTT+UA (= cubical model).
Pure logic, isomorphism-invariant: FOLDS over HoTT (Univalence Principle).
Reverse-mathematical strength: stay with ZFC variants.

9.3 Limitations

This paper does not prove the full Univalence Principle; we report the result of ANST 2019. We also do not address the predicativity issue: HoTT proper is predicative, IZF is impredicative, ETCS sits in between. A precise predicativity-comparative analysis is left to future work. Finally, the “square of interpretations” is not commutative on the nose; the diagram commutes up to bi-interpretation, a notion we have not fully formalised here.

10 Worked case study: monoid theory across the four foundations

To make the comparison concrete, we trace a single mathematical concept — the theory of monoids — through ETCS, IZF, FOLDS, and HoTT. This illustrates how “structural-ness” progresses from convention (ETCS) to enforced syntax (FOLDS) to internal theorem (HoTT+UA).

10.1 Monoids in ZFC and IZF

In ZFC/IZF, a monoid is a 4-tuple $(M, \cdot, e, laws)$ where $M$ is a set, $\cdot : M \times M \to M$ , $e \in M$ , and the associativity and unit laws hold. The encoding of the 4-tuple uses Kuratowski pairs. Two monoids are equal iff they have the same underlying $\in$ -tree — a notion that depends on the choice of pair encoding. Monoid isomorphism is a derived notion: a bijection $ϕ : M \to N$ commuting with operations. Junk theorems (e.g. “the underlying set of $Z$ contains the empty set as an element”) depend on encoding.

10.2 Monoids in ETCS

In ETCS, a monoid is an object $M$ together with morphisms $\cdot : M \times M \to M$ , $e : 1 \to M$ , and the equational axioms expressed using composition and the universal property of products. There is no encoding choice for $\cdot$ or $e$ . Two monoids are isomorphic iff there is an invertible morphism between them respecting the operations. The category $Mon (ETCS)$ of monoids in ETCS is well-defined, and is the category of models of the algebraic theory of monoids.

10.3 Monoids in FOLDS

A FOLDS signature for monoids:

Kind $M$ (elements).
Relation $E (x, y)$ (equality, parallel arrows from triangulation).
Relation $P (x, y, z)$ (multiplication: $z = x \cdot y$ ).
Relation $U (x)$ (unit: $x = e$ ).

Axioms:

Associativity: $\forall a, b, c, x y, y z, ab c, ab c^{'} : M . P (a, b, x y) \land P (x y, c, ab c) \land P (b, c, y z) \land P (a, y z, ab c^{'}) \Rightarrow E (ab c, ab c^{'}) .$
Left unit: $\forall e, x, e x : M . U (e) \land P (e, x, e x) \Rightarrow E (e x, x)$ .
Right unit: dual.

A FOLDS-equivalence between two monoids $M, N$ is a span via very surjective homomorphisms, which here coincides with the usual monoid isomorphism. Makkai’s invariance theorem guarantees: any FOLDS sentence holding in $M$ also holds in $N$ . There is no way to express “ $M$ is the monoid whose elements are von Neumann ordinals $\leq 5$ ” in FOLDS, since this is non-isomorphism-invariant.

10.4 Monoids in HoTT

In HoTT, a monoid is a Sigma-type: $Monoid := Σ_{M : Set} Σ_{\cdot : M \to M \to M} Σ_{e : M} (Assoc (\cdot) \times LUnit (\cdot, e) \times RUnit (\cdot, e)) .$ The components are: a set, a binary operation, an identity element, and proofs (mere propositions) of the laws.

Theorem 49 (Structure Identity Principle for monoids). For two monoids $M, N : Monoid$ : $(M =_{Monoid} N) ≃ MonoidIso (M, N)$ where $MonoidIso (M, N)$ is the type of monoid isomorphisms.

Sketch. By Sigma-induction on $M, N$ and SIP for each component: the sets are identified by UA, the operations and identity are transported, the laws are mere propositions and so identified automatically. The full proof is a routine application of HoTT Book §9.8. ◻

10.5 Comparison

	Equality	Iso	SIP-statement
ZFC	encoding-dependent	derived	metatheorem (sociological)
IZF	encoding-dependent	derived	metatheorem
ETCS	up to unique iso	primitive	metatheorem (categorical)
FOLDS	up to FOLDS-eq	primitive	syntactic (invariance theorem)
HoTT+UA	SIP-statement	primitive	internal theorem

The rightmost column is the key: only HoTT+UA makes the SIP an internal theorem, expressed in the same language as the structures themselves. ETCS makes it a category-theoretic metatheorem (true of every property of the category of sets). FOLDS makes it a syntactic invariance theorem (true of every well-formed FOLDS sentence). ZFC and IZF make it a sociological convention. Each escalation reduces the “trust assumption” needed.

11 Practical foundational choice

11.1 Which foundation for which task?

The foundational pluralism we have surveyed is not just a curiosity; it has practical consequences for formalisation projects.

Number theory and analysis: ZFC variants are best, due to the deep classical results requiring AC and EM. Lean/Mathlib uses ZFC (via the type-theoretic formalisation of $ZFSet$ inside Lean).
Category theory and topos theory: ETCS or HoTT+UA. ETCS is sufficient for 1-categorical structuralism; HoTT+UA is needed for higher-categorical structuralism (the theory of $(\infty, 1)$ -categories).
Synthetic differential geometry, synthetic homotopy theory: HoTT, naturally, since the synthetic methods rely on the type-theoretic semantics.
Constructive analysis and computer-verified mathematics: CZF or HoTT without UA, where computational interpretation is crucial.
Foundations of foundations (model theory of foundations themselves): IZF and topos theory provide the best general-purpose framework.
Pedagogy: ETCS is arguably the cleanest entry point, since it explains “what set theory is really doing” without the encoding noise.

11.2 Foundational consensus or pluralism?

A plausible reading of the present landscape is that no single foundation dominates; each excels in a particular domain. This contrasts with the 20th century, where ZFC was dominant. We propose to call the current situation principled pluralism: each foundation is correct for its target domain, and translation theorems (McLarty, Friedman–Aczel, ANST) tie them together.

11.3 Open foundational debates

Several debates remain unresolved as of 2026:

Predicativity vs impredicativity: HoTT proper is predicative; IZF is impredicative. The right level of impredicativity for a unified foundation is contested.
Constructivity vs classicality: HoTT defaults to constructive but is compatible with EM; IZF is constructive; ZFC is classical; FOLDS is logic-agnostic.
Higher coherence: how high should the dimensional ladder go? HoTT goes to $\infty$ ; FOLDS-Szumiło goes to arbitrary $n$ ; ETCS stops at $1$ .
The role of universes: HoTT has a Russellian hierarchy; ETCS has none (the category of all sets is the universe); IZF has none (the proper class of all sets); FOLDS has small categories of structures.

12 Conclusion

We have presented ETCS, IZF, and FOLDS as three orthogonal responses to the same underlying problem: how to build a foundation in which only structurally relevant assertions are formulable or provable. ETCS attacks the problem at the level of ontology (replace sets-with-membership by sets-with-functions). IZF attacks the problem at the level of logic (move to intuitionistic logic, where structural properties are easier to certify). FOLDS attacks the problem at the level of syntax (build a logic in which only invariant predicates are expressible).

HoTT—in particular HoTT + UA—synthesises all three. The Structure Identity Principle recapitulates the structural ontology of ETCS at the level of types. Constructive HoTT (without EM, without AC) shares the logical environment of IZF. The Univalence Principle recapitulates the syntactic invariance of FOLDS as a metatheorem.

The univalence boundary precisely separates: the principles that hold in MLTT alone (the near side: NNO, induction, basic structural reasoning), and the principles requiring univalence (the far side: SIP, FOLDS-equivalence-as-identity, the full equivalence principle). Mapping out this boundary is, we suggest, one of the more illuminating exercises in 2026 foundations.

Acknowledgements

The author thanks colleagues at the YonedaAI Research Collective for discussions on structuralism and on FOLDS-style invariance proofs. This paper continues the foundations programme of our prior series (Papers I–VI on HoTT and structural foundations), to which the reader is referred for the technical prerequisites.

F. W. Lawvere, An elementary theory of the category of sets, Proceedings of the National Academy of Sciences 52 (1964), 1506–1511. Reprinted with author’s commentary, TAC Reprints 11 (2005).

F. W. Lawvere and R. Rosebrugh, Sets for Mathematics, Cambridge University Press, 2003.

C. McLarty, Exploring categorical structuralism, Philosophia Mathematica 12 (2004), 37–53.

M. Makkai, First-order logic with dependent sorts, with applications to category theory, Preprint, McGill University, 1995. Available at https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.

H. Friedman, The consistency of classical set theory relative to a set theory with intuitionistic logic, Journal of Symbolic Logic 38 (1973), 315–319.

L. Crosilla, Set theory: constructive and intuitionistic ZF, Stanford Encyclopedia of Philosophy, Spring 2024 edition, ed. E. N. Zalta.

P. Aczel, The type theoretic interpretation of constructive set theory, in Logic Colloquium ’77, North-Holland (1978), 55–66.

S. Awodey, Structuralism, invariance, and univalence, Philosophia Mathematica 22 (2014), 1–11.

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013.

M. Shulman, All $(\infty, 1)$ -toposes have strict univalent universes, arXiv:1904.07004 (2019).

B. Ahrens, P. R. North, M. Shulman, D. Tsementzis, The Univalence Principle, arXiv:2102.06275 (2019/2021).

E. Palmgren, Categories with families and first-order logic with dependent sorts, arXiv:1605.01586 (2016).

N. Rasekh, Every elementary higher topos has a natural number object, arXiv:1809.01734 (2018), TAC 37(13) 2021.

V. Voevodsky, Univalent foundations of mathematics, preprint, IAS Princeton (2010).

J. M. E. Hyland, The effective topos, in The L. E. J. Brouwer Centenary Symposium, North-Holland (1982), 165–216.

J. Myhill, Constructive set theory, Journal of Symbolic Logic 40 (1975), 347–382.

A. Joyal and I. Moerdijk, Algebraic Set Theory, LMS Lecture Note Series 220, Cambridge University Press (1995).

D. Tsementzis, First-order logic with isomorphism, arXiv:1603.03092 (2016/2017).

S. Awodey, From sets to types to categories to sets, in Foundational Theories of Classical and Constructive Mathematics, Springer (2009).

E. Riehl and M. Shulman, A type theory for synthetic $\infty$ -categories, Higher Structures 1 (2017), 147–224, arXiv:1705.07442.

K. Szumiło, Frames in cofibration categories, Journal of Homotopy and Related Structures 14 (2019), 345–378. See also: $n$ -FOLDS and Reedy fibrant diagrams, preprint, 2019.