|
74ddb6fd94
|
move
|
2024-10-15 10:51:47 -05:00 |
|
|
84bd2a2b85
|
wip lemma 4.1.5
|
2024-10-15 01:29:02 -05:00 |
|
|
e64326c1c3
|
LES
|
2024-10-15 00:02:12 -05:00 |
|
|
ce6a6f734a
|
remove existing stuff
|
2024-10-15 00:00:27 -05:00 |
|
|
45fa777765
|
closes #31
|
2024-10-14 23:53:52 -05:00 |
|
|
4ef8cf0dc2
|
closes #33
|
2024-10-14 23:33:54 -05:00 |
|
|
750e9a218b
|
closes #30
|
2024-10-14 21:10:08 -05:00 |
|
|
ba99d0714b
|
wtf
|
2024-10-14 20:35:07 -05:00 |
|
|
7d6635dcaa
|
wip
|
2024-10-14 19:58:22 -05:00 |
|
|
c1bc1659c4
|
some work
|
2024-10-12 00:03:02 -05:00 |
|
|
65f9ec18c5
|
LES definition similar to the one used by Floris, closes #25
|
2024-10-10 04:41:21 -05:00 |
|
|
705372bd9c
|
wip
|
2024-10-08 04:47:55 -05:00 |
|
|
78fe433b0d
|
complete this for now
|
2024-10-02 20:32:00 -05:00 |
|
|
fe2eedeed2
|
agda (Agda version 2.7.0) hangs on src/CubicalHott/Theorem8-1.agda
|
2024-10-02 18:42:17 -05:00 |
|
|
2745850cfd
|
wip
|
2024-10-02 04:04:24 -05:00 |
|
|
085f146252
|
wip
|
2024-10-02 01:43:05 -05:00 |
|
|
aba838f901
|
more proofs
|
2024-09-27 13:50:18 -05:00 |
|
|
dcfc5e58f4
|
wip
|
2024-09-26 14:18:52 -05:00 |
|
|
e415340890
|
add
|
2024-09-25 14:26:13 -05:00 |
|
|
922455701b
|
exercises3
|
2024-09-25 14:25:22 -05:00 |
|
|
4f2c25cf44
|
6.4.2
|
2024-09-24 23:59:10 -05:00 |
|
|
056d9fd2e8
|
prove 6.4.1
|
2024-09-24 23:39:38 -05:00 |
|
|
43cad1c4bd
|
prove example 3.1.9
|
2024-09-24 22:33:54 -05:00 |
|
|
72f0d83a53
|
add lemma 6.5.1
|
2024-09-20 15:32:02 -05:00 |
|
|
9e1da47565
|
wip
|
2024-09-18 06:44:37 -05:00 |
|
|
81fb1d0c77
|
wtf
|
2024-09-15 19:40:25 -05:00 |
|
|
c1788c20fb
|
a
|
2024-09-15 19:40:10 -05:00 |
|
|
8ecbcefe92
|
cubical stuff
|
2024-09-15 19:40:04 -05:00 |
|
|
1a06c10bb5
|
updates
|
2024-09-15 17:39:30 -05:00 |
|
|
f10e3a09b9
|
wtf
|
2024-08-23 21:02:50 -05:00 |
|
|
73a58bd2c2
|
ch2
|
2024-08-23 20:18:40 -05:00 |
|
|
c84f1f8958
|
add pierce book
|
2024-08-21 11:15:18 -05:00 |
|
|
1c5a7e692e
|
susp
|
2024-08-15 14:05:11 -05:00 |
|
|
7ebaf615b0
|
the cubical stuff
|
2024-08-15 04:40:01 -05:00 |
|
|
040a68bc2a
|
wip
|
2024-08-09 04:55:32 -05:00 |
|
|
12beca17dc
|
remove existing
|
2024-08-09 04:28:50 -05:00 |
|
|
e0f6ba0477
|
remove cubical hott folder
|
2024-08-06 17:13:37 -04:00 |
|
|
491b1b87b0
|
wip
|
2024-08-05 11:17:04 -04:00 |
|
|
3ffdaf1fcb
|
updates
|
2024-08-01 02:36:13 -05:00 |
|
|
e41548a6f9
|
update
|
2024-07-30 09:29:03 -05:00 |
|
|
e2212f7999
|
update
|
2024-07-27 22:20:41 -05:00 |
|
|
5d3ebb119b
|
wip
|
2024-07-26 23:24:55 -05:00 |
|
|
a0906b6bff
|
update
|
2024-07-26 23:22:29 -05:00 |
|
|
c8ddc593bc
|
nya
|
2024-07-25 07:31:02 -05:00 |
|
|
50d8ce8453
|
wip
|
2024-07-25 05:28:30 -05:00 |
|
|
a2dbafb324
|
wip
|
2024-07-24 21:18:14 -05:00 |
|
|
acbb85481f
|
exercise 2.4
|
2024-07-24 21:16:47 -05:00 |
|
|
94609e69f9
|
wip
|
2024-07-22 14:43:05 -05:00 |
|
|
3763a1f062
|
yak shaving
|
2024-07-22 14:43:01 -05:00 |
|
|
61dc53cf32
|
wip 2.7.4
|
2024-07-21 14:45:33 -05:00 |
|