昨日の構成が自然かどうかを確かめる。
g:c \to c'に対してcolim TU(c) \to colim TU(c')とVc \to Vc'が定まり、
これがcolimitの普遍性から定まる射と可換かどうか調べる。
colim TU(c) \to Vc'が、まずVcを経由する射については、これがVcへの普遍性から定まる射とVc \to Vc'を合成するものだからこれも図式と整合的な射になり、したがって普遍性から定まるcolim TU(c) \to Vc'と一致する。
一方でcolim TU(c')を経由する射は、TU(c) \to TU(c')が図式の射を定め、colim TU(c') \to Vc'が図式の射と可換なため、これも普遍性から定まる射となる。
いずれの射も普遍性から定まる射と一致するので、これらは一致している。
このことから、昨日の対応が自然変換であることがわかり、c \mapsto colim TU(c)がKan拡張としての普遍性を持つことがわかる。
