# Postulating self types in a proof assistant

Self types introduce two typing new rules (simplified):

$$\frac{\Gamma \; \vdash \; t : [t/x]T}{\Gamma \; \vdash \; t : \iota x. T}$$ I-self and $$\frac{\Gamma \; \vdash \; t : \iota x. T}{\Gamma \; \vdash \; t : [t/x]T}$$ E-self

The are related to Very dependent types, dependent intersection.

Their huge appeal is that they allow to prove induction for lambda encoded terms. They are implemented in Formality for that reason.

Is it possible to "hack" them into Agda (or Coq) so that one can play with them in a familiar environment? By "hack" I mean that it is fine to disable termination-checker, allow type-in-type, postulate stuff etc. (I'd be happy with source code modification too but that is likely beyond my skill set).

My first idea was to model the encoding after isorecursive types with $$T$$ as a higher order type and postulate constants 'Self', 'self' and 'unself':

$$\frac {\Gamma, T:\star \rightarrow \star \; \vdash \; t : (T t)} {\Gamma, T:\star \rightarrow \star \; \vdash \; \text{self}\, t : \text{Self} \, T}$$ I-self and $$\frac {\Gamma, T:\star \rightarrow \star \; \vdash \; t : \text{Self} \, T} {\Gamma, T:\star \rightarrow \star \; \vdash \; \text{unself} \, t : T t}$$ E-self

And intended evaluation rule ($$\text{unself}\, (\text{self}\, t) \stackrel{\beta}{\rightarrow} t$$).

Unfortunately this is not working in Agda for various reasons:

postulate
Self : (T : Set -> Set) -> Set
unself : (T : Set -> Set) -> (t : Self T) -> T t
self : (T : Set -> Set) -> (t : T t) -> Self T


Perhaps the technique described in this mysterious issue in Agda can be of help.

• I'm curious what do you think the type of T should be in the two rules I-self and E-self? It is certainly not Set -> Set, more something like T ? -> Set but then you can't fill the question mark. I have a feeling that this isn't going to be possible in an intrinsically typed language such as Agda or Coq, perhaps Cedille (github.com/cedille) will get you further. – Jesper May 4 '20 at 7:38