fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Update changelog and backlog

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-13 10:40:43 +01:00
parent 896e0d3d37
commit 6db2a3e5d4
2 changed files with 19 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
BACKLOG.md
View file

@ -1,14 +1,9 @@
Backlog Backlog
======= =======
Prove univalence for various categories
Prove postulates in `Cat.Wishlist` Prove postulates in `Cat.Wishlist`
`propHasLevel` should be in `cubical`
`ntypeCommulative` might be there as well. `ntypeCommulative` might be there as well.
Define and use Monad≡
Prove that the opposite category is a category. Prove that the opposite category is a category.
Prove univalence for the category of Prove univalence for the category of

20
CHANGELOG.md
View file

@ -1,9 +1,27 @@
Changelog Changelog
========= =========
Version 1.4.0
-------------
Adds documentation to a number of modules.
Adds an "equality principle" for categories and monads.
Prove that `IsMonad` is a mere proposition.
Provides the yoneda embedding without relying on the existence of a category of
categories. This is acheived by providing some of the data needed to make a ccc
out of the category of categories without actually having such a category.
Renames functors object map and arrow map to `omap` and `fmap`.
Prove that kleisli- and monoidal- monads are equivalent!
[WIP] Started working on the proofs for univalence for the category of sets and
the category of functors.
Version 1.3.0 Version 1.3.0
------------- -------------
Removed unused modules and streamlined things more: All specific categories are Removed unused modules and streamlined things more: All specific categories are
in the namespace `Cat.Categories`. in the namespace `Cat.Categories`.