§ Kan Extensions: Key idea
- 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
( -> Kx) -> Kx. So it's really the
-> Kx that controls the situation.