aboutsummaryrefslogtreecommitdiff
path: root/ex/HoTT book/Ch1.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* add ROOT fileLars Hupel2018-09-181-50/+0
|
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen2018-09-181-26/+21
| | | | handling universes. Commit for release 0.1.0!
* Should write the correct rule for Ord_leq_min. Another exercise.Josh Chen2018-08-301-0/+12
|
* Regrouping type rulesJosh Chen2018-08-181-2/+1
|
* Misc formattingJosh Chen2018-08-181-1/+1
|
* Some comments and reorganizationJosh Chen2018-08-161-0/+44