Models of lean 4

Stream: Type theory

[Brendan Seamas Murphy]

Recently I've been thinking about some things involving the internal logic of the topos of sheaves on the one point compactification of N (or the stone cech compactification, either have the right logical properties). I'd like to prove some things synthetically, and I'm a lot more comfortable with lean over coq or agda. Does every sheaf topos model lean 4?

I think I really want to ask something more specific here, maybe whether it's true that in ZFC+"there exists a (ω+1)-indexed chain of inaccessibles κ0, κ1,...,κω", for any κ0-small topological space X we can model lean 4 in Fun(Opens(X)^op, Set_κω) where the dependent type formers have their usual topos-theoretic universal properties and Prop is the subobject classifier and for finite n the constant sheaf at V_κn is Type n and so on. Let me know if I've made any mistakes in this statement, I'm very new to this toposy stuff

[Jun Yoshida]

The standard reference of Lean's type system is https://github.com/digama0/lean-type-theory , which I believe is valid for Lean4 too. In this paper, an instance of Lean internal to ZFC+κω is constructed. Just glancing the construction, I think the choice function is used only to interpret Classical.choice, and the others make sense in general toposes (recall that the internal logic in any topos admits well-founded recursion and the unique choice). If so, the answer to your question is "Yes, except Classical.choice".

I am not an expert either. Please correct me if wrong.

[Brendan Seamas Murphy]

Yes, to be clear I meant lean excluding anything in the classical namespace

[Brendan Seamas Murphy]

I was mostly worried about quotient types and judgmental proof irrelevance, since I've heard type theorists grumble about these things. But I don't understand this stuff well enough to know whether those would preclude a model in a sheaf topos. I'll take a look at that paper

[Jun Yoshida]

In (sheaf) topos, neither the soundness of quatients nor proof irrelevance causes the problem as long as Prop is properly interpreted; e.g. as the type of subobjects of a fixed terminal object. (This may be problematic with internal universes)

[Trebor Huang]

Can you link a reference that solves the coherence issue for Prop? In the Lumsdaine local universes construction, there only seems to be a retraction between the elements of Prop and the subobject classifier, not an isomorphism.

[Trebor Huang]

And Hofmann's coherence construction seems to have difficulties dealing with intensional equality (i.e. without equality reflection).

[Johan Commelin]

@Sina I guess you are one of the canonical people to answer this question (-;

[Jun Yoshida]

Oops, it turned out that I was a serious stupid thinking Lean as a first-order type system, as it is mostly my use case. I am sorry my half-asleep brain and withdraw my answer; just forget about it.

[Reid Barton]

My answer "yes" is based on the following argument:

1. Lean's type theory is a subsystem of extensional type theory (in the sense that any judgment of Lean's type theory is also a valid judgment of extensional type theory).
2. Extensional type theory is valid in a topos (as are funext, propext etc.)

I'm not sure exactly how to justify either claim, especially 1.

[Reid Barton]

In particular, the extensionality is used to interpret the large elimination for the proposition Eq (which seems like the main dubious feature).