@constantine@types.pl

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

2

0

Constantine Theocharis @constantine@types.pl

· 5mo ago

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

1

0

Constantine Theocharis @constantine@types.pl

· 6mo ago

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”

1

0

Constantine Theocharis @constantine@types.pl

· 8mo ago

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 😅

rafaelbocquet.gitlab.io

Rafaël Bocquet’s webpage

1

0

Constantine Theocharis @constantine@types.pl

· 8mo ago

Replying to

@ncf @edwinb Maybe the wording is a bit weird though, it should maybe say “interpreted as (Γ → φ)” because otherwise it sounds like there is a particular unspecified map of type Γ → φ..

0

5

0

Constantine Theocharis @constantine@types.pl

· 8mo ago

Replying to

@NathanielB this is the way

0

Constantine Theocharis @constantine@types.pl

· 5mo ago

Replying to

@bhaktishh life is not the same after vim-surround

0

Constantine Theocharis @constantine@types.pl

· 8mo ago

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.

0

3

0

Constantine Theocharis @constantine@types.pl

· 8mo ago

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.

0

1

0

Constantine Theocharis @constantine@types.pl

· 8mo ago

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)

0

3

0

Constantine Theocharis @constantine@types.pl

· 5mo ago

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

0

1

0