Commit graph

484 commits

Author SHA1 Message Date
Frederik Hanghøj Iversen 86d3d7368e Use equality construction principle
Also update submodules
2018-01-30 22:41:18 +01:00
Frederik Hanghøj Iversen 255b0236f9 Use alternative syntax for arrow composition 2018-01-30 19:19:16 +01:00
Frederik Hanghøj Iversen e33911ad9e Use alternate syntax for arrow-composition 2018-01-30 18:26:11 +01:00
Frederik Hanghøj Iversen c87a6fb469 Make IsFunctor a seperate record 2018-01-30 16:24:16 +01:00
Frederik Hanghøj Iversen f13b98b009 Merge branch 'dev' 2018-01-30 13:23:17 +01:00
Frederik Hanghøj Iversen 52dea06df9 Add planning report 2018-01-30 13:00:09 +01:00
Frederik Hanghøj Iversen 4db19b6420 Do not use PathPrelude directly 2018-01-30 11:19:48 +01:00
Frederik Hanghøj Iversen 86c9b5b111 Update submodules 2018-01-30 10:59:01 +01:00
Frederik Hanghøj Iversen 53816aeb74 One step closer to yoneda 2018-01-30 10:57:24 +01:00
Frederik Hanghøj Iversen eae441b659 Merge branch 'Saizan-dev-yoneda' 2018-01-25 22:00:22 +01:00
Andrea Vezzosi 2295022619 used presheaf as first component of yoneda 2018-01-25 17:04:00 +00:00
Frederik Hanghøj Iversen ee2e84edfe Remove unused bindings 2018-01-25 14:11:28 +01:00
Frederik Hanghøj Iversen 6e25083a47 Comments in yoneda 2018-01-25 13:58:56 +01:00
Frederik Hanghøj Iversen aaa80f26d5 Merge branch 'master' into dev 2018-01-25 13:17:00 +01:00
Frederik Hanghøj Iversen bd824143bc Update reference to Agda-version 2018-01-25 12:54:00 +01:00
Frederik Hanghøj Iversen e501f8152b Merge branch 'dev' 2018-01-25 12:52:39 +01:00
Frederik Hanghøj Iversen 812662bda3 Rename some variables 2018-01-25 12:47:32 +01:00
Frederik Hanghøj Iversen 7a77ba230c Move functor-equality to functor module 2018-01-25 12:11:50 +01:00
Frederik Hanghøj Iversen a480fca956 Clean up some stuff 2018-01-25 12:01:37 +01:00
Frederik Hanghøj Iversen c5a3673d9b Prove that Cat is cartesian closed
WIP
2018-01-24 16:38:28 +01:00
Frederik Hanghøj Iversen 6a25a4c3ff Fix typo, rename implicit variables, implement presheaf 2018-01-22 15:03:04 +01:00
Frederik Hanghøj Iversen dd3415a69d Some stuff about CwF's 2018-01-22 14:44:50 +01:00
Frederik Hanghøj Iversen fd03049c92 Move the category of functors 2018-01-22 14:44:25 +01:00
Frederik Hanghøj Iversen 9fdf6b589b Use TDNR in Functor 2018-01-22 11:35:37 +01:00
Frederik Hanghøj Iversen bf1d1566af Naturality; category of functors and natural transformations
WIP
2018-01-22 00:07:44 +01:00
Frederik Hanghøj Iversen 3fcdf828d8 Implement exponentials 2018-01-21 21:29:15 +01:00
Frederik Hanghøj Iversen be4949180b Merge branch 'dev' 2018-01-21 19:24:13 +01:00
Frederik Hanghøj Iversen 922570a5bd Make some names more explicit 2018-01-21 19:23:24 +01:00
Frederik Hanghøj Iversen 26d210dcc3 Rename the category of categories 2018-01-21 15:23:40 +01:00
Frederik Hanghøj Iversen b21c9b7a89 Choose new name for functor composition 2018-01-21 15:21:50 +01:00
Frederik Hanghøj Iversen b158b1d420 Use TDNR 2018-01-21 15:19:15 +01:00
Frederik Hanghøj Iversen ea3e14af96 Re-add eqpair 2018-01-21 15:03:00 +01:00
Frederik Hanghøj Iversen 793fc30534 Move properties of categories to Cat.Category.Properties 2018-01-21 15:01:01 +01:00
Frederik Hanghøj Iversen 316de7e4f9 Remove undefined 2018-01-21 14:32:27 +01:00
Frederik Hanghøj Iversen 4c13334277 Make properties of a category an instance argument 2018-01-21 14:31:37 +01:00
Frederik Hanghøj Iversen 07e4269399 Make level-parameters to Category explicit 2018-01-21 01:11:08 +01:00
Frederik Hanghøj Iversen 0990a3778f Use EqReasoning and clean up some stuff 2018-01-21 01:03:40 +01:00
Frederik Hanghøj Iversen b379c3fed0 Add Makefile 2018-01-21 00:22:52 +01:00
Frederik Hanghøj Iversen 40816eb17a Dummy file to compile everything 2018-01-21 00:21:51 +01:00
Frederik Hanghøj Iversen 5fd7dcae9d Notes from Andrea and some stuff about products 2018-01-21 00:21:25 +01:00
Frederik Hanghøj Iversen da10e63cc8 Fix import-statements. Make file that checks everything 2018-01-17 23:00:27 +01:00
Frederik Hanghøj Iversen e1e8b60930 Merge branch 'dev' 2018-01-17 12:32:23 +01:00
Frederik Hanghøj Iversen e98793a620 Remove duplicate section for references 2018-01-17 12:19:04 +01:00
Frederik Hanghøj Iversen acacfac31c Type-synonyms for Representable functors and Presheafs 2018-01-17 12:16:07 +01:00
Frederik Hanghøj Iversen 902b953ad0 Implement representable functors 2018-01-17 12:10:18 +01:00
Frederik Hanghøj Iversen 7090c2c6bf Clarify some points about the project aim. 2018-01-15 17:56:08 +01:00
Frederik Hanghøj Iversen 69adb726de Fix typos as spotted by HUghes 2018-01-15 16:20:14 +01:00
Frederik Hanghøj Iversen 26d449771a Unfinished stuff about HOM-sets and exponentials 2018-01-15 16:13:23 +01:00
Frederik Hanghøj Iversen 0cd75e6e31 Move functor-stuff to own module 2018-01-08 22:54:53 +01:00
Frederik Hanghøj Iversen 7d6db415a1 Move modules around again.
Henceforth all modules shall be placed under the top-level module-name
`Cat` (at least until I've come up with a better name)

Also fixes an issue caused by https://github.com/Saizan/cubical-demo/ redefining Sigma.
2018-01-08 22:48:59 +01:00