aboutsummaryrefslogtreecommitdiff
path: root/EqualProps.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2018-07-11Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen1-5/+8
derivation of "A:U" from "a:A".
2018-07-09Pre-universe implementation commitJosh Chen1-15/+10
2018-07-07Library snapshot. Methods written, everything nicely organized.Josh Chen1-14/+8
2018-07-06Added attributes to type elimination rules, not sure if these will actually ↵Josh Chen1-21/+0
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-25/+25
2018-07-03Rewrote methods: wellformed now two lines, uses named theorems. New, more ↵Josh Chen1-30/+18
powerful derive method. Used these to rewrite proofs.
2018-06-30Proving path composition. Need to set up the Simplifier to simplify ↵Josh Chen1-10/+28
application of object-lambdas to arguments.
2018-06-30EqualityJosh Chen1-0/+90