aboutsummaryrefslogtreecommitdiff
path: root/hott/Propositions.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Bad practice huge commit:Josh Chen2021-06-241-2/+6
| | | | | | | 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file
* start hprop stuffJosh Chen2021-04-101-0/+19