aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Application should bind tighter than compositionJosh Chen2018-09-201-1/+1
* Rename properties of equality + more properties. Output formatting for `Josh Chen2018-09-201-1/+1
* Not sure what advantage is provided by having eta-expanded forms in the rules...Josh Chen2018-09-191-2/+2
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...Josh Chen2018-09-181-0/+1
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-2/+3
* Moved function composition lemmas into Prod.thyJosh Chen2018-09-171-51/+51
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-23/+19
|\
| * Implementing univalenceJosh Chen2018-09-111-0/+5
| * Go back to higher-order application notationJosh Chen2018-09-111-11/+11
* | Trying to atomize universal quantificationJosh Chen2018-08-191-0/+9
|/
* Move Empty and Unit types to their own theoriesJosh Chen2018-08-181-19/+0
* Reorganize methodsJosh Chen2018-08-181-2/+2
* Regrouping type rulesJosh Chen2018-08-181-12/+12
* Make function composition a definition instead of an axiomatization (should n...Josh Chen2018-08-171-9/+1
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-17/+11
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-151-8/+18
* Basic compute methodJosh Chen2018-08-151-1/+1
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-151-1/+1
* Function composition, rename path composition to differentiate the two.Josh Chen2018-08-151-0/+16
* rcompose doneJosh Chen2018-08-131-14/+8
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-10/+12
* Old application syntax incompatible with EisbachJosh Chen2018-08-071-6/+6
* Experiment with polymorphic dependent eliminators, i.e. we leave type and typ...Josh Chen2018-08-071-5/+5
* Partway through changing function application syntax style.Josh Chen2018-08-061-17/+17
* Reorganize theoriesJosh Chen2018-08-041-26/+30
* Unit and Null types. Methods.Josh Chen2018-07-121-0/+19
* Universes implemented. Type rules modified accordingly. No more automatic der...Josh Chen2018-07-111-4/+4
* Library snapshot. Methods written, everything nicely organized.Josh Chen2018-07-071-0/+1
* Remove extra attributes for elimination rules, unneeded for now.Josh Chen2018-07-061-2/+1
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-0/+2
* Trivial changesJosh Chen2018-07-041-1/+1
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-2/+1
* Proving path composition. Need to set up the Simplifier to simplify applicati...Josh Chen2018-06-301-0/+1
* Finished proofs of projectionsJosh Chen2018-06-301-1/+1
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Add...Josh Chen2018-06-181-5/+13
* Removed all [simp] attributes, these will be added later when I set up the si...Josh Chen2018-06-181-12/+19
* Decided on a new proper scheme for type rules using the idea of implicit well...Josh Chen2018-06-171-1/+1
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-6/+13
* Reorganize codeJosh Chen2018-06-091-0/+48