aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Methods.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* working towards biinv_imp_qinvJosh Chen2019-03-261-2/+2
|
* Improve automated handling of universes. derive now can automatically handle ↵Josh Chen2019-03-031-2/+3
| | | | more proofs requiring the use of "U i: U (Suc i)", and shouldn't loop as much.
* finished proof of transport_biinvJosh Chen2019-03-011-1/+0
|
* compute method solves subgoals arising from substJosh Chen2019-02-231-6/+8
|
* Cleanups and reorganizationJosh Chen2019-02-221-2/+3
|
* Proof of pathcomp associativity done. Some commentsJosh Chen2019-02-221-22/+19
|
* Method "quantify" converts product inhabitation into Pure universal ↵Josh Chen2019-02-171-8/+21
| | | | statements. Also misc. cleanups.
* Put typing functionality into a .thy and clean up antiquotations, which ↵Josh Chen2019-02-111-0/+5
| | | | results in some reorganization of the theory import structure.
* Clean and comment methods fileJosh Chen2019-01-301-41/+34
|
* Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵Josh Chen2018-09-181-2/+23
| | | | handling universes. Commit for release 0.1.0!
* Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-181-9/+9
|
* Tweak proofJosh Chen2018-09-171-2/+2
|
* Reorganizing theoriesJosh Chen2018-09-171-34/+22
|
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-161-3/+3
|
* Reorganize methodsJosh Chen2018-08-181-19/+23
|
* Regrouping type rulesJosh Chen2018-08-181-3/+2
|
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-1/+1
| | | | Definition of function composition and properties.
* Rename to distinguish function and path composition; function composition ↵Josh Chen2018-08-151-1/+1
| | | | proofs, which have issues...
* Basic compute methodJosh Chen2018-08-151-0/+4
|
* Tweak proof methods, some type rules; add HoTT Book examplesJosh Chen2018-08-151-7/+7
|
* Equality inverse and composition done. Cleaned up methods and method example ↵Josh Chen2018-08-141-42/+25
| | | | theory.
* Commit before testing polymorphic equality eliminatorJosh Chen2018-08-121-2/+2
|
* Rewriting projection functionsJosh Chen2018-08-081-3/+3
|
* Unit and Null types. Methods.Josh Chen2018-07-121-2/+5
|
* Universes implemented. Type rules modified accordingly. No more automatic ↵Josh Chen2018-07-111-6/+5
| | | | derivation of "A:U" from "a:A".
* Pre-universe implementation commitJosh Chen2018-07-091-7/+3
|
* Methods added and organized!Josh Chen2018-07-071-47/+40
|
* Added attributes to type elimination rules, not sure if these will actually ↵Josh Chen2018-07-061-4/+43
| | | | be needed or useful later. Added [comp] attribute to be used by simplification met methods.
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-78/+14
|
* Rewrote methods: wellformed now two lines, uses named theorems. New, more ↵Josh Chen2018-07-031-57/+86
| | | | powerful derive method. Used these to rewrite proofs.
* EqualityJosh Chen2018-06-301-2/+12
|
* wellformed method works!!!Josh Chen2018-06-281-6/+6
|
* wellformed method to automatically prove wellformed judgments derivable from ↵Josh Chen2018-06-271-0/+76
a wellformed judgment
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 17:15:22 +0000