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