**Lemme 4.7.**

1. ax11. Si $\alpha < \sup(\alpha, \beta)$, alors $\alpha < \beta$;

2. ax12. Si $\gamma < \alpha$ et $\alpha \le \sup(\beta, \gamma)$, alors $\alpha \le \beta$.

*Démonstration.* 1. Supposons $\alpha < \sup(\alpha, \beta)$. Le lemme 3.7 donne $\alpha < \alpha, \beta$. Le point 1 du lemme 4.6 donne $\alpha < \beta$.

2. Supposons $\gamma < \alpha$ et $\alpha \le \sup(\beta, \gamma)$. La première hypothèse donne $\gamma \le \alpha_F$ pour $F \subseteq_f \text{In}_\alpha$ non vide. La seconde hypothèse donne $\alpha \le \gamma, \beta$ (d'après le lemme 3.7). Par transitivité on a $\alpha \le \alpha_F, \beta$. Le point 2 du lemme 4.6 donne $\alpha \le \beta$. □

**Théorème 4.8.** Nous avons construit **Ord** en tant qu'un $\mathfrak{F}$-ordre.

*Démonstration.* En utilisant *rfl* et *trans1*, on montre d'une part que l'égalité est bien une relation d'équivalence, et d'autre part que la relation $\leqslant$ passe au quotient dans **Ord**.

De la même manière, *trans2* et *trans3* impliquent que la relation $<$ passe au quotient dans **Ord**.

La loi $\sup$ passe au quotient d'après le lemme 3.16.

La loi $\S$ passe au quotient d'après le lemme 3.16, point 2.

Il reste à noter que les axiomes 1 à 15 des $\mathfrak{F}$-ordres ont été démontrés précédemment. Voir, respectivement : le lemme 3.16 (point 3) ; le fait 3.8 (point 1) ; le lemme 3.16 (point 5) ; le lemme 4.3 ; le lemme 4.2 ; le fait 3.13 ; le lemme 4.4 ; le lemme 4.7 ; le fait 3.12 ; le lemme 3.16 (point 7) ; la remarque 3.9. □

Le théorème suivant généralise le fait 3.10.

**Théorème 4.9.** L'ensemble **Ord** n'est pas réduit à un point. Plus précisément :

— pour tous $\alpha, \beta \in \text{Ord}$, $\beta \le \alpha$ et $\alpha < \beta$ sont incompatibles;

— l'application $n \mapsto \underline{n} : \mathbb{N} \to \text{Ord}$ est injective ($m < n$ si, et seulement si, $\underline{m} < \underline{n}$);

— pour tout $\alpha \in \text{Ord}$ et $n > m$ dans $\mathbb{N}$, il est impossible que $s^{(n)}(\alpha) =_{\text{Ord}} s^{(m)}(\alpha)$.

*Démonstration.* Le premier point résulte de *irfl* et de *trans2*. Le reste suit. □

**Théorème 4.10.** **Ord** est objet initial dans la catégorie des $\mathfrak{F}$-ordres.

*Esquisse de démonstration.* L'idée est la suivante : la structure est « purement algébrique » et pour construire **Ord**, on n'a rien fait d'autre qu'utiliser les axiomes.

En effet, considérons un objet $(E, <_E, \leq_E, 0_E, \sup_E, s_E)$ dans la catégorie. Les éléments de **ord** ont leurs copies dans $E$. Et les relations $\cdot < \dots$ et $\cdot \le \dots$ que l'on a définies sur **ord** sont satisfaites dans $E$ d'après le fait 2.7 lorsqu'on les interprète dans $E$ via des sup finis à droite (comme cela est nécessaire d'après le lemme 3.7). Cela implique qu'il y a un unique morphisme de **Ord** vers $E$ dans la catégorie considérée. □

## 4.2 Quelques propriétés supplémentaires

**Proposition 4.11.** La relation binaire $<$ sur **Ord** est bien fondée.

*Démonstration.* Conséquence directe du fait 3.4. □

**Lemme 4.12** (formes faibles de la disjonction "$\alpha \le \beta$ ou $\beta < \alpha$").

Soient $r \ge 1$ et $\alpha, \beta^1, \dots, \beta^r, \gamma \in \text{ord}$.

