 Frederik Hanghøj Iversen
|
e7f5648607
|
Disable cube
|
2018-10-30 14:37:15 +01:00 |
|
Frederik Hanghøj Iversen
|
95a8e82d40
|
Update agda-stdlib to newer version
|
2018-10-30 14:28:09 +01:00 |
|
Frederik Hanghøj Iversen
|
8f15001a93
|
Use smaller symbols for arrows in presentation
|
2018-10-29 12:39:12 +01:00 |
|
Frederik Hanghøj Iversen
|
c5020a0d87
|
Add Chalmers logo to front page
|
2018-09-11 15:16:14 +02:00 |
|
Frederik Hanghøj Iversen
|
d7a07da07b
|
Update to most recent version of stdlib
|
2018-08-04 13:46:59 +02:00 |
|
Frederik Hanghøj Iversen
|
7836367f4a
|
Use HEAD version of cubical and stdlib
|
2018-07-19 20:22:17 +02:00 |
Andrea Vezzosi
|
e16a4b8189
|
isEquiv is now a record
|
2018-07-18 16:49:01 +02:00 |
|
Frederik Hanghøj Iversen
|
9ee05e1a36
|
Universally quantify test object in epi- mono- morphism
Closes #26
|
2018-07-17 17:03:23 +02:00 |
|
Frederik Hanghøj Iversen
|
188bba6c8d
|
Old unstaged changes
I hope these are mostly non dangerous. Looks like it's mainly some reformatting.
|
2018-07-17 16:51:16 +02:00 |
|
Frederik Hanghøj Iversen
|
6f275247dd
|
Final presentation
|
2018-06-07 15:20:14 +02:00 |
|
Frederik Hanghøj Iversen
|
5a748c57f0
|
Update RAEDME
|
2018-05-31 02:12:45 +02:00 |
|
Frederik Hanghøj Iversen
|
c784723184
|
Insert link to pre-compiled pdf
|
2018-05-31 02:09:46 +02:00 |
|
Frederik Hanghøj Iversen
|
93871358a3
|
Update README
|
2018-05-31 02:05:56 +02:00 |
|
Frederik Hanghøj Iversen
|
66e5f46912
|
Untabify readme
|
2018-05-31 02:00:29 +02:00 |
|
Frederik Hanghøj Iversen
|
9497a650ea
|
Test with master Agda version 2.6.0-d3efe64
|
2018-05-31 01:56:44 +02:00 |
|
Frederik Hanghøj Iversen
|
33f7e2ebbb
|
Merge branch 'dev'
|
2018-05-31 01:07:31 +02:00 |
|
Frederik Hanghøj Iversen
|
27ae920634
|
Fixup some missing files
|
2018-05-31 01:07:05 +02:00 |
|
Frederik Hanghøj Iversen
|
08046d05dc
|
Update makefile
|
2018-05-29 15:35:20 +02:00 |
|
Frederik Hanghøj Iversen
|
98cad057d5
|
Merge branch 'dev'
|
2018-05-29 15:26:38 +02:00 |
|
Frederik Hanghøj Iversen
|
49f1262b2c
|
Update change log
|
2018-05-29 15:24:18 +02:00 |
|
Frederik Hanghøj Iversen
|
6d362af88e
|
Add type-synonym
|
2018-05-29 15:14:46 +02:00 |
|
Frederik Hanghøj Iversen
|
392d656709
|
Move included graphics
|
2018-05-29 15:14:27 +02:00 |
|
Frederik Hanghøj Iversen
|
37a675a84f
|
Final touch-up on report and acknowledgments
|
2018-05-29 15:09:38 +02:00 |
|
Frederik Hanghøj Iversen
|
b992d5a7f2
|
Use unicode symbols
|
2018-05-28 17:44:23 +02:00 |
|
Frederik Hanghøj Iversen
|
1f750e2275
|
Erratta
|
2018-05-28 17:32:56 +02:00 |
|
Frederik Hanghøj Iversen
|
636b5f3e27
|
Makefile uses included libraries
|
2018-05-26 01:15:57 +02:00 |
|
Frederik Hanghøj Iversen
|
326951d826
|
Put in brackets for readability
|
2018-05-24 15:57:30 +02:00 |
|
Frederik Hanghøj Iversen
|
2d0dfab12a
|
Remove some TODO-notes, add section on motifs
|
2018-05-23 18:28:27 +02:00 |
|
Frederik Hanghøj Iversen
|
fc7e504359
|
Correctly terminate appendix section
|
2018-05-23 17:49:54 +02:00 |
|
Frederik Hanghøj Iversen
|
251fcf1966
|
Add backlog based on comments from Andrea, implement some of them
|
2018-05-23 17:34:50 +02:00 |
|
Frederik Hanghøj Iversen
|
879f5bab52
|
Use `fromIsomorphism` globally
|
2018-05-22 18:01:03 +02:00 |
|
Frederik Hanghøj Iversen
|
9848fac672
|
Provide grpdSig
|
2018-05-22 16:31:26 +02:00 |
|
Frederik Hanghøj Iversen
|
cb0117819b
|
Monoidal monads are also groupoids
|
2018-05-22 16:28:23 +02:00 |
|
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 |