# Proof of id and associativity in Rel category

I'm learning Category Theory by Steve Awodey's book. The very first exercise asks to show if $\mathbf{Rel}$ is a category. As I understood everything is already set (objects, arrow, id and composition) and all I need to do is to show that axioms for id and composition work.

I did it like this:

For id axiom using the definition of composition in $\mathbf{Rel}$:

$f \circ 1_A = \{ \langle a,b \rangle \in A \times B \mid \langle a,a \rangle \in 1_A \land \langle a,b \rangle \in f \} = f = \{ \langle a,b \rangle \in A \times B \mid \langle a,b \rangle \in B \land \langle b,b \rangle \in 1_B\} = 1_B \circ f$

For showing composition associativity I have introduced a new arrow $h\colon C \to D$:

$h \circ (g \circ f) = \{ \langle a,d \rangle \in A \times D \mid \exists c\, (\langle a,c \rangle \in g \circ f \land \langle c,d \rangle \in h) \} = \{ \langle a,d \rangle \in A \times D \mid \exists b\, (\langle a,b \rangle \in f \land \langle b,d \rangle \in h \circ g) \} = (h \circ g) \circ f$

Is it how it should be or my considerations were wrong?

• It's all correct, although some things could be made more explicitly (in particular, I would personally add one intermediate equality between the two lines for associativity). Commented Jan 16, 2018 at 13:13
• I'm less sanguine than Arnaud D. It's all "correct", but it isn't much of a proof. You've simply written out the definition of each side and then merely asserted that they are, in fact, equal. You might as well have just said "It's trivial. QED." It is very simple but since you are asking about it here, you are perhaps not at the point where you can just dismiss it as trivial. I recommend working it out step-by-step in as much detail as you can. Commented Jan 16, 2018 at 19:04
• @ArnaudD, thank you! I will try to expand the proof.
– lsa
Commented Jan 18, 2018 at 9:53
• @DerekElkins, thank you! I got the point, it seems trivial indeed, so I was actually wondering to which level of detalization I should go to make it look as a proof.
– lsa
Commented Jan 18, 2018 at 9:54
• @Isa, I don't see how you moved to the third equation where you introduce $\exists b$, could your please explain? Commented Apr 11, 2020 at 13:45

As an example of what Derek Elkins said in his comment, you might try including detail such as, --- where the “•” is punctuation ---

   f ∘ 1
=⟨ definition of composition ⟩
{ ⟨x, z⟩ ❙ (∃ y • ⟨x,y⟩ ∈ 1 ∧ ⟨y, z⟩ ∈ f) }
=⟨ definition of identity relation ⟩
{ ⟨x, z⟩ ❙ (∃ y • x = y ∧ ⟨y, z⟩ ∈ f) }
=⟨ Removing the silly quantifier, since y = x ⟩
{ ⟨x, z⟩ ❙ ⟨x, z⟩ ∈ f }
=⟨ extensionality ⟩
f

• Thank you, looks very reasonable.
– lsa
Commented Jan 18, 2018 at 10:19
• @Musa Al-hassy, could your please do the same for the associativity law? Commented Apr 11, 2020 at 14:11
• Invoke the definition of composition twice, then you'll have two conjunctions $\land$, which is associative, so shuffle the parens, then close up with the definition of compoistion ;-) Commented Apr 12, 2020 at 9:48