Constantine Theocharis
constantine@types.pl
Posts
-
Post #2590503
Has anyone studied the (2,2)-category of natural models of type theory? Specifically in reference to (op)lax limits/colimits
-
Post #2590502
It would be nice if proof assistants supported custom LSP semantic highlighting annotations on definitions/postulates. It would really level up embedded DSLs.
-
Post #2103989
I finally found a way to mechanise synthetic Tait computability in Agda where restricting along the syntactic open computes definitionally.. without relying on cubical cofibrations. It amounts to working completely within an indexed universe whose base is open-modal and fibers are closed-modal. Has this been observed before? (full code soon) cc @trebor @jonmsterling @olynch
-
Post #1411891
RE: https://types.pl/@constantine/116040364817905918 Now accepted to FSCD!
-
Post #968742
New paper with @edwinb on a SOGAT approach to erasure for dependent types, where erasure is an open modality: https://cthe.me/erasure-sogat.pdf Turns out this is pretty nice for implementation: having a structural specification means it is clear how to do pattern unification. Demo impl: https://github.com/kontheocharis/erasure-impl