Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Last active October 2, 2017 07:59
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Icelandjack/4801d18d39e8e31217fb227d2ee24fd6 to your computer and use it in GitHub Desktop.
CCC talking points

Free Categories

You can build categories just by connecting objects with arrows. You can imagine starting with any directed graph and making it into a category by simply adding more arrows. First, add an identity arrow at each node. Then, for any two arrows such that the end of one coincides with the beginning of the other (in other words, any two composable arrows), add a new arrow to serve as their composition. Every time you add a new arrow, you have to also consider its composition with any other arrow (except for the identity arrows) and itself. You usually end up with infinitely many arrows, but that’s okay.

Another way of looking at this process is that you’re creating a category, which has an object for every node in the graph, and all possible chains of composable graph edges as morphisms. (You may even consider identity morphisms as special cases of chains of length zero.)

Such a category is called a free category generated by a given graph. It’s an example of a free construction, a process of completing a given structure by extending it with a minimum number of items to satisfy its laws (here, the laws of a category). We’ll see more examples of it in the future.

type CAT k = k -> k -> Type

data FreeCat :: CAT k -> CAT k where
  Nil  :: FreeCat cat a a
  Cons :: cat a b -> FreeCat cat b c -> FreeCat cat a c

instance Category (FreeCat cat) where
  id :: (FreeCat cat) a a
  id = Nil

  (.) :: (FreeCat cat) b c -> (FreeCat cat) a b -> (FreeCat cat) a c
  xs . Nil       = xs
  xs . Cons y ys = Cons y (xs . ys)

Zero Category

The most trivial category is one with zero objects and, consequently, zero morphisms. It’s a very sad category by itself, but it may be important in the context of other categories, for instance, in the category of all categories (yes, there is one). If you think that an empty set makes sense, then why not an empty category?

data ZeroTemplate :: Cat Void

type Zero = FreeCat ZeroTemplate

One Category

-- Generate a free category from a graph with one node and no edges
data OneTemplate :: CAT ()
type One = FreeCat OneTemplate

id_unit :: One () ()
id_unit = Nil

Two Category

-- Graph with two nodes and a single arrow between them
data AB = A | B
data TwoTemplate :: CAT AB where
  A_to_B :: TwoTemplate A B

type Two = FreeCat TwoTemplate

idA :: Two A A
idA = Nil

idB :: Two B B
idB = Nil

ab :: Two A B
ab = Cons A_to_B Nil 

Three Category

data XYZ = X | Y | Z
data ThreeTemplate :: CAT XYZ where
  X_to_Y :: ThreeTemplate X Y
  Y_to_Z :: ThreeTemplate Y 'Z

type Three = FreeCat ThreeTemplate

xy :: Three X Y
xy = Cons X_to_Y Nil

yz :: Three Y 'Z
yz = Cons Y_to_Z Nil

xz :: Three X 'Z
xz = xy >>> yz
@Icelandjack
Copy link
Author

-- A monoid gives a rise to a single-object category.
data Dummy = MkDummy

newtype MonoidCat :: Type -> CAT Dummy where
  MCat :: m -> MonoidCat m dummy dummy'

instance Monoid m => Category (MonoidCat m) where
  id = MCat mempty
  MCat a . MCat b = MCat (mappend a b)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment