generated at
対象と射を持たない圏

対象を持たない
ありなんかそれtakker
{\bf ZERO}=(\varnothing,\varnothing,\bullet\circ\bullet)
注:\bf ZEROという表記はtakkerの造語
確かに、圏の要件は満たす
\vdash\forall A,B,C,D\in{\rm ob}({\bf ZERO})\forall h\in{\bf ZERO}(C,D)\forall g\in{\bf ZERO}(B,C)\forall f\in{\bf ZERO}(A,B).(h\circ g)\circ f=h\circ(g\circ f)
\vdash\forall A,B\in{\rm ob}({\bf ZERO})\forall f\in{\bf ZERO}(A,B).f\circ{\rm id}_A=f={\rm id}_B\circ f
\vdash\forall A,B,A',B'\in{\rm ob}({\bf ZERO}).{\bf ZERO}(A,B)\cap{\bf ZERO}(A',B')\neq\varnothing\implies A=A'\land B=B'
{\rm ob}({\bf ZERO})=\varnothingなので、/takker/├∀x∈∅;P(x)より全て成立する

ウケるnishio
実用性もZERO