aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Moved function composition lemmas into Prod.thyJosh Chen2018-09-172-108/+51
|
* Reorganized HoTT_Base, updated theoriesJosh Chen2018-09-1616-207/+635
|\
| * 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
| |
* | 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
|/
* Forgot to add the theories for Empty and UnitJosh Chen2018-08-182-0/+63
|
* Distinguish the typing judgmentJosh Chen2018-08-181-2/+1
|
* Move Empty and Unit types to their own theoriesJosh Chen2018-08-183-32/+2
|
* .gitignoreJosh Chen2018-08-181-0/+7
|
* Update Test.thyJosh Chen2018-08-181-12/+12
|
* Reorganize methodsJosh Chen2018-08-1813-94/+98
|
* Regrouping type rulesJosh Chen2018-08-1816-108/+102
|
* HoTT_Test.thy should go in test/Josh Chen2018-08-181-1/+1
|
* Comments on subgoal test theoryJosh Chen2018-08-181-23/+29
|
* RenameJosh Chen2018-08-181-1/+2
|
* .gitignoreJosh Chen2018-08-181-0/+1
|
* Test theoriesJosh Chen2018-08-182-9/+64
|
* Misc formattingJosh Chen2018-08-183-3/+2
|
* Output formattingJosh Chen2018-08-181-1/+1
|
* Ignore more filesJosh Chen2018-08-181-0/+3
|
* Update licenseJosh Chen2018-08-181-1/+1
|
* Update test fileJosh Chen2018-08-181-113/+19
|
* Fixed mistake in Equal_elim and proof of rpathcomp_compJosh Chen2018-08-182-26/+26
|
* Update README.mdJosh Chen2018-08-171-9/+5
|
* Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTTJosh Chen2018-08-171-2/+3
|\
| * Update README.mdJosh Chen2018-08-171-2/+3
| |
* | Fix silly mistakes in Coprod.thyJosh Chen2018-08-171-10/+10
| |
* | CleanupsJosh Chen2018-08-171-4/+4
|/
* Merge branch 'master' of github.com:jaycech3n/HoTTJosh Chen2018-08-171-0/+22
|\
| * Update README.mdJosh Chen2018-08-171-1/+6
| |
| * Add contactJosh Chen2018-08-171-1/+1
| |
| * Update README.mdJosh Chen2018-08-171-1/+1
| |
| * Update README.mdJosh Chen2018-08-171-1/+2
| |
| * Create README.mdJosh Chen2018-08-171-0/+16
| |
* | Properties of function compositionJosh Chen2018-08-171-24/+5
|/
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-06 13:57:30 +0000