It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 495
- Study Groups 6
- Biological Models 1
- Categorical Network Theory 1
- Programming with Categories 4
- Review Sections 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Statistical methods 2
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 0
- Strategy 111
- Azimuth Project 1.1K
- - Spam 1
- News and Information 147
- Azimuth Blog 149
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 708

Options

*A tiny category.*

Recall that a category consists of the data:

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

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

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 \);

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 \).

(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

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

https://gitlab.com/snippets/1930056

`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)`

I don't understand what it means by

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

@kenwebb Here is a hint: look at

2.in the definition of category above. For everypairof 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?`@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?`

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).

`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).`

@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.

`@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.`