自然数対象

定義から点付き自己射の射 $v\colon N\to N'$ と $v'\colon N'\to N$ がただ一つずつある。$v'\circ v\colon N\to N$ は $(N,0,s)$ からそれ自身への点付き自己射の射であり、$\operatorname{id}_N$ もそうなので、一意性から $v'\circ v=\operatorname{id}_N$ である。同様に $v\circ v'=\operatorname{id}_{N'}$ である。$\square$

1. 余積の入射を $i_1\colon1\to1+N$、$i_2\colon N\to1+N$ とし、$t:=i_2\circ[0,s]\colon1+N\to1+N$ とおく。定義により $u\circ0=i_1$、$u\circ s=t\circ u$ を満たす $u\colon N\to1+N$ がある。$[0,s]\circ i_1=0$、$[0,s]\circ t=[0,s]\circ i_2\circ[0,s]=s\circ[0,s]$ なので、$[0,s]\circ u$ は
   $$ ([0,s]\circ u)\circ0=[0,s]\circ i_1=0,\qquad([0,s]\circ u)\circ s=[0,s]\circ t\circ u=s\circ([0,s]\circ u) $$
   を満たす。$\operatorname{id}_N$ も同じ 2 式を満たすので、定義の一意性から $[0,s]\circ u=\operatorname{id}_N$ である。逆向きは、余積の普遍性により入射との合成で確かめる。$u\circ[0,s]\circ i_1=u\circ0=i_1$、および
   $$ u\circ[0,s]\circ i_2=u\circ s=t\circ u=i_2\circ[0,s]\circ u=i_2 $$
   なので $u\circ[0,s]=\operatorname{id}_{1+N}$ である。
2. $h\colon N\to X$ が $h\circ s=h$ を満たすとし、$x:=h\circ0$ とおく。$h$ と $x\circ{!}$ はどちらも、点付き自己射 $(X,x,\operatorname{id}_X)$ について $u\circ0=x$、$u\circ s=\operatorname{id}_X\circ u$ を満たす（$!\circ0=\operatorname{id}_1$、$!\circ s={!}$ による）。定義の一意性から $h=x\circ{!}$ である。$k\circ{!}=h$ となる $k\colon1\to X$ は $k=k\circ{!}\circ0=h\circ0$ に限るので、分解は一意である。$\square$

定義により $u\circ0=0'$、$u\circ s=s'\circ u$ を満たす $u\colon N\to M$ がある。$m\circ u$ は $m\circ u\circ0=m\circ0'=0$、$m\circ u\circ s=m\circ s'\circ u=s\circ m\circ u$ を満たすので、定義の一意性から $m\circ u=\operatorname{id}_N$ である。すると $m\circ u\circ m=m=m\circ\operatorname{id}_M$ で $m$ はモノ射だから $u\circ m=\operatorname{id}_M$ であり、$m$ は同型である。$\square$

随伴の全単射を $\varphi\colon\mathcal D(LC,Y)\cong\mathcal C(C,RY)$ と書く。自然性により、$\mathcal C$ の射 $c\colon C'\to C$ と $\mathcal D$ の射 $g\colon Y\to Y'$ について $\varphi(g\circ v\circ L(c))=R(g)\circ\varphi(v)\circ c$ である。
$\mathcal D$ の対象 $Y$ と射 $y\colon1\to Y$、$f\colon Y\to Y$ をとり、$y^\flat:=\varphi(y\circ\iota)\colon1\to RY$ とおく。$(RY,y^\flat,R(f))$ に自然数対象の定義を当てると、$w\circ0=y^\flat$、$w\circ s=R(f)\circ w$ を満たす $w\colon N\to RY$ がただ一つある。射 $v\colon LN\to Y$ について、自然性から
$$ \varphi(v\circ L(0))=\varphi(v)\circ0,\qquad\varphi(v\circ L(s))=\varphi(v)\circ s,\qquad\varphi(f\circ v)=R(f)\circ\varphi(v) $$
であり、$v\circ L(0)\circ\iota^{-1}=y$ は $v\circ L(0)=y\circ\iota$、すなわち $\varphi(v)\circ0=y^\flat$ と同値である。よって $v$ が $v\circ L(0)\circ\iota^{-1}=y$、$v\circ L(s)=f\circ v$ を満たすことは、$\varphi(v)$ が $\varphi(v)\circ0=y^\flat$、$\varphi(v)\circ s=R(f)\circ\varphi(v)$ を満たすことと同値である。$\varphi$ は全単射なので、そのような $v$ は $\varphi^{-1}(w)$ ただ一つである。$\square$

1. 前層 $P$ について、$\lim P$ を「$\mathcal C$ の各射 $c'\to c$ で制限すると互いに移り合う元の族 $(p_c)_c$（$p_c\in P(c)$）」の集合とする。自然変換 $\Delta S\to P$ は写像の族 $\alpha_c\colon S\to P(c)$ で、各射 $g\colon c'\to c$ について $P(g)\circ\alpha_c=\alpha_{c'}$ を満たすもの、すなわち写像 $S\to\lim P$ と同じものであり、この対応は $S$ と $P$ について自然である。よって $\Delta\dashv\lim$ である。$\Delta1$ は各対象で 1 点の前層、すなわち前層の圏の終対象であり、ex-nno-set と thm-nno-left-adjoint から主張が従う。
2. 層化関手 $\mathbf a$ は包含関手 $\operatorname{Sh}(\mathcal C,J)\to\mathbf{Set}^{\mathcal C^{\mathrm{op}}}$ の左随伴で有限極限を保つ（MM92 III.5 Theorem 1, p. 128）。とくに終対象を保つので、1 と thm-nno-left-adjoint から $\mathbf a\Delta\mathbb N$ は自然数対象である。$\square$

$\bar g:=\lambda g\colon1\to X^A$ と、$F:=\lambda\bigl(h\circ\langle\mathrm{ev},\pi_A\rangle\bigr)\colon X^A\to X^A$（$\langle\mathrm{ev},\pi_A\rangle\colon X^A\times A\to X\times A$）をとる。定義により $v\circ0=\bar g$、$v\circ s=F\circ v$ を満たす $v\colon N\to X^A$ がただ一つある。
存在。 $u:=\mathrm{ev}\circ(v\times\operatorname{id}_A)$ とおく。$u\circ(0\times\operatorname{id}_A)=\mathrm{ev}\circ(\bar g\times\operatorname{id}_A)=g$ である。また
$$ u\circ(s\times\operatorname{id}_A)=\mathrm{ev}\circ(F\times\operatorname{id}_A)\circ(v\times\operatorname{id}_A)=h\circ\langle\mathrm{ev},\pi_A\rangle\circ(v\times\operatorname{id}_A)=h\circ\langle u,\pi_A\rangle $$
である（最後は $\langle\mathrm{ev},\pi_A\rangle\circ(v\times\operatorname{id}_A)=\langle\mathrm{ev}\circ(v\times\operatorname{id}_A),\pi_A\rangle$ による）。
一意性。 $u'$ が 2 式を満たすとし、$v':=\lambda u'$ とおく。$v'\circ0=\lambda(u'\circ(0\times\operatorname{id}_A))=\lambda g=\bar g$ である。さらに $\lambda$ の性質から
$$ \lambda^{-1}(F\circ v')=h\circ\langle\mathrm{ev},\pi_A\rangle\circ(v'\times\operatorname{id}_A)=h\circ\langle u',\pi_A\rangle=u'\circ(s\times\operatorname{id}_A)=\lambda^{-1}(v'\circ s) $$
であり（$\lambda^{-1}(w)=\mathrm{ev}\circ(w\times\operatorname{id}_A)$）、$\lambda$ は全単射なので $F\circ v'=v'\circ s$ である。よって $v'=v$ であり、$u'=\mathrm{ev}\circ(v'\times\operatorname{id}_A)=u$ である。$\square$