Post #1490091
2026-04-09 20:33 UTC
Modal type theory people:
Given a judgmental proposition P (that is, not necessarily a type, a meta-level proposition), there is an open modality associated to it which looks like (P -> A), this is right adjoint to adding a proof of P to the context. So far, so good.
I want to now instead have a context formation operator which acts like (P -> Γ). My intuition here is that (P -> Γ) "locks" the context Γ, and Γ,P "unlocks" the context. This seems to make sense because (P -> Γ,P) = (P -> Γ), (locking something unlocked is the same as locking the original thing) and (P -> Γ),P = Γ,P (unlocking something that has been locked is the same as unlocking the original thing).
Now, I don't expect (P -> Γ) to have a further right adjoint (I'm using it for a different purpose). But is this a kind of context operation that people have looked at?
Replies (3)
-
@SamToth@mathstodon.xyz 2026-04-09 20:57
@olynch Maybe you already had this in mind and it doesn’t work in your situation for some reason but Mitchell Riley considers this context operation in “a type theory with a tiny object”. Of course he is interested in the right adjoint as well, and he only considers the case where P is actually a type.
-
@constantine@types.pl 2026-04-09 21:13
@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”
-
@avmu@mathstodon.xyz 2026-04-10 05:31
@anuytstt