Tabulations and a Small Equivalence

After Shin's kind explanation, I've finally got some idea about tabulations. In Rel it's just like how database theory models relations --- by building a table for each relation. (This reminds me of the always-smiling professor Hao who taught the course on databases.) Given a relation R : A ← B, it can be tabulated as R = f . gº where f : A ← C and g : B ← C and C is a subset of A × B. C is just the table for R, and the thing between f and gº, a member of C, is exactly one of the table entries. Following this line of thought, the condition (fº . f) ∩ (gº . g) = id can be interpreted as "two table entries are equal if and only if they are component-wise equal". Regarding R as a nonderministic mapping, gº is like looking up the table for entries whose right component equals the input, and then f selects one of the matched entries and returns its left component as the output. Everything goes smoothly! (In fact, more correspondences between database theory and relational calculus can be found. For example, relational composition is comparable to the "natural join" operation in database systems. That's no surprise, since they are essentially the same thing viewed from different angles.)

Before the midterm on computer architecture this afternoon (which turned out to be much, much easier than I expected), I practiced proving that (fº . f) ∩ (gº . g) = id is equivalent to "(f, g) is jointly monic" in a tabular allegory. When proving the "only if" direction, I simply weakened f . h = f . k to f . h ⊆ f . k and then got h . kº ⊆ fº . f by applying the shunting rules. Later when I was proving the other direction, I couldn't go backward, since the route I took from f . h = f . k to h . kº ⊆ fº . f is only one-way. Then I realised that I should go like this to have an equivalence:

in which converse, again, played an essential role.

--
On the other hand, I need to think more about why tabulation enables pointwise proofs...