aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Derive can prove pathcomp_comp. Fix typo.Josh Chen2018-09-201-1/+1
* proof of associativity of path compositionJosh Chen2018-09-191-3/+8
* Add ROOT. No eta-contractionJosh Chen2018-09-181-0/+2
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...Josh Chen2018-09-181-14/+15
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-3/+1
* Clean up Equal.thy + some other tweaksJosh Chen2018-09-171-1/+1
* Reorganizing theoriesJosh Chen2018-09-171-11/+14
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-47/+40
|\
| * Running into trouble with the polymorphic identity functionJosh Chen2018-09-111-6/+10
| * Go back to higher-order application notationJosh Chen2018-09-111-8/+6
| * Some higher groupoid structure proofsJosh Chen2018-08-301-1/+1
| * Should write the correct rule for Ord_leq_min. Another exercise.Josh Chen2018-08-301-2/+6
| * Add leq relation to meta-ordinals, it helps with proofsJosh Chen2018-08-301-6/+11
* | begin reorganizingJosh Chen2018-09-151-9/+10
|/
* Distinguish the typing judgmentJosh Chen2018-08-181-2/+1
* Regrouping type rulesJosh Chen2018-08-181-1/+0
* Output formattingJosh Chen2018-08-181-1/+1
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-1/+1
* Well-formation rules are back in the methods; new theory synthesizing the nat...Josh Chen2018-08-141-1/+1
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-0/+1
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-4/+0
* Partway through changing function application syntax style.Josh Chen2018-08-061-9/+12
* Reorganize theoriesJosh Chen2018-08-041-35/+41
* Unit and Null types. Methods.Josh Chen2018-07-121-1/+2
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-23/+12
* Alternative implementation of universes using meta-level numerals.Josh Chen2018-07-111-32/+43
* Pre-universe implementation commitJosh Chen2018-07-091-2/+23
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-1/+1
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-3/+7
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-1/+3
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-4/+5
* Library organization and formattingJosh Chen2018-06-271-1/+3
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-181-2/+1
* Removed all [simp] attributes, these will be added later when I set up the si...Josh Chen2018-06-181-1/+1
* Proof of projection functions now harder. Should look up automation methods.Josh Chen2018-06-171-1/+1
* projectionsJosh Chen2018-06-151-27/+13
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-15/+29
* Reorganize codeJosh Chen2018-06-091-0/+52
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 10:05:58 +0000