From 10c3c36305aa07872c2f18a3efb971651a215002 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 8 May 2018 02:02:13 +0200 Subject: [PATCH] Fix typos --- CHANGELOG.md | 10 +++++----- src/Cat/Categories/Free.agda | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 42ab3e0..6bd4bc4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 8fe148a..b55face 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -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)