1. Si $\alpha \le \beta$ et $\beta < \alpha, \gamma^1, \dots, \gamma^r$, alors $\beta < \gamma^1, \dots, \gamma^r$.

2. Si $\beta < \alpha$ et $\alpha \le \beta, \gamma^1, \dots, \gamma^r$, alors $\alpha \le \gamma^1, \dots, \gamma^r$.

*Démonstration.* On pose $\beta = \sup(\beta^1, \dots, \beta^r)$ et l'on est ramené à des propriétés déjà démontrées (en utilisant le lemme 3.7). □

**Définition 4.13.** Un élément $\beta = s(\beta_i)_{i \in \text{In}_\beta} \in \text{ord}$ est dit filtrant si pour tout $F \subseteq_f \text{In}_\beta$, il existe $j \in \text{In}_\beta$ tel que $\sup(\beta_i)_{i \in F} \le \beta_j$.

**Lemme 4.14.** Pour tout $\alpha \in \text{ord}$, il existe un $\beta \in \text{ord}$ tel que $\alpha =_{\text{Ord}} \beta$ et $\beta$ est filtrant.

*Démonstration.* Si $\alpha = s(\alpha_i)_{i \in J}$, on note $K$ l'ensemble des parties finiment énumérées de $J$, et pour $F \subseteq_f J$ on note $\beta_F = \sup(\alpha_j)_{j \in F}$. Enfin $\beta = s(\beta_F)_{F \in K}$. □
## 4.3 Arithmétique élémentaire des ordinaux

### Addition (séquentielle)

L'addition $\alpha + \beta$ ($\alpha$ suivi de $\beta$: l'addition n'est pas commutative) est définie par induction sur $\beta$ :

$$ \alpha + \underline{0} = \alpha \quad \text{et} \quad \alpha + \beta = s(\alpha + \beta_j)_{j \in \text{In}_\beta} \quad \text{si} \quad \beta = s(\beta_j)_{j \in \text{In}_\beta} \in \text{ord}^*. $$

Cette formule pour $\alpha + \beta$ ne fonctionne que pour le cas $\text{In}_\beta \neq \mathbb{N}_0$ (elle donnerait $\alpha + \underline{0} = \underline{0}$). Nous avons aussi $\alpha + \beta = \sup((\alpha + \beta_j) + \underline{1})_{j \in \text{In}_\beta}$ si $\text{In}_\beta \neq \mathbb{N}_0$.

Les propriétés suivantes se démontrent par induction :

- si $\alpha \le \alpha'$ et $\beta \le \beta'$, alors $\alpha + \beta \le \alpha' + \beta'$;

- $(\alpha + \beta) + \gamma = \alpha + (\beta + \gamma)$;

- $\alpha + \underline{0} = \underline{0} + \alpha = \alpha$;

- $\alpha + \beta \le \alpha + \gamma$ si, et seulement si, $\beta \le \gamma$;

- $\alpha + \beta < \alpha + \gamma$ si, et seulement si, $\beta < \gamma$;

- $\alpha = \underline{1} + \alpha$ si, et seulement si, $\omega \le \alpha$;

- si $\alpha \le \gamma$, alors il y a un $\beta$ tel que $\gamma = \alpha + \beta$;

- si $\alpha < \gamma$, alors il y a un $\beta \ne \underline{0}$ tel que $\gamma = \alpha + \beta$.

### Somme séquentielle

Soit $J \in \mathfrak{F}$ muni d'une relation d'ordre $\prec$ bien fondée, possédant un élément minimum $0_J$ détachable. Soit $(\beta^j)_{j \in J}$ un élément de $\text{Fam}(J, \mathbf{Ord})$. La « somme indexée $\prec$-séquentielle » $\sum_{j \prec \ell} \beta^j$ est définie par induction sur $\ell$ dans $(J, \prec)$ :

$$ \sum_{j<0_J} \beta^j = 0_J \quad \text{et} \quad \sum_{j<\ell} \beta^j = \sup \left( \left( \sum_{j<k} \beta^j \right) + \beta^k \right)_{k<\ell} \quad \text{si } 0_J \prec \ell. $$

