Post #2103975

@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.