Is this approach compatible with large elimination?

[NathanielB123]

From what I understand, the current theory formalised here includes pi-types, base types (U₀) and something that looks a bit like large elimination (El₀). As far as I can tell though, the only reasonable large-elim-supporting way to instantiate U₀/El₀ is a universe containing bottom.

Specifically, consider adding a type of booleans with term and type-level if_then_else_s. I would like to have definitional equality, and so if true then A else B at the type level should reduce to A. Clearly this is impossible with el because el _ as a spine never reduces. I think adding a dedicated if_then_else_ constructor to spines would have the same problem (and putting terms in spines causes positivity issues anyway).

I think Conor's approach in "Outrageous but meaningful coincidences" avoids this issue by not having spines, and because types ask for an environment, they can, e.g. evaluate the condition expression into to a boolean, match on it, and return the LHS or RHS, reusing Agda's definitional equality. I don't think the same trick is possible when spines are added to the mix because they are inductively defined (this is what enables recursing on them in NbE) and so can't take an environment.

Note NbE also benefits from this restricted case of large elim. The only values of type el _ are neutrals. On the other hand, values of if c then A else B could be neutrals, values of type A or values of type B. By retaining propositional evidence of what c reduces to, I think NbE can almost be extended to deal with this but you get stuck when needing to reify a value of type A into a value of type if c then A else B (no propositional equality about the type can help with equating the fundamentally unequal spines).

Anyway, I'd be really interested to hear your opinions. Do you think I have understood this situation correctly/are there possible alternatives? I really like the idea of using "Outrageous but meaningful coincidences" to formalise a language, but having to choose between normalisation and large elimination seems like a pretty huge limitation.

[nad]

I seem to recall that @pigworker had some ideas about how to extend his approach to support normalisation, but I don't know how concrete those ideas were.

More recently I've contributed to an Agda formalisation of type theory that uses raw syntax and separate typing relations. That formalisation currently supports large elimination (with an infinite universe hierarchy), Π-types, Σ-types with or without η-equality, an empty type, unit types with or without η-equality, natural numbers, and identity types with or without the K rule. It is proved that every well-typed term has an η-long normal form, that definitional equality is decidable, that the supported type theories are consistent, and other things. There is also support for modalities, in particular erasure.

[NathanielB123]

Yeah at the end of the paper @pigworker mentioned the possibility of allowing free variables in the interpretation of types and perhaps getting normalisation that way, but at least when I tried, I kept hitting positivity issues (for the variables to be well scoped/typed, they need to be indexed by contexts/types themselves, and variables have to appear in negative position to allow instantiating with an environment in a non-empty context). Maybe there is some trick to make this work...

Wow I hadn't see that formalisation, cool! I do find intrinsically-typed syntax more appealing but given it seems there are quite fundamental issues (setoids/quotients having their own problems), perhaps separate typing relations are just a more practical approach.

P.S. I think Conor currently goes by they/them pronouns