On démontre par induction sur $J$ que si l'on a deux familles $(\beta^j)_{j \in J}$ et $(\gamma^j)_{j \in J}$ avec $\beta^j \le \gamma^j$ pour tout $j \in J$, alors pour tout $\ell \in J$, $\sum_{j<\ell} \beta^j \le \sum_{j<\ell} \gamma^j$. Cette construction passe donc au quotient $\mathbf{Ord}$.

Remarque 4.15. Cette construction permet de définir une fonction $\text{ord}_2^{\text{Br}} \to \text{ord}_2$, où $\text{ord}_2^{\text{Br}}$ est l'ensemble des noms des ordinaux de Brouwer. Voir Troelstra (1969) et Brouwer (1918, 1926). Troelstra traite uniquement les ordinaux de Brouwer dénombrables.

### Multiplication

On définit $\alpha \cdot \beta$ par induction sur $\beta \in \mathbf{ord}$ :

$$ \alpha \cdot \underline{0} = \underline{0} \quad \text{et} \quad \alpha \cdot \beta = \sup(\alpha \cdot \beta_j + \alpha)_{j \in \text{In}_\beta} \quad \text{si} \quad \beta = s(\beta_j)_{j \in \text{In}_\beta} \in \mathbf{ord}^*. $$

Les propriétés suivantes se démontrent par induction :

- si $\alpha \le \alpha'$ et $\beta \le \beta'$, alors $\alpha \cdot \beta \le \alpha' \cdot \beta'$;

- $(\alpha \cdot \beta) \cdot \gamma = \alpha \cdot (\beta \cdot \gamma)$;

- $\alpha \cdot \underline{1} = \underline{1} \cdot \alpha = \alpha$;

- $\alpha \cdot (\beta + \gamma) = (\alpha \cdot \beta) + (\alpha \cdot \gamma)$;

- si $\underline{1} \le \alpha$, alors $\alpha \cdot \beta \le \alpha \cdot \gamma$ si, et seulement si, $\beta \le \gamma$;

- si $\underline{1} \le \alpha$, alors $\alpha \cdot \beta < \alpha \cdot \gamma$ si, et seulement si, $\beta < \gamma$.

### Exponentiation

On définit $\alpha^\beta$ par induction sur $\beta \in \mathbf{ord}$ :

$$ \alpha^{\underline{0}} = \underline{1} \quad \text{et} \quad \alpha^{\beta} = \sup(\alpha^{\beta_j} \cdot \alpha)_{j \in \text{In}_\beta} \quad \text{si} \quad \beta = s(\beta_j)_{j \in \text{In}_\beta} \in \mathbf{ord}^*. $$
## Ackermann

On peut continuer cette «arithmétique élémentaire» à la Ackermann comme dans Finsler 1951 en définissant par induction un ordinal Ack($\alpha, \beta, \gamma$) obtenu «en itérant $\gamma$ fois la fonction précédente, initialisée à $\alpha$», c'est-à-dire de manière plus précise

$$ 
\begin{align*}
\underline{\text{Ack}}(\alpha, \beta, \mathbf{0}) &= \alpha + \beta \\
\underline{\text{Ack}}(\alpha, \mathbf{0}, \gamma) &= \alpha \quad \text{si } \gamma \in \mathbf{ord}^* \\
\underline{\text{Ack}}(\alpha, \beta, \gamma) &= \sup\left(\sup\left(\underline{\text{Ack}}\left(\underline{\text{Ack}}(\alpha, \beta_j, \gamma), \alpha, \gamma_k\right)\right)_{j \in \text{In}_\beta}\right)_{k \in \text{In}_\gamma} \\
&\qquad \text{si } \beta = s(\beta_j)_{j \in \text{In}_\beta} \text{ et } \gamma = s(\gamma_k)_{k \in \text{In}_\gamma}.
\end{align*}
$$

En particulier, $\varepsilon_0 = \underline{\text{Ack}}(\omega, \omega, \mathbf{4})$.

# 5 Ordinaux dénombrables

## 5.1 Premiers pas

Comme indiqué précédemment, les ordinaux de la seconde classe (les ordinaux dénombrables), sont définis en prenant l'ensemble d'indexeurs

$$ \mathfrak{F}_2 = \{ \mathbb{N}_k \mid k \in \mathbb{N}, k \ge 0 \} \cup \{ \mathbb{N} \} $$

