aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Cleanups and reorganizationJosh Chen2019-02-221-219/+0
|
* Partway through associativity proof. Lots to work on to make this more usable.Josh Chen2019-02-181-28/+58
|
* Dependent elimator for Eq now has the correct form. Cleaned up theoremsJosh Chen2019-02-171-20/+104
|
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-171-21/+74
| | | | statements. Also misc. cleanups.
* Not sure what advantage is provided by having eta-expanded forms in the ↵Josh Chen2018-09-191-2/+2
| | | | rules. Removing for now.
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen2018-09-181-0/+1
| | | | handling universes. Commit for release 0.1.0!
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-5/+5
|
* Clean up Equal.thy + some other tweaksJosh Chen2018-09-171-37/+22
|
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-16/+16
|\
| * Go back to higher-order application notationJosh Chen2018-09-111-11/+11
|/
* Reorganize methodsJosh Chen2018-08-181-1/+1
|
* Regrouping type rulesJosh Chen2018-08-181-15/+13
|
* Fixed mistake in Equal_elim and proof of rpathcomp_compJosh Chen2018-08-181-1/+1
|
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-1/+1
| | | | Definition of function composition and properties.
* Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen2018-08-141-3/+7
| | | | natural number predecessor function.
* rcompose doneJosh Chen2018-08-131-6/+6
|
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-10/+10
|
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-17/+17
|
* Reorganize theoriesJosh Chen2018-08-041-13/+16
|
* Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen2018-07-111-8/+8
| | | | derivation of "A:U" from "a:A".
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-0/+1
|
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-061-2/+1
|
* Added attributes to type elimination rules, not sure if these will actually ↵Josh Chen2018-07-061-0/+2
| | | | be needed or useful later. Added [comp] attribute to be used by simplification met methods.
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-1/+1
|
* Fix precedence of =Josh Chen2018-06-301-1/+1
|
* EqualityJosh Chen2018-06-301-54/+29
|
* Library organization and formattingJosh Chen2018-06-271-1/+0
|
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-121-75/+79
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-0/+81
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-22 10:27:19 +0000