aboutsummaryrefslogtreecommitdiff
path: root/EqualProps.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Axiomatizations should be definitionsJosh Chen2018-08-171-4/+2
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-1/+1
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-151-20/+20
* Basic compute methodJosh Chen2018-08-151-6/+6
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-151-29/+29
* Function composition, rename path composition to differentiate the two.Josh Chen2018-08-151-20/+20
* Equality inverse and composition done. Cleaned up methods and method example ...Josh Chen2018-08-141-40/+152
* rcompose doneJosh Chen2018-08-131-18/+60
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-13/+16
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-5/+8
* 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 b...Josh Chen2018-07-061-21/+0
* 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 pow...Josh Chen2018-07-031-30/+18
* Proving path composition. Need to set up the Simplifier to simplify applicati...Josh Chen2018-06-301-10/+28
* EqualityJosh Chen2018-06-301-0/+90
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-29 10:08:23 +0000