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
path:
root
/
EqualProps.thy
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2018-09-12
Some final touchups before release 0.1 for the MS thesis
Josh Chen
1
-2
/
+2
2018-09-11
Add the univalence axiom
Josh Chen
1
-0
/
+2
2018-09-11
Running into trouble with the polymorphic identity function
Josh Chen
1
-0
/
+15
2018-09-11
Implementing univalence
Josh Chen
1
-0
/
+5
2018-09-11
Go back to higher-order application notation
Josh Chen
1
-42
/
+43
2018-08-30
Some higher groupoid structure proofs
Josh Chen
1
-1
/
+55
2018-08-18
Reorganize methods
Josh Chen
1
-33
/
+33
2018-08-18
Regrouping type rules
Josh Chen
1
-2
/
+1
2018-08-18
Fixed mistake in Equal_elim and proof of rpathcomp_comp
Josh Chen
1
-25
/
+25
2018-08-17
Axiomatizations should be definitions
Josh Chen
1
-4
/
+2
2018-08-16
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
1
-1
/
+1
2018-08-16
Prod.thy now has the correct definitional equality structure rule. Definition...
Josh Chen
1
-1
/
+1
2018-08-15
Rename to distinguish function and path composition; function composition pro...
Josh Chen
1
-20
/
+20
2018-08-15
Basic compute method
Josh Chen
1
-6
/
+6
2018-08-15
Tweak proof methods, some type rules; add HoTT Book examples
Josh Chen
1
-29
/
+29
2018-08-15
Function composition, rename path composition to differentiate the two.
Josh Chen
1
-20
/
+20
2018-08-14
Equality inverse and composition done. Cleaned up methods and method example ...
Josh Chen
1
-40
/
+152
2018-08-13
rcompose done
Josh Chen
1
-18
/
+60
2018-08-12
Commit before testing polymorphic equality eliminator
Josh Chen
1
-13
/
+16
2018-07-11
Universes implemented. Type rules modified accordingly. No more automatic der...
Josh Chen
1
-5
/
+8
2018-07-09
Pre-universe implementation commit
Josh Chen
1
-15
/
+10
2018-07-07
Library snapshot. Methods written, everything nicely organized.
Josh Chen
1
-14
/
+8
2018-07-06
Added attributes to type elimination rules, not sure if these will actually b...
Josh Chen
1
-21
/
+0
2018-07-03
Refactor HoTT_Methods.thy, proved more stuff with new methods.
Josh Chen
1
-25
/
+25
2018-07-03
Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...
Josh Chen
1
-30
/
+18
2018-06-30
Proving path composition. Need to set up the Simplifier to simplify applicati...
Josh Chen
1
-10
/
+28
2018-06-30
Equality
Josh Chen
1
-0
/
+90