muni d'opérations convenables pour l'ensemble des sous-ensembles finis d'un $I \in \mathfrak{F}$ et pour les réunions disjointes d'éléments de $\mathfrak{F}$ indexés par un élément de $\mathfrak{F}$. On écrit $\text{ord}_2$ et $\text{Ord}_2$ pour $\text{ord}_{\mathfrak{F}_2}$ et $\text{Ord}_{\mathfrak{F}_2}$. Donc $\text{Ord}_2$ est l'ensemble des ordinaux de la seconde classe tandis que $\text{ord}_2$ est un ensemble de noms pour les éléments de $\text{Ord}_2$.

**Lemme 5.1.** *Tout ordinal dénombrable est le s d'une suite croissante d'ordinaux dénombrables.*

*Démonstration.* C'est le lemme 4.14. □

**Proposition 5.2.** *Supposons LPO. Alors, pour $\alpha, \beta \in \text{Ord}, \text{ on a } \alpha \le \beta \text{ ou } \beta < \alpha.*

*Démonstration.* C'est comme la proposition 3.19, pour le cas dénombrable. □

## 5.2 Comparaison avec les ordinaux de Martin-Löf

Nous présentons ici une variante de la théorie des ordinaux du livre Notes on Constructive Mathematics (Martin-Löf 1970, Chapter 3). Nous disons «variante» car la théorie de Martin-Löf est présentée dans le cadre des mathématiques récursives à la Markov, alors que nous nous situons dans la logique intuitionniste avec les définitions inductives généralisées, comme dans le travail Heyting 1961 (le fait que ce cadre fournit un traitement plus élégant que celui des mathématiques récursives est souligné dans le rapport de Kreisel (1963) sur ce travail).

### 5.2.1 Le système formel de Martin-Löf

Dans ce système, les ordinaux sont décrits de manière inductive : si l'on a une suite finie ou infinie d'ordinaux $\sigma = \sigma_0, \dots, \sigma_n, \dots$ (peut-être vide), alors $s(\sigma)$ est un ordinal.

La sémantique classique de cette opération est la suivante : à la suite d'ordinaux $(\sigma_n)$ on associe le supremum de la suite des successeurs des $\sigma_n$.

En particulier, $\mathbf{0}$ est défini comme $s(\sigma)$, où $\sigma$ est la suite vide.

Nous écrivons simplement $s(\alpha)$ pour $s(\sigma)$, où $\sigma$ est la suite à un élément $\sigma_0 = \alpha$.

En mathématiques constructives, l'ensemble de ces ordinaux est un exemple d'ensemble non discret.

Comme décrit dans l'introduction, à chaque ordinal $\alpha$ nous associons, par induction sur $\alpha$, un arbre $\text{Tree}(\alpha)$ : $\text{Tree}(\alpha)$ contient toujours la suite vide, et $\text{Tree}(s(\sigma))$ contient $n \sim \ell$ si $\ell$ est dans $\text{Tree}(\sigma_n)$.
Cet ensemble $\text{Tree}(\alpha)$ ne contient aucune branche infinie : si $f$ est une fonction numérique, nous pouvons toujours trouver un $n$ tel que $[f(0), \dots, f(n-1)]$ n'est pas dans $\text{Tree}(\alpha)$. Ceci est démonté directement par induction sur $\alpha$. Autrement dit, l'arbre $\text{Tree}(\alpha)$ est bien fondé.

L'ensemble de ces arbres, $\text{ord}_2$, est l'ensemble des noms d'ordinaux, aussi bien chez Martin-Löf que dans notre approche.

Le fait que l'on trouve de cette manière tous les arbres bien fondés est le contenu du théorème de la barre. Ce théorème de Brouwer n'est valide ni dans la théorie des ensembles de Bishop, ni dans la théorie des types dépendants. Cela résulte du fait que ces deux systèmes ont une interprétation en mathématiques récursives, où le théorème de la barre est faux, comme démontré dans un exemple dû à Kleene (voir Kleene et Vesley 1965).

Par définition, une formule atomique est une formule de la forme $\alpha < \beta$ ou $\alpha \le \beta$; et un séquent est un ensemble fini de formules atomiques.

Nous définissons maintenant par induction la phrase « le séquent $\Gamma$ est valide ». La formulation est très élégante !

