Homotopy Type Theory
Boolean W-topical dagger 2-poset > history