aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
...
* Proof of projection functions now harder. Should look up automation methods.Josh Chen2018-06-171-1/+1
|
* projectionsJosh Chen2018-06-151-27/+13
|
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-121-15/+29
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-0/+52