# 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). – Arnaud D. Jan 16 '18 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. – Derek Elkins left SE Jan 16 '18 at 19:04
• @ArnaudD, thank you! I will try to expand the proof. – lsa Jan 18 '18 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 Jan 18 '18 at 9:54
• @Isa, I don't see how you moved to the third equation where you introduce $\exists b$, could your please explain? – neshkeev Apr 11 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 Jan 18 '18 at 10:19
• @Musa Al-hassy, could your please do the same for the associativity law? – neshkeev Apr 11 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 ;-) – Musa Al-hassy Apr 12 at 9:48