Commit Graph

20 Commits

Author SHA1 Message Date
Frederik Hanghøj Iversen 95a8e82d40 Update agda-stdlib to newer version 2018-10-30 14:28:09 +01: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
Frederik Hanghøj Iversen 636b5f3e27 Makefile uses included libraries 2018-05-26 01:15:57 +02:00
Frederik Hanghøj Iversen a5571de191 Document version numbers 2018-05-08 18:45:36 +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 c0cf6789cd Use propositions straight from the horses mouth 2018-03-12 13:56:49 +01:00
Frederik Hanghøj Iversen 35390c02d3 Stuff about univalence in the category of sets 2018-03-12 13:38:48 +01:00
Frederik Hanghøj Iversen 459718da23 Finish proof of equivalence of klesili/monoidal categories!! 2018-03-07 17:30:09 +01:00
Frederik Hanghøj Iversen 19103e1678 Update cubical 2018-03-07 16:24:43 +01:00
Frederik Hanghøj Iversen 3749124d09 Switch to experimental branch of stdlib 2018-03-07 15:38:37 +01:00
Frederik Hanghøj Iversen bf605e09fe Update commit refs 2018-03-07 15:10:36 +01:00
Frederik Hanghøj Iversen ee2b30d640 Update commit references 2018-02-23 13:18:47 +01:00
Frederik Hanghøj Iversen 8f620e0dbe Update commit references 2018-02-21 13:43:26 +01:00
Frederik Hanghøj Iversen 23c458983c Rely on global `cubical` again 2018-02-16 11:37:22 +01:00
Frederik Hanghøj Iversen 86d3d7368e Use equality construction principle
Also update submodules
2018-01-30 22:41:18 +01:00
Frederik Hanghøj Iversen 86c9b5b111 Update submodules 2018-01-30 10:59:01 +01:00
Frederik Hanghøj Iversen 19d5605981 Add new submodules 2017-11-10 16:56:52 +01:00
Frederik Hanghøj Iversen 38fd690839 Add more instances 2017-06-07 22:03:56 +02:00
Frederik Hanghøj Iversen 8485b55152 Add cubical as a submodule 2017-06-07 15:52:40 +02:00