aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Remove test commit folderJosh Chen2018-08-171-1/+0
* Partway through updating proofs after the change of the function composition ...Josh Chen2018-08-171-46/+11
* Axiomatizations should be definitionsJosh Chen2018-08-171-4/+2
* Make function composition a definition instead of an axiomatization (should n...Josh Chen2018-08-171-9/+1
* Change unnecessary axiomatization to a definitionJosh Chen2018-08-171-2/+2
* Testing with the new theoryJosh Chen2018-08-171-29/+25
* second testJosh Chen2018-08-161-0/+1
* test new machineJosh Chen2018-08-161-0/+2
* Some comments and reorganizationJosh Chen2018-08-162-24/+42
* Merge branch 'master' of github.com:jaycech3n/HoTTJosh Chen2018-08-160-0/+0
|\
| * Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-1613-59/+105
* | Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-1613-59/+105
|/
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-155-101/+93
* Basic compute methodJosh Chen2018-08-155-12/+45
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-157-50/+87
* Function composition, rename path composition to differentiate the two.Josh Chen2018-08-152-20/+36
* Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen2018-08-147-102/+174
* Equality inverse and composition done. Cleaned up methods and method example ...Josh Chen2018-08-145-121/+215
* rcompose doneJosh Chen2018-08-137-78/+105
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-129-56/+108
* Rewriting projection functionsJosh Chen2018-08-082-211/+7
* TweaksJosh Chen2018-08-072-4/+9
* Old application syntax incompatible with EisbachJosh Chen2018-08-077-78/+74
* Experiment with polymorphic dependent eliminators, i.e. we leave type and typ...Josh Chen2018-08-072-14/+14
* Partway through changing function application syntax style.Josh Chen2018-08-067-138/+206
* CoproductJosh Chen2018-08-041-0/+61
* Reorganize theoriesJosh Chen2018-08-045-100/+130
* Unit and Null types. Methods.Josh Chen2018-07-125-19/+73
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-117-70/+63
* Alternative implementation of universes using meta-level numerals.Josh Chen2018-07-111-32/+43
* Pre-universe implementation commitJosh Chen2018-07-096-70/+104
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-077-20/+45
* Methods added and organized!Josh Chen2018-07-071-47/+40
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-063-5/+2
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-067-29/+110
* Trivial changesJosh Chen2018-07-042-7/+8
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-039-205/+133
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-036-121/+117
* Proving path composition. Need to set up the Simplifier to simplify applicati...Josh Chen2018-06-302-10/+29
* Fix precedence of =Josh Chen2018-06-301-1/+1
* EqualityJosh Chen2018-06-303-56/+131
* Finished proofs of projectionsJosh Chen2018-06-302-21/+77
* Add Pair_introJosh Chen2018-06-301-0/+7
* Proving theorems in Proj.thy in a simpler way with wellformedJosh Chen2018-06-281-40/+23
* wellformed method works!!!Josh Chen2018-06-281-6/+6
* wellformed method to automatically prove wellformed judgments derivable from ...Josh Chen2018-06-271-0/+76
* Move projection function definitions out of Sum.thyJosh Chen2018-06-272-170/+197
* Library organization and formattingJosh Chen2018-06-274-9/+10
* Dependent projection properties done.Josh Chen2018-06-181-27/+58
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-183-23/+95
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-18 01:10:08 +0000