Homotopy Type Theory propositional logic > history

< propositional logic as a dependent type theory