No description, website, or topics provided.
Agda TeX Other
Latest commit f0b5cc7 Apr 24, 2017 @emblack emblack last last
Permalink
Failed to load latest commit information.
categories mark postulates so I can see what is left Feb 8, 2015
computational-interp stuff Sep 7, 2016
homotopy
lib changed listbijection to be a bijection between lists of different ty… Feb 6, 2017
metatheory andrew Sep 5, 2016
misc stuff Nov 22, 2016
mso last last Apr 24, 2017
oldlib resuccitate partial torus proof from last fall Mar 8, 2013
polymorphism mark postulates so I can see what is left Feb 8, 2015
programming heterogeneous equality Oct 29, 2016
species/notes species notes Oct 14, 2015
.gitignore
README finish library revisions Jan 16, 2013
badpostulates mark postulates so I can see what is left Feb 8, 2015

README

oldlib
 a bunch of stuff using an older version of lib/
 some of this needs to be resuccitated, like joseph's code in applications/torus2

lib
  basic constructions of homotopy type theory

homotopy
  applications of homotopy type theory to formalizing homotopy theory

programming
  applications of homotopy type theory to programming

computational-interp
  code having to do with the computational interpretation or 2tt

misc
  miscellaneous little experiments