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

Fix typos

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-08 02:02:13 +02:00
parent 6a3e7390d7
commit 10c3c36305
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
CHANGELOG.md
View file

@ -1,4 +1,4 @@
Changelog
Change log
=========
Version 1.4.1
@ -29,12 +29,12 @@ 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
categories. This is achieved 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!
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.
@ -42,7 +42,7 @@ the category of functors.
Version 1.3.0
-------------
Removed unused modules and streamlined things more: All specific categories are
in the namespace `Cat.Categories`.
in the name space `Cat.Categories`.
Lemmas about categories are now in the appropriate record e.g. `IsCategory`.
Also changed how category reexports stuff.
@ -53,7 +53,7 @@ Rename Opposite to opposite
Add documentation in Category-module
Formulation of monads in two ways; the "monoidal-" and "kleisli-" form.
Formulation of monads in two ways; the "monoidal-" and "Kleisli-" form.
WIP: Equivalence of these two formulations

2
src/Cat/Categories/Free.agda
View file

@ -1,4 +1,4 @@
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Categories.Free where
open import Cat.Prelude hiding (Path ; empty)