less prototype, less bad code implementation of CCHM type theory
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
Abigail 62459c81dc Remove `(φ = i0) as p` syntax + clean up proof of univalence + formalise theorems 4.7.6, 4.7.7, 7.2.2 2 days ago
src Remove `(φ = i0) as p` syntax + clean up proof of univalence + formalise theorems 4.7.6, 4.7.7, 7.2.2 2 days ago
.gitignore initial commit w/ lexer & parser 2 months ago
LICENSE initial commit w/ lexer & parser 2 months ago
README.md initial commit w/ lexer & parser 2 months ago
Setup.hs asfjhkdgf fix stuff?? 3 weeks ago
cubical.cabal optimise transport in Glue using gcomp 2 weeks ago
hie.yaml initial commit w/ lexer & parser 2 months ago
intro.tt Remove `(φ = i0) as p` syntax + clean up proof of univalence + formalise theorems 4.7.6, 4.7.7, 7.2.2 2 days ago
stack.yaml Add strict equality 1 month ago
stack.yaml.lock Add strict equality 1 month ago

README.md

cubical