aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-4/+13
* Library organization and formattingJosh Chen2018-06-271-6/+7
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-0/+15
* Reorganize codeJosh Chen2018-06-091-248/+0
* Symmetry and transitivity done.Josh Chen2018-06-071-3/+26
* But also looser than PairJosh Chen2018-06-071-1/+1
* Nondependent function arrow should bind tighter than the Pi former, but loose...Josh Chen2018-06-071-21/+43
* Code formattingJosh Chen2018-06-051-41/+54
* Proved that the inductor on Sum has the correct type.Josh Chen2018-06-051-17/+31
* Dependent sum done, I think.Josh Chen2018-06-051-28/+40
* Prod_comp should have a type constraint. This also fixes a false proof for th...Josh Chen2018-06-041-22/+31
* Should be final version of Prod. Theorems proving stuff about currying. Rules...Josh Chen2018-06-011-22/+15
* New type rules for dependent product and sum.Josh Chen2018-05-301-12/+29
* Fixed dependent product rules, hopefully final now.Josh Chen2018-05-301-3/+2
* More rigorous rules for Product type. Propositions and proofs all working, bu...Josh Chen2018-05-291-12/+17
* Dependent product rules done and proofs of typing properties so far work. Sta...Josh Chen2018-05-281-27/+54
* pre-system upgrade commitJosh Chen2018-05-231-35/+40
* Added precedences. Need to figure out how to organize metatypes.Josh Chen2018-05-141-13/+12
* Decided to go with no explicit type declarations in object-lambda expressions...Josh Chen2018-05-101-14/+25
* InitJosh Chen2018-05-031-0/+99
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 02:42:15 +0000