aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 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 ↵Josh Chen2018-08-171-9/+1
| | | | not need to worry about preconditions)
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-17/+11
| | | | Definition of function composition and properties.
* Rename to distinguish function and path composition; function composition ↵Josh Chen2018-08-151-8/+18
| | | | proofs, which have issues...
* 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 ↵Josh Chen2018-08-071-5/+5
| | | | type family decorations implicit.
* 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 ↵Josh Chen2018-07-111-4/+4
| | | | derivation of "A:U" from "a:A".
* 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 ↵Josh Chen2018-07-061-0/+2
| | | | be needed or useful later. Added [comp] attribute to be used by simplification met methods.
* Trivial changesJosh Chen2018-07-041-1/+1
|
* Rewrote methods: wellformed now two lines, uses named theorems. New, more ↵Josh Chen2018-07-031-2/+1
| | | | powerful derive method. Used these to rewrite proofs.
* Proving path composition. Need to set up the Simplifier to simplify ↵Josh Chen2018-06-301-0/+1
| | | | application of object-lambdas to arguments.
* Finished proofs of projectionsJosh Chen2018-06-301-1/+1
|
* Fixed wrong definition of snd_dep. Proved projection property of snd_dep. ↵Josh Chen2018-06-181-5/+13
| | | | Added type formation rules expressing necessity of the conditions.
* Removed all [simp] attributes, these will be added later when I set up the ↵Josh Chen2018-06-181-12/+19
| | | | simplifier. Proved simplification rule for dependent fst.
* Decided on a new proper scheme for type rules using the idea of implicit ↵Josh Chen2018-06-171-1/+1
| | | | well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-121-6/+13
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-0/+48