疲れた、ヘロヘロだ。朦朧状態。インスティチューションIの上のプログラムの圏Progは、|Prog| = |Sign|であり、自然な埋め込み Sign ⊆ Progがある。つまり、SignがProgの広大部分圏で入っている。[追記]自然な埋め込みがあるのではなくて、埋め込みの族があ…