Presheaf Models of Relational Modalities in Dependent Type Theory

Andreas Nuyts

This report is an extension of 'A Model of Parametric Dependent Type Theory in Bridge/Path Cubical Sets' (Nuyts, arXiv:1706.04383). The purpose of this text is to prove all technic…