aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Prod_comp should have a type constraint. This also fixes a false proof for th...Josh Chen2018-06-041-14/+38
* Should be final version of Prod. Theorems proving stuff about currying. Rules...Josh Chen2018-06-011-19/+50
* New type rules for dependent product and sum.Josh Chen2018-05-301-9/+4
* Fixed dependent product rules, hopefully final now.Josh Chen2018-05-301-72/+27
* 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