aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* RenamingJosh Chen2018-09-191-2/+2
|
* Load Univalence by defaultJosh Chen2018-09-181-0/+1
|
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen2018-09-181-4/+5
| | | | handling universes. Commit for release 0.1.0!
* Clean up Equal.thy + some other tweaksJosh Chen2018-09-171-2/+5
|
* Reorganizing theoriesJosh Chen2018-09-171-1/+1
|
* Move Empty and Unit types to their own theoriesJosh Chen2018-08-181-0/+2
|
* Reorganize methodsJosh Chen2018-08-181-4/+4
|
* Regrouping type rulesJosh Chen2018-08-181-5/+16
|
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-1/+1
| | | | Definition of function composition and properties.
* Partway through changing function application syntax style.Josh Chen2018-08-061-1/+3
|
* Pre-universe implementation commitJosh Chen2018-07-091-1/+1
|
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-1/+0
|
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-4/+13
|
* Library organization and formattingJosh Chen2018-06-271-6/+7
|
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-121-0/+15
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-248/+0
|
* Symmetry and transitivity done.Josh Chen2018-06-071-3/+26
|
* But also looser than PairJosh Chen2018-06-071-1/+1
|
* Nondependent function arrow should bind tighter than the Pi former, but ↵Josh Chen2018-06-071-21/+43
| | | | looser than equality.
* Code formattingJosh Chen2018-06-051-41/+54
|
* Proved that the inductor on Sum has the correct type.Josh Chen2018-06-051-17/+31
|
* Dependent sum done, I think.Josh Chen2018-06-051-28/+40
|
* Prod_comp should have a type constraint. This also fixes a false proof for ↵Josh Chen2018-06-041-22/+31
| | | | the dependent sum projection functions.
* Should be final version of Prod. Theorems proving stuff about currying. ↵Josh Chen2018-06-011-22/+15
| | | | Rules for Sum, going to change them to use object-level arguments more.
* New type rules for dependent product and sum.Josh Chen2018-05-301-12/+29
|
* Fixed dependent product rules, hopefully final now.Josh Chen2018-05-301-3/+2
|
* More rigorous rules for Product type. Propositions and proofs all working, ↵Josh Chen2018-05-291-12/+17
| | | | but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions.
* Dependent product rules done and proofs of typing properties so far work. ↵Josh Chen2018-05-281-27/+54
| | | | Starting on dependent sums.
* pre-system upgrade commitJosh Chen2018-05-231-35/+40
|
* Added precedences. Need to figure out how to organize metatypes.Josh Chen2018-05-141-13/+12
|
* Decided to go with no explicit type declarations in object-lambda ↵Josh Chen2018-05-101-14/+25
| | | | expressions. Everything in the proof stuff is working at the moment.
* InitJosh Chen2018-05-031-0/+99