対象と射を持たない圏

ありなんかそれtakker.icon

$ {\bf ZERO}=(\varnothing,\varnothing,\bullet\circ\bullet)

注：$ \bf ZEROという表記はtakker.iconの造語

確かに、圏の要件は満たす

$ \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.icon

実用性もZERO