› ›
Options

Question 1.2 - A tiny category

JakeGillberg
edited January 2020 in MIT 2020: Exercises

A tiny category.

Recall that a category consists of the data:

  1. a set \(Ob(C) \) of objects;

  2. for every pair of objects \(c,d \in Ob(C) \) a set \(C(c,d) \) of morphisms;

  3. for every three objects \(b,c,d \) and morphisms \(f : b \to c \) and \(g : c \to d \), a specified morphism \((f ; g) : b \to d \) called the composite of \(f \) and \(g \);

  4. for every object \(c \), an identity morphism \(id_c \in C(c,c) \); and

subject to two laws:

Unit: for any \(f : c \to d \), the equations \(id_c ; f = f \) and \(f ; id_d = f \) hold.

Associative: for any \(f_1 : c_1 \to c_2, f_2 : c_2 \to c_3 \), and \(f_3 : c_3 \to c_4 \), the equation \((f_1 ; f_2) ; f_3 = f_1 ; (f_2 ; f_3) \) holds.

--

This tiny category is sometimes called the walking arrow category \(2 \).

img

(a) Write down the set of objects, the four sets of morphisms, the composition rule, and the identity morphisms.

(b) Prove that this category obeys the unit and associative laws.

Comments

  • Options
    1.
    JakeGillberg

    For funzies, here is the definition and proof via Idris. I use the definition of Category from idris-ct:

    https://gitlab.com/snippets/1930056

    Comment Source:For funzies, here is the definition and proof via [Idris](https://www.idris-lang.org/). I use the definition of Category from [idris-ct](https://github.com/statebox/idris-ct): [https://gitlab.com/snippets/1930056](https://gitlab.com/snippets/1930056)
  • Options
    2.
    KenWebb

    I don't understand what it means by the four sets of morphisms.

    Comment Source:I don't understand what it means by **the four sets of morphisms**.
  • Options
    3.
    JakeGillberg
    edited January 2020

    @kenwebb Here is a hint: look at 2. in the definition of category above. For every pair of objects, we must have a set of morphisms (the set may be empty). There must be four pairs of objects in our category. Which pairs do you see?

    Comment Source:@kenwebb Here is a hint: look at **2.** in the definition of category above. For every **pair** of objects, we must have a set of morphisms (the set may be empty). There must be four pairs of objects in our category. Which pairs do you see?
  • Options
    4.
    KenWebb

    Thanks @JakeGillberg. The key observation that I was missing is that any of the four sets of morphisms might be the empty set. There's no actual arrow corresponding to the pair (2,1).

    Comment Source:Thanks @JakeGillberg. The key observation that I was missing is that any of the four sets of morphisms might be the empty set. There's no actual arrow corresponding to the pair (2,1).
  • Options
    5.
    LeifMetcalf

    @JakeGillberg Is it possible to write a similar proof in Haskell? I tried it here (https://paste.sr.ht/~leif/86497a18e9ae2ba10daaed64302284a287c21ad6) but got stuck on what to put for the definition of identity.

    Comment Source:@JakeGillberg Is it possible to write a similar proof in Haskell? I tried it here (https://paste.sr.ht/%7Eleif/86497a18e9ae2ba10daaed64302284a287c21ad6) but got stuck on what to put for the definition of identity.
Sign In or Register to comment.