Commit graph

48 commits

Author SHA1 Message Date
Frederik Hanghøj Iversen 7787a8f0be Indentation 2018-02-23 12:52:14 +01:00
Frederik Hanghøj Iversen 48423cc816 Rename arrowIsSet to arrowsAreSets 2018-02-23 12:51:44 +01:00
Frederik Hanghøj Iversen 6446435a49 Rename ident to isIdentity 2018-02-23 12:49:41 +01:00
Frederik Hanghøj Iversen 5cbc409770 Rename assoc to isAssociative 2018-02-23 12:43:49 +01:00
Frederik Hanghøj Iversen cc1ddaac9f Add new type-synonym 2018-02-23 10:35:42 +01:00
Frederik Hanghøj Iversen 57d7eab4cb Make sets a category according to HoTT 2018-02-21 13:37:07 +01:00
Frederik Hanghøj Iversen ed40824edc Cosmetics 2018-02-21 12:59:31 +01:00
Frederik Hanghøj Iversen edf552cb86 Do not define synonym for contractible 2018-02-20 18:15:30 +01:00
Frederik Hanghøj Iversen d2da84269f Move some more things into RawCategory 2018-02-20 18:14:42 +01:00
Frederik Hanghøj Iversen 0c861c4bde Factor univalence out to a seperate module 2018-02-20 18:13:06 +01:00
Frederik Hanghøj Iversen a4f8a37e36 Proove that IsCategory is a mere proposition! 2018-02-20 18:01:26 +01:00
Frederik Hanghøj Iversen 159bffa6ae Factor out more from IsCategory 2018-02-20 17:59:48 +01:00
Frederik Hanghøj Iversen a016c67b88 Succesfully apply path-induction.
Now all that's left to do is prove the original proposition in a
heterogenous equality
2018-02-20 17:46:32 +01:00
Frederik Hanghøj Iversen ff496aae09 Factor out a useful type-family 2018-02-20 17:33:02 +01:00
Frederik Hanghøj Iversen 860c91f913 Trim mess 2018-02-20 16:43:53 +01:00
Frederik Hanghøj Iversen 8ef61d9db0 Simplify Category 2018-02-20 16:26:40 +01:00
Frederik Hanghøj Iversen 10df9511a4 Move various type-synonyms to RawCategory 2018-02-20 16:24:14 +01:00
Frederik Hanghøj Iversen 38ec53d5c2 Cosmetics 2018-02-20 14:08:47 +01:00
Frederik Hanghøj Iversen 44eda0ced0 Stuff about propositionality of fields of IsCategory 2018-02-19 15:46:19 +01:00
Frederik Hanghøj Iversen bec5acdc59 Move proposition to wishlist 2018-02-19 11:25:16 +01:00
Frederik Hanghøj Iversen 23c458983c Rely on global cubical again 2018-02-16 11:37:22 +01:00
Frederik Hanghøj Iversen 7d4aae4f49 Try to show that natural transformations are sets 2018-02-09 12:09:59 +01:00
Frederik Hanghøj Iversen 56d689fb4b Use arrowIsSet to simplify equality constructor for functors 2018-02-07 20:19:17 +01:00
Frederik Hanghøj Iversen 9349b37550 Refactor Functor - only in module Functor 2018-02-06 14:31:18 +01:00
Frederik Hanghøj Iversen 0688f5c372 Rename arrowIsSet 2018-02-06 10:34:43 +01:00
Frederik Hanghøj Iversen e8ac6786ff Changes to the category of categories 2018-02-05 16:35:33 +01:00
Frederik Hanghøj Iversen 83ccde62e9 Use co-patterns 2018-02-05 14:47:15 +01:00
Frederik Hanghøj Iversen 20dc9d26ac Move product, exponential and cart closed to own file 2018-02-05 14:08:30 +01:00
Frederik Hanghøj Iversen 8022ed349d "re-delegate" projections in new module Category 2018-02-05 12:21:39 +01:00
Frederik Hanghøj Iversen 22a9a71870 Split Category into RawCategory and IsCategory 2018-02-05 11:43:38 +01:00
Frederik Hanghøj Iversen fecb4dc1ce Towards IsCategory-is-prop 2018-02-05 10:24:57 +01:00
Frederik Hanghøj Iversen e5f1fa018a Merge branch 'Saizan-master' into dev 2018-02-02 15:34:30 +01:00
Frederik Hanghøj Iversen 19987dd917 Add some stuff about the category of cubes
Also some feedback from Thierry
2018-02-02 14:47:51 +01:00
Andrea Vezzosi 8d5e992e48 changed IsCategory to follow the HoTT book definition. 2018-02-01 14:37:55 +00: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 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 3fcdf828d8 Implement exponentials 2018-01-21 21:29:15 +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 5fd7dcae9d Notes from Andrea and some stuff about products 2018-01-21 00:21:25 +01:00
Frederik Hanghøj Iversen 902b953ad0 Implement representable functors 2018-01-17 12:10:18 +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
Renamed from src/Category.agda (Browse further)