aboutsummaryrefslogtreecommitdiff
path: root/Proj.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Change unnecessary axiomatization to a definitionJosh Chen2018-08-171-2/+2
|
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-1/+1
| | | | Definition of function composition and properties.
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-151-6/+6
|
* Well-formation rules are back in the methods; new theory synthesizing the ↵Josh Chen2018-08-141-4/+2
| | | | natural number predecessor function.
* Equality inverse and composition done. Cleaned up methods and method example ↵Josh Chen2018-08-141-20/+12
| | | | theory.
* rcompose doneJosh Chen2018-08-131-6/+13
|
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-2/+43
|
* Rewriting projection functionsJosh Chen2018-08-081-208/+4
|
* TweaksJosh Chen2018-08-071-4/+3
|
* Partway through changing function application syntax style.Josh Chen2018-08-061-6/+22
|
* Reorganize theoriesJosh Chen2018-08-041-8/+22
|
* Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen2018-07-111-8/+18
| | | | derivation of "A:U" from "a:A".
* Pre-universe implementation commitJosh Chen2018-07-091-25/+16
|
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-3/+32
|
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-74/+30
|
* Rewrote methods: wellformed now two lines, uses named theorems. New, more ↵Josh Chen2018-07-031-27/+6
| | | | powerful derive method. Used these to rewrite proofs.
* Finished proofs of projectionsJosh Chen2018-06-301-20/+76
|
* Proving theorems in Proj.thy in a simpler way with wellformedJosh Chen2018-06-281-40/+23
|
* Move projection function definitions out of Sum.thyJosh Chen2018-06-271-0/+196
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-16 20:06:08 +0000