Monthly Archives: December 2017

2dimensional directed type theory

Henosophia TOPOSOPHIA μαθεσις uni√ersalis τοποσοφια MATHESIS οντοποσοφια ενοσοφια Philosophie, théorie des catégories et théorie homotopique des types

« The 2-dimensional directed type theory of Licata and Harper has semantics in 1-categories, with a syntax that distinguishes between co- and contra-variant dependencies; but since the 1-categorical structure is “put in by hand”, it’s not especially synthetic and doesn’t generalize well to higher categories.«

http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf

View original post