Replying to
@jonmsterling@mathstodon.xyz @olynch@mathstodon.xyz @HarrisonGrodin@mathstodon.xyz
Here it is: https://github.com/kontheocharis/synthetait
Remote
Constantine Theocharis
@constantine@types.pl
mastodon 4.8.0-alpha.2+glitch150 Followers
128 Following
18 Posts
Joined February 11, 2025
website:
cthe.me
github:
github.com/kontheocharis
New paper with @edwinb@types.pl 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.
Replying to
@ncf @de_Jong_Tom @ionchy @andrejbauer if only it was also typed… then it would truly live up to its name
Replying to
@julesh@mathstodon.xyz @gallais@mamot.fr
unsafeDestroyWorld
I know Idris is powerful etc but this is too far..
Replying to
@trebor@types.pl Yeah that should be possible. You should also be able to implement the whole signature (opaquely) through a proposition with realignment, rather than postulating everything, and your suggestion would become a theorem.
It would be nice if proof assistants supported custom LSP semantic highlighting annotations on definitions/postulates. It would really level up embedded DSLs.
Replying to
@olynch This is the context former you need to have an “amazing right adjoint” to the open modality. Mitchell Riley’s “Type Theory with a Tiny Object” shows how to do this, but you might also find other formulations useful, eg “Transpension: The Right Adjoint to the Pi-Type”
Replying to
@ncf @rafaelbocquet It is now listed at https://rafaelbocquet.gitlab.io/ as well.. I am not sure if it wasn’t supposed to be accessed, I was given this URL 😅
Replying to
Replying to
@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.
Replying to
@olynch Is your approach based on an inductively defined predicate on types like isStatic? If so, I’m not sure if this would work for this style of erasure where there is a separate sort for erased vs runtime terms, but only one kind of ‘type’. Either way I would be interested to hear more.
Replying to
@ncf Makes sense, I will edit that, thanks.
By relativises I basically mean the ‘contextualisation’ procedure, which in the basic case takes a Tarski universe and turns it into a CwF (but there are a few variations of it that are given in @rafaelbocquet ‘s thesis, one of which is the correspondence between SOGAT and GAT models)
Has anyone studied the (2,2)-category of natural models of type theory? Specifically in reference to (op)lax limits/colimits