aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Cleanups and reorganizationJosh Chen2019-02-221-16/+12
* 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 han...Josh Chen2018-09-181-4/+5
* 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. Definition...Josh Chen2018-08-161-1/+1
* 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 formulat...Josh Chen2018-06-121-0/+15
* 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 loose...Josh Chen2018-06-071-21/+43
* 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 th...Josh Chen2018-06-041-22/+31
* Should be final version of Prod. Theorems proving stuff about currying. Rules...Josh Chen2018-06-011-22/+15
* 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, bu...Josh Chen2018-05-291-12/+17
* Dependent product rules done and proofs of typing properties so far work. Sta...Josh Chen2018-05-281-27/+54
* 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 expressions...Josh Chen2018-05-101-14/+25
* InitJosh Chen2018-05-031-0/+99
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 16:10:45 +0000