aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2018-09-19RenamingJosh Chen1-2/+2
2018-09-18Load Univalence by defaultJosh Chen1-0/+1
2018-09-18Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen1-4/+5
handling universes. Commit for release 0.1.0!
2018-09-17Clean up Equal.thy + some other tweaksJosh Chen1-2/+5
2018-09-17Reorganizing theoriesJosh Chen1-1/+1
2018-08-18Move Empty and Unit types to their own theoriesJosh Chen1-0/+2
2018-08-18Reorganize methodsJosh Chen1-4/+4
2018-08-18Regrouping type rulesJosh Chen1-5/+16
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-06Partway through changing function application syntax style.Josh Chen1-1/+3
2018-07-09Pre-universe implementation commitJosh Chen1-1/+1
2018-07-07Library snapshot. Methods written, everything nicely organized.Josh Chen1-1/+0
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-11-03 05:14:16 +0000