Notices

1. Izzy Swart (syntacticsugarglider@merveilles.town)'s status on Thursday, 12-Aug-2021 12:49:44 CEST Izzy Swart

   • theruran 🌐🏴
   • chjara~
   • chaotic avocado goblin

   @theruran @a_breakin_glass @chjara this is based on System S, and is mostly prior art from Formality (jcb and victor maia) minus the reflection stuff, which isn't that theoretically interesting. just different practical goals. I haven't read Barendregt so I don't know how PTS classifications work, but I know every corner of the lambda cube can be classified in terms of PTS stuff, and this shares a corner with inductive CoC plus primitives (a la coq etc.)

   • Izzy Swart (syntacticsugarglider@merveilles.town)'s status on Thursday, 12-Aug-2021 12:49:44 CEST Izzy Swart

     in reply to

     • theruran 🌐🏴
     • chjara~
     • chaotic avocado goblin

     @theruran @a_breakin_glass @chjara it's not as expressive as a univalent type system but that's intentional, canonicity and proof relevance/only definitional *equality* (you can have other equivalences with like setoids etc) are IMO desirable in practical computing, since two different implementations of the same computation are usefully distinct with regard to operational characteristics. (and canonicity just makes interoperation tasks 100x easier)