Realising Intensional S4 and GL Modalities (with cubical-mini) This is a port of https://github.com/L-TChen/provability to the cubical-mini library.