aboutsummaryrefslogtreecommitdiff
path: root/Eq.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2019-03-08type lemmas for derived functions should type the functions themselvesJosh Chen1-8/+14
2019-03-06Make functions object-levelJosh Chen1-77/+86
2019-03-03Removed transport section from Eq.thyJosh Chen1-99/+1
2019-03-01change id precedenceJosh Chen1-13/+13
2019-03-01Syntax changes. Transport inverse lemmas.Josh Chen1-18/+70
2019-02-28more convenient syntaxJosh Chen1-68/+91
2019-02-281. Remove all type inference functionality (feature development moving to ano...Josh Chen1-53/+163
2019-02-23more proofs involving equalityJosh Chen1-44/+97
2019-02-23rewrite associativity proofJosh Chen1-17/+16
2019-02-22Cleanups and reorganizationJosh Chen1-10/+17
2019-02-22Proof of pathcomp associativity done. Some commentsJosh Chen1-33/+43
2019-02-18Partway through associativity proof. Lots to work on to make this more usable.Josh Chen1-28/+58
2019-02-17Dependent elimator for Eq now has the correct form. Cleaned up theoremsJosh Chen1-20/+104
2019-02-17Method "quantify" converts product inhabitation into Pure universal statement...Josh Chen1-21/+74
2018-09-19Not sure what advantage is provided by having eta-expanded forms in the rules...Josh Chen1-2/+2
2018-09-18Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...Josh Chen1-0/+1
2018-09-18Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen1-5/+5
2018-09-17Clean up Equal.thy + some other tweaksJosh Chen1-37/+22
2018-09-11Go back to higher-order application notationJosh Chen1-11/+11
2018-08-18Reorganize methodsJosh Chen1-1/+1
2018-08-18Regrouping type rulesJosh Chen1-15/+13
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. Definition...Josh Chen1-1/+1
2018-08-16Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen1-1/+1
2018-08-14Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen1-3/+7
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 der...Josh Chen1-8/+8
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 b...Josh Chen1-0/+2
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 formulat...Josh Chen1-75/+79
2018-06-09Reorganize codeJosh Chen1-0/+81
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 17:08:46 +0000