aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
| * 1. Change syntax to rely less on unicode/control symbols.Josh Chen2019-02-043-53/+116
| * Text remarksJosh Chen2019-01-311-3/+7
| * Clean and comment methods fileJosh Chen2019-01-301-41/+34
| * Remove "constrained" notation for type families. Clean and document.Josh Chen2019-01-301-20/+13
| * Begin refactorJosh Chen2019-01-301-12/+7
* | Update README.mdJosh Chen2018-09-201-1/+1
|/
* Derive can prove pathcomp_comp. Fix typo.Josh Chen2018-09-202-16/+2
* Application should bind tighter than compositionJosh Chen2018-09-202-3/+3
* Rename properties of equality + more properties. Output formatting for `Josh Chen2018-09-202-1/+216
* RenamingJosh Chen2018-09-192-220/+0
* RenamingJosh Chen2018-09-193-3/+46
* Not sure what advantage is provided by having eta-expanded forms in the rules...Josh Chen2018-09-195-12/+12
* proof of associativity of path compositionJosh Chen2018-09-192-27/+73
* Merge branch 'larsrh-topic/root'Josh Chen2018-09-184-2/+27
|\
| * Add ROOT. No eta-contractionJosh Chen2018-09-182-2/+18
| * add ROOT fileLars Hupel2018-09-183-2/+11
|/
* Load Univalence by defaultJosh Chen2018-09-181-0/+1
* Update README.mdJosh Chen2018-09-181-0/+6
* Update README.mdJosh Chen2018-09-181-16/+0
* Merge branch 'develop', ready for release 0.1.0Josh Chen2018-09-1819-1088/+588
|\
| * Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...Josh Chen2018-09-1815-273/+177
| * Theories fully reorganized. Well-formedness rules removed. New methods etc.Josh Chen2018-09-186-471/+158
| * Clean up Equal.thy + some other tweaksJosh Chen2018-09-173-40/+28
| * Tweak proofJosh Chen2018-09-172-10/+7
| * Reorganizing theoriesJosh Chen2018-09-179-219/+155
| * Moved function composition lemmas into Prod.thyJosh Chen2018-09-172-108/+51
| * Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-1616-207/+635
| |\
| * | begin reorganizingJosh Chen2018-09-152-10/+11
| * | Trying to atomize universal quantificationJosh Chen2018-08-191-0/+9
| * | Higher groupoid structure of typesJosh Chen2018-08-191-4/+67
* | | Update README.mdJosh Chen2018-09-171-3/+1
* | | Update README.mdJosh Chen2018-09-121-2/+2
* | | Update README.mdJosh Chen2018-09-121-1/+1
* | | Add DOI badgeJosh Chen2018-09-121-0/+2
| |/ |/|
* | Final commit before first releaseJosh Chen2018-09-121-1/+1
* | Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTTJosh Chen2018-09-121-3/+7
|\ \
| * | Update README.mdJosh Chen2018-09-111-3/+7
* | | Some final touchups before release 0.1 for the MS thesisJosh Chen2018-09-126-7/+9
|/ /
* | Add the univalence axiomJosh Chen2018-09-113-4/+71
* | Running into trouble with the polymorphic identity functionJosh Chen2018-09-113-17/+80
* | Implementing univalenceJosh Chen2018-09-113-0/+81
* | Go back to higher-order application notationJosh Chen2018-09-1111-139/+138
* | Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTTJosh Chen2018-08-301-1/+1
|\ \
| * | Update README.mdJosh Chen2018-08-301-1/+1
* | | Some higher groupoid structure proofsJosh Chen2018-08-302-2/+56
|/ /
* | Should write the correct rule for Ord_leq_min. Another exercise.Josh Chen2018-08-302-2/+18
* | Add leq relation to meta-ordinals, it helps with proofsJosh Chen2018-08-302-7/+12
* | Rename LICENSE.md to LICENSEJosh Chen2018-08-211-0/+0
* | Create LICENSE.mdJosh Chen2018-08-211-0/+165
|/
* Forgot to add the theories for Empty and UnitJosh Chen2018-08-182-0/+63
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-19 23:38:33 +0000