 Frederik Hanghøj Iversen
|
b116247702
|
Kleisli monads are groupoids
|
2018-05-22 16:18:22 +02:00 |
|
|
Frederik Hanghøj Iversen
|
e7f40eed8a
|
Scaffolding for proving groupoid for monads
|
2018-05-22 15:40:30 +02:00 |
|
|
Frederik Hanghøj Iversen
|
1f2b105f9d
|
Provide grpdPiImpl
|
2018-05-22 14:43:21 +02:00 |
|
|
Frederik Hanghøj Iversen
|
1683178f1c
|
Ignore index-files
|
2018-05-22 13:48:30 +02:00 |
|
|
Frederik Hanghøj Iversen
|
01159930de
|
Add section on functors and natural transformations
Also do not use ugly overbar
|
2018-05-22 13:45:52 +02:00 |
|
|
Frederik Hanghøj Iversen
|
2fce963072
|
TENTATIVE COMMIT
|
2018-05-18 13:14:41 +02:00 |
|
|
Frederik Hanghøj Iversen
|
d4dc125fb0
|
Merge remote-tracking branch 'Saizan/benchmark' into dev
|
2018-05-16 11:38:12 +02:00 |
|
|
Frederik Hanghøj Iversen
|
1c0b0d9db2
|
Small changes
|
2018-05-16 11:36:26 +02:00 |
|
|
Frederik Hanghøj Iversen
|
4073d70189
|
Add note about constructive intepretation of univalence
|
2018-05-16 11:03:34 +02:00 |
|
|
Frederik Hanghøj Iversen
|
be88602d24
|
Fix spacing after 'e.g.' and 'i.e.'
|
2018-05-16 11:01:07 +02:00 |
|
Andrea Vezzosi
|
47c881ba2a
|
Voe: gone back to equational reasoning, as it's fairly cheap now.
|
2018-05-16 10:50:56 +02:00 |
|
|
Andrea Vezzosi
|
9f7a13b5da
|
no-eta-equality for monads speeds up Voevodsky
|
2018-05-16 10:41:41 +02:00 |
|
|
Frederik Hanghøj Iversen
|
d33c814e78
|
Add introduction
|
2018-05-15 18:36:33 +02:00 |
|
|
Andrea Vezzosi
|
c75a1d5d8b
|
commented out code with holes
|
2018-05-15 17:21:57 +02:00 |
|
|
Frederik Hanghøj Iversen
|
8a0ea9f4a5
|
Use darkorange for all bordercolors
|
2018-05-15 17:11:01 +02:00 |
|
|
Frederik Hanghøj Iversen
|
21363dbb78
|
Move opposite- and span- category to own modules
|
2018-05-15 16:38:07 +02:00 |
|
|
Frederik Hanghøj Iversen
|
aced19e990
|
Various changes proposed by Andreas
|
2018-05-15 16:08:29 +02:00 |
|
|
Frederik Hanghøj Iversen
|
4d73514ab5
|
Use long name
|
2018-05-14 11:50:14 +02:00 |
|
|
Frederik Hanghøj Iversen
|
30cf0bb765
|
Add additional example of pathJ
|
2018-05-11 13:09:03 +02:00 |
|
|
Frederik Hanghøj Iversen
|
058f3c15a8
|
Provide example of using pathJ
|
2018-05-10 15:29:56 +02:00 |
|
|
Frederik Hanghøj Iversen
|
513d91ae4f
|
Merge branch 'dev'
|
2018-05-10 14:29:41 +02:00 |
|
|
Frederik Hanghøj Iversen
|
3574ebc323
|
Add abstract
|
2018-05-10 14:28:54 +02:00 |
|
|
Frederik Hanghøj Iversen
|
3d618c001b
|
Layout headache
|
2018-05-10 14:10:11 +02:00 |
|
|
Frederik Hanghøj Iversen
|
ac6e838e48
|
Move package config to packages.tex
|
2018-05-10 13:11:07 +02:00 |
|
|
Frederik Hanghøj Iversen
|
00df3ccb45
|
Add conclusion
|
2018-05-10 12:40:39 +02:00 |
|
|
Frederik Hanghøj Iversen
|
258aa3d0e4
|
Write conclusion
|
2018-05-10 12:19:44 +02:00 |
|
|
Frederik Hanghøj Iversen
|
616d85351a
|
Remove all my beloved contractions :(
|
2018-05-09 18:47:12 +02:00 |
|
|
Frederik Hanghøj Iversen
|
34798632f2
|
Fix its it's mistakes
|
2018-05-09 18:34:05 +02:00 |
|
|
Frederik Hanghøj Iversen
|
bc8309c0cd
|
Only index some things, change crossref to citation
|
2018-05-09 18:29:44 +02:00 |
|
|
Frederik Hanghøj Iversen
|
d8f1aabed5
|
Expand gitignore
|
2018-05-09 18:25:01 +02:00 |
|
|
Frederik Hanghøj Iversen
|
9842c66eea
|
Use macros extensively
|
2018-05-09 18:24:07 +02:00 |
|
|
Frederik Hanghøj Iversen
|
179570edf0
|
Changes based on Pierre's suggestions
|
2018-05-09 18:13:36 +02:00 |
|
|
Frederik Hanghøj Iversen
|
2b0dfe4984
|
Change titlepage
|
2018-05-09 12:33:58 +02:00 |
|
|
Frederik Hanghøj Iversen
|
2e11a2390f
|
Shorten link
|
2018-05-08 23:05:45 +02:00 |
|
|
Frederik Hanghøj Iversen
|
ae9a0b3de7
|
Encourage people to read my report
|
2018-05-08 22:46:17 +02:00 |
|
|
Frederik Hanghøj Iversen
|
655c12720a
|
Remove obsolete comment
|
2018-05-08 18:49:17 +02:00 |
|
|
Frederik Hanghøj Iversen
|
a5571de191
|
Document version numbers
|
2018-05-08 18:45:36 +02:00 |
|
|
Frederik Hanghøj Iversen
|
a181cfb63e
|
Merge branch 'dev'
|
2018-05-08 18:35:45 +02:00 |
|
|
Frederik Hanghøj Iversen
|
d1981ec0fa
|
Update CHANGELOG and remove --allow-unsolved-metas pragma
|
2018-05-08 18:35:22 +02:00 |
|
|
Frederik Hanghøj Iversen
|
32e7290fe9
|
Prove missing link for univalence via new branch of cubical
|
2018-05-08 18:01:34 +02:00 |
|
|
Frederik Hanghøj Iversen
|
e5d55c7b2b
|
Include appendices
|
2018-05-08 16:22:51 +02:00 |
|
|
Frederik Hanghøj Iversen
|
4e7506f06a
|
Decrease line-width
|
2018-05-08 14:50:45 +02:00 |
|
|
Frederik Hanghøj Iversen
|
10c3c36305
|
Fix typos
|
2018-05-08 02:02:13 +02:00 |
|
|
Frederik Hanghøj Iversen
|
6a3e7390d7
|
Do not use colon directly for typing judgments
|
2018-05-08 02:01:17 +02:00 |
|
|
Frederik Hanghøj Iversen
|
e18730e0e5
|
Remove tex warnings
|
2018-05-08 02:00:23 +02:00 |
|
|
Frederik Hanghøj Iversen
|
7faf0961c5
|
Fix spelling mistakes
|
2018-05-08 00:25:34 +02:00 |
|
|
Frederik Hanghøj Iversen
|
0db4e97511
|
Do not use wishlist
|
2018-05-07 14:39:50 +02:00 |
|
|
Frederik Hanghøj Iversen
|
d5a4550ca9
|
Always use brackets in subscript
|
2018-05-07 10:53:22 +02:00 |
|
|
Frederik Hanghøj Iversen
|
4070e702d7
|
Various changes
|
2018-05-07 10:13:13 +02:00 |
|
|
Frederik Hanghøj Iversen
|
29c4c4a3b9
|
Equality principle for isomorphisms
|
2018-05-07 10:12:11 +02:00 |
|