### 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 = gNow 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 . CAnd the puzzle is solved.

--

Is it possible to prove the identity without using tabulations?

Labels: Category Theory

<< 回到主頁