aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy (unfollow)
Commit message (Collapse)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 ↵Josh Chen1-0/+15
formulation in the HoTT book.
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 ↵Josh Chen1-21/+43
looser than equality.
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 ↵Josh Chen1-22/+31
the dependent sum projection functions.
2018-06-01Should be final version of Prod. Theorems proving stuff about currying. ↵Josh Chen1-22/+15
Rules for Sum, going to change them to use object-level arguments more.
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, ↵Josh Chen1-12/+17
but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions.
2018-05-28Dependent product rules done and proofs of typing properties so far work. ↵Josh Chen1-27/+54
Starting on dependent sums.
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 ↵Josh Chen1-14/+25
expressions. Everything in the proof stuff is working at the moment.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:28:35 +0000