Modal Descent

Felix Cherubini, Egbert Rijke

Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal f…