Directed type theory, with a twist

Fernando Rafael Chu Rivera, Paige Randall North

In recent years, Homotopy Type Theory (HoTT) has had great success both as a foundation of mathematics and as internal language to reason about $\infty$-groupoids (a.k.a. spaces).…