$$ \frac{\Gamma, \alpha \leq \sigma_n}{\Gamma, \alpha < s(\sigma)} \qquad \frac{\dots \Gamma, \sigma_n < \beta \dots}{\Gamma, s(\sigma) \leq \beta} $$

Notez qu'il y a une démonstration directe de $\emptyset \le \beta$ par la deuxième règle, appliquée avec un ensemble vide de prémisses.

La signification intuitive du séquent est la disjonction classique des formules atomiques qu'il contient.

Martin-Löf définit alors une relation d'équivalence $\alpha =_{\text{ML}} \beta$ sur $\text{ord}_2$ comme exprimant le fait que les séquents $\alpha \le \beta$ et $\beta \le \alpha$ sont valides. L'ensemble des ordinaux de Martin-Löf, noté $\text{Ord}_2^{\text{ML}}$, est le quotient de $\text{ord}_2$ par cette relation d'équivalence.

Martin-Löf prouve le séquent $\alpha < \beta, \beta \le \alpha$ par induction sur $\beta$ et $\alpha$. Il démontre aussi par induction sur $\alpha$ que la règle suivante est admissible :

$$ \frac{\Gamma, \alpha < \alpha}{\Gamma}, $$

ce qui implique en particulier que $\alpha < \alpha$ n'est pas démontrable.

Donnons un exemple de telles démonstrations par induction.

**Lemme 5.3.** Pour tout $\alpha$ les séquents $\alpha \le \alpha$ et $\alpha < s(\alpha)$ sont valides.

*Démonstration.* On démontre $\alpha \le \alpha$ par induction sur $\alpha$. Si $\alpha = s(\sigma)$, on doit montrer $\sigma_n < s(\sigma)$ pour tout $n$, ce qui résulte de $\sigma_n \le \sigma_n$, qui se démontre par induction.

Par suite on a $\alpha < s(\alpha)$ en utilisant la première règle. $\square$

Martin-Löf peut également démontrer l'analogue du théorème 4.9 pour $\text{Ord}_2^{\text{ML}}$. Mais les deux énoncés pour $\text{Ord}_2^{\text{ML}}$ et pour notre $\text{Ord}_2$ sont indépendants l'un de l'autre.

### 5.2.2 Comparaison avec notre système

Expliquons maintenant pourquoi cette définition ne coïncide pas avec la nôtre. Pour cela nous donnons un exemple de la forme $\alpha < \beta$ qui est démontrable dans ce calcul des séquents, mais qui implique **LPO** dans notre système.

On reprend l'exemple 3.18 : on définit $\alpha = s(\sigma)$, où $\sigma_n = \frac{u_n}{\alpha}$ avec $(u_n)$ une suite croissante (au sens large) de 0 et de 1, et $\beta = s(\tau)$, où $\tau_n = s(\sigma_n) = \frac{u_n+1}{\beta}$.

**Lemme 5.4.** Le séquent $\alpha < \beta$ est valide.

*Démonstration.* D'après la première règle, il suffit de valider le séquent $\alpha < s(\tau), \alpha \le \tau_0$. Pour cela on doit démontrer pour tout $n$ le séquent $\sigma_n < \tau_0, \alpha < s(\tau)$. Fixons $n$. Si l'on a $\sigma_n < \tau_0 = s(\sigma_0)$, c'est OK. Notez que nous pouvons tester si $\sigma_n < \tau_0$ est valide ou pas car $\sigma_n$ et $\tau_0$ sont tous deux de la forme $\emptyset$ ou $\frac{1}{2}$ ou $\frac{1}{2}$.

Sinon, nous avons explicitement un $n$ tel que $\sigma_n \ge s(\sigma_0)$ et on a alors $\sigma_m \le \sigma_n$ et donc $\sigma_m < \tau_n$ pour tout $m$. On démontre $\sigma_n < \tau_0, \alpha < s(\tau)$ comme conséquence de $\sigma_n < \tau_0, \alpha \le \tau_n$ qui est valide parce que $\sigma_n < \tau_0, \sigma_m < \tau_n$ est valide pour tout $m$. $\square$
Notez que nous démontrons $\alpha < s(\tau)$ en démontrant $\alpha < s(\tau)$, $\alpha \le \tau_0$, et l'on doit "garder" $\alpha < s(\tau)$ : peut-être $\alpha \le \tau_0$ n'est pas valide (il se peut que la suite $(\sigma_n)$ prenne la valeur $\underline{1}$ et que $\tau_0 = \underline{1}$).

