search

teikalang / teika

MIT License
327 stars 7 forks source link

Commit on self types #186

Open EduardoRFS opened 1 year ago

EduardoRFS commented 1 year ago

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

EduardoRFS commented 11 months ago

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 commented 11 months ago

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

EduardoRFS commented 1 month ago

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 commented 1 week ago

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.