>>42
写像の概念は最初はsource≠domainで定義された後
source=domainのものに限定している
しかしそれでは
Y⊂X
に対して
A^Y⊂A^X
は自然に定義できない
自然なのは限定写像
res:A^X→A^Y
の方
最初これでVB定義できないかと思ったが
colimでなくてlimなのでクラスの集まりを考える羽目になるため断念
やはり自然な包含
A^Y⊂A^X
が定義できるためには
写像の概念はsource≠domainであるものを考えるべきと思うね