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

Add backlog and changelog

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-21 14:06:09 +01:00
parent a82095604d
commit 7ed99a6bb4
2 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
BACKLOG.md Normal file
View file

@ -0,0 +1,6 @@
Backlog
=======
Prove univalence for various categories
Prove postulates in `Cat.Wishlist`

17
CHANGELOG.md Normal file
View file

@ -0,0 +1,17 @@
Changelog
=========
Version 1.1.0
-------------
In this version categories have been refactored - there's now a notion of a raw
category, and a proper category which has the data (raw category) as well as
the laws.
Furthermore the type of arrows must be homotopy sets and they must satisfy univalence.
I've made a module `Cat.Wishlist` where I just postulate things that I hope to
implement upstream in `cubical`.
I have proven that `IsCategory` is a mere proposition.
I've also updated the category of sets to adhere to this new definition.