-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Eitan Chatav
authored and
Eitan Chatav
committed
Nov 2, 2019
1 parent
e777a4b
commit a8e9fb2
Showing
1 changed file
with
1 addition
and
31 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,31 +1 @@ | ||
# free-categories | ||
|
||
Consider the category of Haskell "quivers" with | ||
|
||
* objects are types of higher kind | ||
* `p :: k -> k -> Type` | ||
* morphisms are terms of `RankNType`, | ||
* `forall x y. p x y -> q x y` | ||
* identity is `id` | ||
* composition is `.` | ||
|
||
Now, consider the subcategory of Haskell `Category`s with | ||
|
||
* constrained objects `Category c => c` | ||
* morphisms act functorially | ||
* `t :: (Category c, Category d) => c x y -> d x y` | ||
* `t id = id` | ||
* `t (g . f) = t g . t f` | ||
|
||
The [free category functor](https://ncatlab.org/nlab/show/free+category) | ||
from quivers to `Category`s may be defined up to isomorphism as | ||
|
||
* the functor `Path` of type-aligned lists | ||
|
||
* the functor `FoldPath` of categorical folds | ||
|
||
* abstractly as `CFree path => path`, the class of | ||
left adjoints to the functor which | ||
forgets the constraint on `Category c => c` | ||
|
||
* or as any isomorphic data structure | ||
The free category on a quiver. |