aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2018-08-18Fixed mistake in Equal_elim and proof of rpathcomp_compJosh Chen1-1/+1
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-16Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen1-1/+1
Definition of function composition and properties.
2018-08-14Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen1-3/+7
natural number predecessor function.
2018-08-13rcompose doneJosh Chen1-6/+6
2018-08-12Commit before testing polymorphic equality eliminatorJosh Chen1-10/+10
2018-08-07Old application syntax incompatible with EisbachJosh Chen1-17/+17
2018-08-04Reorganize theoriesJosh Chen1-13/+16
2018-07-11Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen1-8/+8
derivation of "A:U" from "a:A".
2018-07-07Library snapshot. Methods written, everything nicely organized.Josh Chen1-0/+1
2018-07-06Remove extra attributes for elimination rules, unneeded for now.Josh Chen1-2/+1
2018-07-06Added attributes to type elimination rules, not sure if these will actually ↵Josh Chen1-0/+2
be needed or useful later. Added [comp] attribute to be used by simplification met methods.
2018-07-03Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen1-1/+1
2018-06-30Fix precedence of =Josh Chen1-1/+1
2018-06-30EqualityJosh Chen1-54/+29
2018-06-27Library organization and formattingJosh Chen1-1/+0
2018-06-12Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen1-75/+79
formulation in the HoTT book.
2018-06-09Reorganize codeJosh Chen1-0/+81
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-03 00:21:09 +0000