aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* More rigorous rules for Product type. Propositions and proofs all working, bu...Josh Chen2018-05-291-12/+55
* Dependent product rules done and proofs of typing properties so far work. Sta...Josh Chen2018-05-281-37/+56
* pre-system upgrade commitJosh Chen2018-05-231-0/+68