Realising Intensional S4 and GL Modalities

This repo contains the manuscript (source/pdf) and proofs which are formalised in Agda 2.6.2 with the Cubical library d5030a9.