Dans l'exemple 3.18, on a vu que $\alpha < \beta$ implique **LPO** dans notre système. Par conséquent, dans l'ensemble $\mathbf{Ord}_2^{\mathrm{ML}}$ des ordinaux de Martin-Löf, l'égalité est plus grossière que dans l'ensemble $\mathbf{Ord}_2$ (les deux sont des quotients de $\mathbf{ord}_2$).

Références

Peter ACZEL et Michael RATHJEN : CST book draft. http://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010. F2

Nicolas BOURBAKI : *Éléments de mathématique : théorie des ensembles*. Hermann, Paris, 1970. Nouvelle édition. F2

L. E. J. BROUWER : Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil : allgemeine Mengenlehre. *Verh. Nederl. Akad. Wetensch. Afd. Natuurk. Sect. 1*, 12(5):3-43, 1918. F17

L. E. J. BROUWER : Zur Begründung der intuitionistischen Mathematik. III. *Math. Ann.*, 96:451-488, 1926. http://eudml.org/doc/159181. F2, F17

Alonzo CHURCH : The constructive second number class. *Bull. Amer. Math. Soc.*, 44:224-232, 1938. doi:10.1090/S0002-9904-1938-06720-1. F2

Patrick DEHORNOY : *La théorie des ensembles : introduction à une théorie de l'infini et des grands cardinaux*. Tableau Noir, 106. Calvage et Mounet, Paris, 2017. F2

Paul FINSLER : Eine transfinite Folge arithmetischer Operationen. *Comment. Math. Helv.*, 25:75-90, 1951. http://eudml.org/doc/139019. F18

Gerhard GENTZEN : Die Widerspruchsfreiheit der reinen Zahlentheorie. *Math. Ann.*, 112:493-565, 1936. http://eudml.org/doc/159839. Traduction par M. Szabo : The consistency of elementary number theory, in *Szabo 1969*, pages 132-201. F2

Arend HEYTING : Infinitistic methods from a finitist point of view. In *Infinitistic methods : proceedings of the symposium on foundations of mathematics*, Warsaw, 2-9 September 1959, pages 185-192. Pergamon, Oxford et Państwowe Wydawnictwo Naukowe, Varsovie, 1961. F2, F18, F20

Stephen Cole KLEENE : On notation for ordinal numbers. *J. Symb. Log.*, 3:150-155, 1938. http://www.jstor.org/stable/2267778. F2

Stephen Cole KLEENE et Richard Eugene VESLEY : *The foundations of intuitionistic mathematics, especially in relation to recursive functions*. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1965. F19

Nicolai KRAUS, Fredrik NORDVALL FORSBERG et Chuangjie XU : Connecting constructive notions of ordinals in homotopy type theory. In *46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)*, Leibniz International Proceedings in Informatics (LIPIcs), 202, pages 70:1-70:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LI-PIcs.MFCS.2021.70. arXiv:2104.02549 contient un appendice avec des démonstrations. F2

Georg KREISEL : Recension de Heyting 1961. *Math. Rev.*, 26, 1963. #2363 (MR0144822), http://mathscinet.ams.org/mathscinet-getitem?mr=144822. F18

Jean-Louis KRIVINE : *Théorie des ensembles*. Cassini, Paris, 1998. F2

Per MARTIN-LÖF : *Notes on constructive mathematics*. Almqvist & Wiksell, Stockholm, 1970. F1, F2, F18

Ray MINES, Fred RICHMAN et Wim RUITENBURG : *A course in constructive algebra*. Universitext. Springer, New York, 1988. F2

Manfred E. SZABO, éditeur. *The collected papers of Gerhard Gentzen*. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1969. F20

Anne S. TROELSTRÅL : *Principles of intuitionism : lectures presented at the summer conference on intuitionism and proof theory (1968) at SUNY at Buffalo, N.Y.* Lecture Notes in Mathematics, 95. Springer, Berlin, 1969. F17

UNIVALENT FOUNDATIONS PROGRAM : *Homotopy type theory : univalent foundations of mathematics*. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. F2