- The key insight is to notice that when we map from via , then the object that we get whose comma we form with also has an arrow via the identity arrow. Thus we can think of as looking like
(. So it's really the-> Kx) -> Kx Kxin thethat controls the situation.-> Kx