$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2008/04/12

### Left-Division in Rel

I got up earlier than expected and had a little bit of time to do a small exercise. Below is a proof of the universal property of left-division in Rel:

The power of classical logic is essential to this proof. But there is a constructive proof in AoPA (for right-division).

--
I have to think more thoroughly about what happens in the proof...

Labels: