6
$\begingroup$

Is there any book that teaches the basics of Type Theory and Calculus of Inductive Constructions (CIC) and also shows a construction of ZFC (or preferably NBG) in CIC?

I only found the paper "Sets in types, types in sets" by Benjamin Werner, but it assumes that the reader knows type theory.

Thank you for your attention!

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ It's not exactly what you asked for for several reasons, but the HoTT book does start from basic type theory, and constructs a universe of ZF-style sets in section 10.5. $\endgroup$
    – Reid Barton
    Commented Apr 6, 2023 at 8:01

1 Answer 1

Reset to default
5
$\begingroup$

As noted by Reid Barton in comments, the Homotopy Type Theory book is probably the closest to what you ask for. It introduces its dependent type theory (which is essentially CIC plus extra assumptions of univalence and, later in the book, higher inductive types) from the ground up. In §10 it introduces a type $V$ representing the cumulative hierarchy, as a higher inductive type, and in Thm 10.5.11, it shows that under the assumption of AC in the ambient type theory, $V$ models ZFC. (They don’t explicitly say so, but the proof also easily shows: under the assumption of LEM, $V$ models ZF.)

This may not quite fit your bill, for a couple of reasons. Firstly, it’s not exactly a generic introduction to CIC, since its approach to working in type theory is deeply infused with the homotopical viewpoint; compared to how one works in non-homotopical type theory, a lot is the same, but some things are necessarily different. Secondly, its construction of the cumulative hierarchy makes use of HIT’s and univalence, which you may not want to assume.

This latter gap is bridged in Håkon Gylterud’s paper From multisets to sets in homotopy type theory, which gives a construction of $V$ without using HIT’s, and then shows that it satisfies the universal property of the HoTT book’s $V$. It follows that the theorem above holds: assuming AC, Gylterud’s $V$ models ZFC. Gylterud’s results on $V$ use univalence at just one point, to show that $V$ is a set — but in fact that doesn’t require full univalence. All that’s needed is the weaker property that $(a =_U b) \to (a \simeq b)$ is always an embedding (this doesn’t have a well-established name; I call it subunivalence) — this is a consequence of univalence, but also of UIP, so holds in both “fully homotopical” and “fully set-based” models.

Gylterud’s $V$ is also closely related to the oldest and most well-studied interpretation of set theory into type theory, Aczel’s $W$ — Gylterud’s papers give good references on that, and discussion of the connections.

Improve this answer
$\endgroup$
4
  • $\begingroup$ With the theory presented in the HoTT book, will I be able to formalize, for example, what are in the books "Classical Set Theory" (by Taras Banakh) and "The Structure of the Real Line" (by Lev Bukovský)? Now I want to learn a Dependent Type Theory similar to those behind theorem prover like Lean and Coq because later I want to rewrite everything using a specific theorem prover (now I just want to prove everything without using any proof assistant). $\endgroup$
    – rfloc
    Commented Apr 6, 2023 at 13:34
  • 2
    $\begingroup$ @rfloc: I haven’t seen those books before so this is only based on a quick look, but: On the one hand, in principle, yes I think you could formalise that material inside the HoTT book’s implementation of ZFC. But (depending on your motivations) that seems a rather unnatural thing to do — formalising mathematical topics within ZFC, inside the interpretation of ZFC into type theory. To use a programming analogy, that’s like writing your programs in assembly language, and then writing an assembly language interpreter in C. [cont’d] $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Apr 6, 2023 at 13:48
  • 1
    $\begingroup$ [cont’d] It will teach you a lot about assembly language interpreters, but it’s not an efficient way to implement programs. Type theory is a higher-level language than set theory in the first place, designed to be closer to mathematical practice — if your main goal is understanding how to formalise mathematical structures, order theory, real analysis, etc, in type theory/proof assistants, then I wouldn’t recommend going via ZFC (and I think few people in the field would). $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Apr 6, 2023 at 13:48
  • 1
    $\begingroup$ @rfloc Isabelle may be a better choice if you want to formalize things set-theoretically. There's Isabelle/ZF as well as auto2. $\endgroup$
    – Timothy Chow
    Commented Apr 7, 2023 at 13:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .