aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2018-06-27Library organization and formattingJosh Chen1-1/+0
2018-06-17Decided on a new proper scheme for type rules using the idea of implicit ↵Josh Chen1-23/+20
well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
2018-06-15projectionsJosh Chen1-0/+3
2018-06-12Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen1-8/+17
formulation in the HoTT book.
2018-06-09Reorganize codeJosh Chen1-9/+44
2018-06-07Symmetry and transitivity done.Josh Chen1-0/+1
2018-06-07Nondependent function arrow should bind tighter than the Pi former, but ↵Josh Chen1-5/+5
looser than equality.
2018-06-05Code formattingJosh Chen1-0/+2
2018-06-05Proved that the inductor on Sum has the correct type.Josh Chen1-27/+50
2018-06-05Dependent sum done, I think.Josh Chen1-0/+2
2018-06-04Prod_comp should have a type constraint. This also fixes a false proof for ↵Josh Chen1-14/+38
the dependent sum projection functions.
2018-06-01Should be final version of Prod. Theorems proving stuff about currying. ↵Josh Chen1-19/+50
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-9/+4
2018-05-30Fixed dependent product rules, hopefully final now.Josh Chen1-72/+27
2018-05-29More rigorous rules for Product type. Propositions and proofs all working, ↵Josh Chen1-12/+55
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-37/+56
Starting on dependent sums.
2018-05-23pre-system upgrade commitJosh Chen1-0/+68