← Feed

Posts

• View post

  Has anyone studied the (2,2)-category of natural models of type theory? Specifically in reference to (op)lax limits/colimits

• View post

  It would be nice if proof assistants supported custom LSP semantic highlighting annotations on definitions/postulates. It would really level up embedded DSLs.

• View post

  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

• View post

  RE: https://types.pl/@constantine/116040364817905918 Now accepted to FSCD!

• View post

  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