Core Theory

[phs]

Turns out an inductive definition of terms without their type annotations is not super useful.

In particular we already lose the ability to check local closure, since bound variables may appear in types!

So keep what we have as spiritual guidance, but otherwise replace it with a representation closer to a "pure type system". Here introducers and eliminators are embedded in judgements and inference rules.

In the spirit of the previous effort, the interesting relations and theorems are not in scope.

[phs]

Incidentally, we're initially shooting for an intensional, predicative type theory with products, functions and stratified universes. No Prop, no sigmas, no propositional equality, no inductive or W types.

I'm eventually aiming at McBride et al.'s observational type theory, meaning later we go after first class inductive types and a rich interplay between definitional and propositional equalities. Sigmas, sums, etc are all encodable as inductive types.

[phs]

Ha ha ha, wrong again!

At least, according to coq in coq, whose development is roughly equivalent to this one (at this stage). They very much break out inductive structures representing naked e.g. terms before couching them in their type theoretic rules.

They also do include the typing annotations in this raw form, even if they are "unused" prior to the introduction of the typing rules.

The problem with reaching for the PTS directly is it challenges the expressiveness of coq's inductive types, by trying to force the defined types to appear in their own definitions in uncomfortable places.

[phs]

I've been casually looking for reasons why people care about impredicativity. Finally noticed an example: polymorphic identity. A general identity function notably should be able to operate on itself, which directly violates predicativity.

[phs]

Hey if you dig observational type theory, check out cubical adventures which is a higher-dimensional version of the same. As before, it takes strong inspiration from univalence/HoTT but stops short of being it. It still gives us extensionality and good computable character.