Set theory - type theory research?

Stream: Type theory

[Nir Paz]

This is a reference request that might fit in stackExchange better. I'm also refering to lean but I would be interested in similar questions about any comparable type theory.

Is there any research into the connections between models of lean and the models of ZFC they construct (with the standard Aczel construction that's in mathlib)?

For example it's clear that the cardinal arithmetic of the ZF model is inherited from the lean universe. I want to know if anything else is known about these models, like if there are statements independent of ZFC that they must satisfy (that are not trivialities such as Con(ZF)), or if there are natural type-theoretical axioms that imply set theoretical ones in the constructed model, such as V=L.

I haven't found anything online about how these ZFC models can look like, and anything like that would be appreciated (if it exists)!

[Mario Carneiro]

Lean is really equivalent to ZFC with countably many inaccessibles. From a set theory perspective there isn't anything additional going on there, all the statements which are independent in ZFC like the continuum hypothesis are also independent in lean.

[Mario Carneiro]

Note when I say "lean" I'm including the three standard axioms

[Mario Carneiro]

lean without those axioms is much different from ZFC, but probably not different in consistency strength

[Mario Carneiro]

I would like to prove that though... I'm hoping that one can just adapt a proof that IZF is equiconsistent to ZFC

[Nir Paz]

But there are statements in ZFC which I don't see a type theoretical equivalent of, ones that aren't purely combinatorical, like V=L, and there are probably possible additional axioms of lean which don't have an obvious ZFC version. It's not obvious to me that there is/isn't something that a model of lean has to satisfy so that the ZFC model will satisfy V=L.

[Nir Paz]

I don't love this example but I'm blanking on statements independent of ZFC that don't have a combinatorial interpretation.

[Nir Paz]

Lean and ZFC are the same on the intersection of things that they can both talk about, like cardinal arithmetic, but can there be statements close to their different foundations that have a non trivial relationship?

[Mario Carneiro]

The point is that both directions have essentially complete translations of the entire respective languages, so it's not really true that there are statements of ZFC without a type theoretical equivalent (because they can all just be encoded as statements about a big type which acts like the universe)

[Mario Carneiro]

V=L is not provable in lean (nor V!=L) for the same reason it's not provable in ZFC

[Mario Carneiro]

the translation from Lean to ZFC is more "lossy" in the sense that lots of things are 'encoded', so additional things become provable theorems that were independent in Lean. For example Nat = Int is independent in lean, but it becomes false when taking the standard encoding of Lean into set theory

[Mario Carneiro]

so in that sense this direction acts more like a "model construction"

[Mario Carneiro]

as far as I am aware though, for the encoding of ZFC in lean, the provable statements about that type are exactly (no more no less) those provable in ZFC + {exists n inaccessibles | n<omega}

[Nir Paz]

I haven't looked at the lean model in ZFC construction yet, is it true that when you construct a lean model, and then construct a ZFC model inside it over some universe, you get back V_k for the appropriate k? That would basically prove it.

[Mario Carneiro]

yes, with the standard model construction of Lean in ZFC and ZFSet.{0} inside that, the resulting set is constructively bijective with $V_{\kappa_0}$ where $\kappa_0$ is the first cardinal in the sequence used as a parameter of the model construction (we can take it to be the first inaccessible cardinal if we wish)

[Nir Paz]

Ah I see. Thanks!

[Bas Spitters]

Here's a recent one.
https://www.danielgratzer.com/papers/the-category-of-iterative-sets-in-homotopy-type-theory-and-univalent-foundations.pdf