Post #2103972
2026-02-09 13:40 UTC
@edwinb @constantine I think we've been thinking very similar thoughts! https://owenlynch.org/archive/2025-aria-ta1-seminar/1.html
Replies (1)
-
@constantine@types.pl 2026-02-09 14:13
@olynch Cool! It seems there are many variations of this kind of system. I particularly like the version where instead of having a primitive open modality, which cannot be done with SOGATs if we want the "types only need modal contexts" rule (that is also in your slides), we just have a representable proposition P, and then a definitional iso (P -> Ty) ~= Ty. The direct GAT translation of this is already quite nice to work with and the original rule is admissible in the syntax.