Post #1692983

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