aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Decided on a new proper scheme for type rules using the idea of implicit well...Josh Chen2018-06-171-23/+20
* projectionsJosh Chen2018-06-151-0/+3
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-8/+17
* Reorganize codeJosh Chen2018-06-091-9/+44
* Symmetry and transitivity done.Josh Chen2018-06-071-0/+1
* Nondependent function arrow should bind tighter than the Pi former, but loose...Josh Chen2018-06-071-5/+5
* Code formattingJosh Chen2018-06-051-0/+2
* Proved that the inductor on Sum has the correct type.Josh Chen2018-06-051-27/+50
* Dependent sum done, I think.Josh Chen2018-06-051-0/+2
* Prod_comp should have a type constraint. This also fixes a false proof for th...Josh Chen2018-06-041-14/+38
* Should be final version of Prod. Theorems proving stuff about currying. Rules...Josh Chen2018-06-011-19/+50
* New type rules for dependent product and sum.Josh Chen2018-05-301-9/+4
* Fixed dependent product rules, hopefully final now.Josh Chen2018-05-301-72/+27
* More rigorous rules for Product type. Propositions and proofs all working, bu...Josh Chen2018-05-291-12/+55
* Dependent product rules done and proofs of typing properties so far work. Sta...Josh Chen2018-05-281-37/+56
* pre-system upgrade commitJosh Chen2018-05-231-0/+68