Homotopy Type Theory
Boolean dagger 2-poset > history