“圏の圏”は2-圏の事例と考えよう。 対象＝ポインティング関手、射＝ポインティング関手のあいだの自然変換、と考えよう。 各種の適用〈application | evaluation〉、射の結合、関手の結合、関手・自然変換のヒゲ結合、自然変換・自然変換の縦結合、自然変換…

ステートメント α::F⇒G:C→D is-natural-iso ⇔ ∀(A in C).( αA is-iso in D ) 主要な概念・命題 α::F⇒G:C→D is-iso within Cat(C, D) in Cat ∃(β::G⇒F:C→D within Cat(C, D)).α;β = IDF ∧ β;α = IDG within Cat(C, D) in Cat α;β = IDF in Cat(C, D) ⇔ ∀(A in…