https://github.com/jaycech3n/Isabelle-HoTT
Tip revision: b01b8ee0f3472cb728f09463d0620ac8b8066bcb authored by Josh Chen on 27 March 2019, 13:41:16 UTC
More progress. I think we are reaching the limit of what can be conveniently proved with the current implementation.
More progress. I think we are reaching the limit of what can be conveniently proved with the current implementation.
Tip revision: b01b8ee
File | Mode | Size |
---|---|---|
ex | ||
tests | ||
.gitignore | -rw-r--r-- | 122 bytes |
Eq.thy | -rw-r--r-- | 13.7 KB |
Equivalence.thy | -rw-r--r-- | 8.9 KB |
HoTT.thy | -rw-r--r-- | 628 bytes |
HoTT_Base.thy | -rw-r--r-- | 3.4 KB |
HoTT_Methods.thy | -rw-r--r-- | 3.3 KB |
LICENSE | -rw-r--r-- | 7.5 KB |
More_Types.thy | -rw-r--r-- | 2.4 KB |
Nat.thy | -rw-r--r-- | 1.2 KB |
Prod.thy | -rw-r--r-- | 6.3 KB |
Projections.thy | -rw-r--r-- | 1.2 KB |
README.md | -rw-r--r-- | 1.3 KB |
ROOT | -rw-r--r-- | 657 bytes |
Sum.thy | -rw-r--r-- | 1.9 KB |
Type_Families.thy | -rw-r--r-- | 6.5 KB |
Univalence.thy | -rw-r--r-- | 1.9 KB |