index
:
Isabelle-HoTT
master
trying to make Isabelle/HoTT work with Isabelle 2021-1
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
Text remarks
Josh Chen
2019-01-31
1
-3
/
+7
*
Clean and comment methods file
Josh Chen
2019-01-30
1
-41
/
+34
*
Remove "constrained" notation for type families. Clean and document.
Josh Chen
2019-01-30
1
-20
/
+13
*
Begin refactor
Josh Chen
2019-01-30
1
-12
/
+7
*
Derive can prove pathcomp_comp. Fix typo.
Josh Chen
2018-09-20
2
-16
/
+2
*
Application should bind tighter than composition
Josh Chen
2018-09-20
2
-3
/
+3
*
Rename properties of equality + more properties. Output formatting for `
Josh Chen
2018-09-20
2
-1
/
+216
*
Renaming
Josh Chen
2018-09-19
2
-220
/
+0
*
Renaming
Josh Chen
2018-09-19
3
-3
/
+46
*
Not sure what advantage is provided by having eta-expanded forms in the rules...
Josh Chen
2018-09-19
5
-12
/
+12
*
proof of associativity of path composition
Josh Chen
2018-09-19
2
-27
/
+73
*
Merge branch 'larsrh-topic/root'
Josh Chen
2018-09-18
4
-2
/
+27
|
\
|
*
Add ROOT. No eta-contraction
Josh Chen
2018-09-18
2
-2
/
+18
|
*
add ROOT file
Lars Hupel
2018-09-18
3
-2
/
+11
|
/
*
Load Univalence by default
Josh Chen
2018-09-18
1
-0
/
+1
*
Update README.md
Josh Chen
2018-09-18
1
-0
/
+6
*
Update README.md
Josh Chen
2018-09-18
1
-16
/
+0
*
Merge branch 'develop', ready for release 0.1.0
Josh Chen
2018-09-18
19
-1088
/
+588
|
\
|
*
Overhaul of the theory presentations. New methods in HoTT_Methods.thy for han...
Josh Chen
2018-09-18
15
-273
/
+177
|
*
Theories fully reorganized. Well-formedness rules removed. New methods etc.
Josh Chen
2018-09-18
6
-471
/
+158
|
*
Clean up Equal.thy + some other tweaks
Josh Chen
2018-09-17
3
-40
/
+28
|
*
Tweak proof
Josh Chen
2018-09-17
2
-10
/
+7
|
*
Reorganizing theories
Josh Chen
2018-09-17
9
-219
/
+155
|
*
Moved function composition lemmas into Prod.thy
Josh Chen
2018-09-17
2
-108
/
+51
|
*
Reorganized HoTT_Base, updated theories
Josh Chen
2018-09-16
16
-207
/
+635
|
|
\
|
*
|
begin reorganizing
Josh Chen
2018-09-15
2
-10
/
+11
|
*
|
Trying to atomize universal quantification
Josh Chen
2018-08-19
1
-0
/
+9
|
*
|
Higher groupoid structure of types
Josh Chen
2018-08-19
1
-4
/
+67
*
|
|
Update README.md
Josh Chen
2018-09-17
1
-3
/
+1
*
|
|
Update README.md
Josh Chen
2018-09-12
1
-2
/
+2
*
|
|
Update README.md
Josh Chen
2018-09-12
1
-1
/
+1
*
|
|
Add DOI badge
Josh Chen
2018-09-12
1
-0
/
+2
|
|
/
|
/
|
*
|
Final commit before first release
Josh Chen
2018-09-12
1
-1
/
+1
*
|
Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT
Josh Chen
2018-09-12
1
-3
/
+7
|
\
\
|
*
|
Update README.md
Josh Chen
2018-09-11
1
-3
/
+7
*
|
|
Some final touchups before release 0.1 for the MS thesis
Josh Chen
2018-09-12
6
-7
/
+9
|
/
/
*
|
Add the univalence axiom
Josh Chen
2018-09-11
3
-4
/
+71
*
|
Running into trouble with the polymorphic identity function
Josh Chen
2018-09-11
3
-17
/
+80
*
|
Implementing univalence
Josh Chen
2018-09-11
3
-0
/
+81
*
|
Go back to higher-order application notation
Josh Chen
2018-09-11
11
-139
/
+138
*
|
Merge branch 'master' of github.com:jaycech3n/Isabelle-HoTT
Josh Chen
2018-08-30
1
-1
/
+1
|
\
\
|
*
|
Update README.md
Josh Chen
2018-08-30
1
-1
/
+1
*
|
|
Some higher groupoid structure proofs
Josh Chen
2018-08-30
2
-2
/
+56
|
/
/
*
|
Should write the correct rule for Ord_leq_min. Another exercise.
Josh Chen
2018-08-30
2
-2
/
+18
*
|
Add leq relation to meta-ordinals, it helps with proofs
Josh Chen
2018-08-30
2
-7
/
+12
*
|
Rename LICENSE.md to LICENSE
Josh Chen
2018-08-21
1
-0
/
+0
*
|
Create LICENSE.md
Josh Chen
2018-08-21
1
-0
/
+165
|
/
*
Forgot to add the theories for Empty and Unit
Josh Chen
2018-08-18
2
-0
/
+63
*
Distinguish the typing judgment
Josh Chen
2018-08-18
1
-2
/
+1
*
Move Empty and Unit types to their own theories
Josh Chen
2018-08-18
3
-32
/
+2
[next]