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

## 2008/05/22

### Simple Identity Proved

I've been puzzled by a naïve-looking identity ΛR . C = Λ(R . C) . C (where C is a coreflexive) for a few days. Since its truth is evident when one examines it in the pointwise way, I believed that it can be proven using tabulations, and luckily I was right. The key is to tabulate C as f . fº, which can be easily justified:

f . gº ⊆ id
≡   { shunting of functions }
f ⊆ g
≡   { inclusion of functions is equality }
f = g
Now we reason:
Λ(R . C) . C
=   { tabulate C as f . fº }
Λ(R . f . fº) . f . fº
=   { fusion }
Λ(R . f . fº . f) . fº
=   { f is simple }
Λ(R . f) . fº
=   { fusion (backwards) }
ΛR . f . fº
=   { tabulation of C }
ΛR . C
And the puzzle is solved.

--
Is it possible to prove the identity without using tabulations?

Labels: