Egbert Rijke & Michael Shulman & Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 16(1):Paper No. 2, 79, 2020. https://doi.org/10.23638/LMCS-16(1:2)2020