Commit on self types

[EduardoRFS]

Should self types trigger an error and only be used by macros?

[EduardoRFS]

This will not be the case, I made the decision to go strictly with dependent intersection as when combined with mutual recursion(induction-induction), they are more general than self.

[EduardoRFS]

Keeping this open to document the thought process and the details.

[EduardoRFS]

Mostly the idea is that, you can replace %self(x). T by A where A == (x : A) & T, this requires a recursive type and while I believe it to be weaker, it is way more well behaved requiring only more or less traditional type theory.

Additionally this dependent intersection can be decomposed further into coinductive pairs and the axiom K, it also implies in the axiom K, which breaks univalence but that can be solved in a dozen ways.

[EduardoRFS]

I'm not super sure about this choice, self seems more well behaved under computationally relevant equality like HoTT. Additionally it seems like self + intersection = dependent intersection, which makes sense but the dual of the dependent intersection is lacking, which indicates something wrong in the theory.