Algebro-geometric model for dependent type theory

Stream: Type theory

[Roman Bars]

IIUC in Lean's type theory the question of whether a given type is inhabited is semi-decidable (since the formal language of raw terms is recursively enumerable and probably even context-free). Another question that is semi-decidable is whether a diophantine equation has solutions. In fact by the MRDP theorem any instance of the halting problem can be reduced to the solving Diophantine equations.

So I wonder if a model could be constructed for dependent type theory where types are schemes/stacks/Zariski sheaves defined by finitely many bits of data and the terms are integer points of those objects. The empty type would be the empty scheme and the unit type would be Spec Z. The universes would then be "moduli spaces" of these objects. Dependent product types would be fiber products of the universal family and whatever family of types you have.

There is many issues e.g. exponential objects usually don't exist in the category of schemes. One solution is to restrict what schemes we consider e.g. if you only consider smooth complete hyperbolic varieties you can get some useful finiteness for Hom spaces There are more issues e.g. the moduli space of a particular deformation class of hyperbolic varieties need not itself be hyperbolic: look at the moduli space of curves. Thus it's not clear how to get an infinite hierarchy of universes. Also things like Faltings's theorem impose restrictions on what we get if we only consider hyperbolic varieties.

Exponential objects exist in any topos but then how do we carve out objects of "finite type" within a topos?

Also I have no idea if there is a natural interpretation of inductive types in this language.

Has anybody considered something like this in the literature? I would appreciate any pointers.

[Johan Commelin]

What kind of application would this have? Are you aiming for some sort of synthetic way to do algebraic geometry? Or do you have a different intention?

[Roman Bars]

I don't have any applications in mind really. I just wondered if we could incorporate geometric intuition into type-theoretic reasoning.

Though there is one explicit thing you could extract: while not every variety has a rational point any non-empty variety has a point over some number field. So from a propositions-as-types perspective this means for each statement there would be some natural weakenings of it that are easier to prove. This seems curious.

[Kevin Buzzard]

It says that a pullback has points, which is like saying that if you add more hypotheses you might be able to prove your theorem

[Kevin Buzzard]

I don't know anything about the foundations of type theory. Can you explicitly write down the type which you're worried about for schemes? I don't know what an exponential object is but I do know what a scheme is

[Kevin Buzzard]

Isn't the issue going to be inductive types?

[Roman Bars]

An exponential object is basically an internal Hom so for example if you take X=Y=affine line then Hom(X, Y) wouldn't be a scheme. Or you could take X=Y=projective line in which case Hom(X, Y) would be a scheme but it would not be complete so then Hom(Hom(X, Y), Hom(X, Y)) probably wouldn't be a scheme.

Regarding adding hypotheses you are correct but it just seems a little surprising to me that you can write down your (infinite) list of number fields once and for all and then for any non-empty variety you will get a point valued in one of those number fields. Meanwhile for propositions I don't know how to uniformly generate more hypotheses that might help.

[Kevin Buzzard]

Just to be clear here, the MRDP result is of an arithmetic nature, it's about Spec(Z). Finite type schemes over Spec(Z) will presumably have a section after some flat extension but general schemes won't, eg Spec(C) won't obtain a section over any number field.

[Kevin Buzzard]

The base change idea seems to be along the lines of "you might not be able to prove P, but if you assume it you'll be able to prove it".

I guess that exponentiation not working is related to the fact that there doesn't seem to me to be any natural way of doing "not" with schemes.

[Kevin Buzzard]

I guess Hom(A^1,A^1) is an ind-scheme?

[Roman Bars]

Regarding "not" if there was a natural way to do it then there would be one and only one map between any two finite type Z-schemes without Z-points (which has no chance of being true). Then this line of thinking is nonsense. I'm a little embarassed I didn't see it immediately.

[Kevin Buzzard]

Aha. There are too many schemes with no Z-points and they don't map to the empty scheme