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