解対象から成る図式 (Ai)i をとり、 その余極限余錐 (pi:Ai→A)i が存在したとする。 すると、 各 i に対して、 Ai が解対象であることから、 φA∘Fpi=Gpi∘φAi=Gpi∘ψAi=ψA∘Fpi が成り立つ。 一方、 F は余極限を保存するから、 (Fpi:FAi→FA)i も余極限である。 したがって、 余極限に関する分解の一意性によって φA=ψA が得られ、 A は解である。

全射 f:B↠A をとり、 B は解であるとする。 F は全射を保存するから、 Ff も全射である。 ここで、 φA∘Ff=Gf∘φB=Gf∘ψB=φA∘Ff が成り立つから、 Ff が全射であることより φA=ψA が成り立つ。 したがって、 A も解である。

F は余極限を保存するから、 命題 6.3 によって Sol(F,G,φ,ψ) は余極限に関して閉じている。 さらに、 󰒯 は余完備だから、 これより Sol(F,G,φ,ψ) も余完備である。 したがって、 󰒯 は冪化可能であることを合わせて、 関手 r: 󰒯 ⟶ Sol(F,G,φ,ψ) A ⟼ ⋃{A󰎘∈Sub󰒯(A)∣A󰎘 は解} が定義できる。 各 󰒯 の対象 A に対し、 定義から rA は A の部分対象だから、 射 ξA:rA↣A がある。

任意に解対象 B および射 f:B→A をとると、 仮定によって f の全射と単射による分解 BAXfei がとれる。 F は余極限を保存するから特に全射を保存するので、 命題 6.4 によって X は解である。 したがって X⊆rA であり、 BXrAAfeξA は可換である。 さらに、 ξA は単射だから、 このような分解は常に一意である。 以上により、 r は包含関手の右随伴関手となるから、 Sol(F,G,φ,ψ) は余反射的である。

f が単射でないと仮定する。 すると、 PComon(󰒚) の射 g,g󰎘:(C,d󰎙,e󰎙)→(B,d󰎘,e󰎘) が存在して、 g≠g󰎘 かつ f∘g=f∘g󰎘 が成り立つ。 ここで、 󰔄g := ❲󰔄BB⫫C⫫b♯g⫫❲ 󰔄g󰎘 := ❲󰔄BB⫫C⫫b♯g󰎘⫫❲ とおくと、 これらは PComon(Chu(󰒚,⫫)) の射 (g,󰔄g),(g󰎘,󰔄g󰎘):((C,C⫫,εC),(d󰎙,d󰎙⫫),(e󰎙,e󰎙⫫))→((B,󰔄B,b),(d󰎘,m󰎘),(e󰎘,u󰎘)) を定め、 さらに (f,󰔄f)∘(g,󰔄g)=(f,󰔄f)∘(g󰎘,󰔄g󰎘) が成り立つ。 (f,󰔄f) は単射だったから (g,󰔄g)=(g󰎘,󰔄g󰎘) が成り立つが、 これは g≠g󰎘 に矛盾する。 以上により、 f は単射である。

󰔄p が全射でないと仮定する。 すると、 PMon(󰒚/B⫫) の射 󰔄g,󰔄g󰎘:((󰔄B,b♯),m󰎘,u󰎘)→((󰔄C,c♯),m󰎙,u󰎙) が存在して、 󰔄g≠󰔄g󰎘 かつ 󰔄g∘󰔄p=󰔄g󰎘∘󰔄p が成り立つ。 ここで、 PComon(Chu(󰒚,⫫)) の射 (id,󰔄g),(id,󰔄g󰎘):((B,C⫫,c),(d󰎘,m󰎙),(e󰎘,u󰎙))→((B,󰔄B,b),(d󰎘,m󰎘),(e󰎘,u󰎘)) が考えられるが、 󰔄g∘󰔄p=󰔄g󰎘∘󰔄p より 󰔄g∘󰔄f=󰔄g󰎘∘󰔄f が得られるから、 (f,󰔄f)∘(id,󰔄g)=(f,󰔄f)∘(id,󰔄g󰎘) が成り立つ。 (f,󰔄f) は単射だったから (id,󰔄g)=(id,󰔄g󰎘) が成り立つが、 これは 󰔄g≠󰔄g󰎘 に矛盾する。 以上により、 󰔄p は全射である。

PComon(Chu(󰒚,⫫)) の対象 ((A,󰔄A,a),(d,m),(e,u)) を 1 つとって固定する。 これの部分対象が集合サイズしか存在しないことを示せば良い。

部分対象 (f,󰔄f):((B,󰔄B,b),(d󰎘,m󰎘),(e󰎘,u󰎘))↣((A,󰔄A,a),(d,m),(e,u)) をとると、 命題 6.6 によって f:(B,d󰎘,e󰎘)↣(A,d,e) は PComon(󰒚) における部分対象である。

一方、 a󰎘♯:=❲󰔄AA⫫B⫫a♯f⫫❲ とおくと、 󰒚/B⫫ の射 󰔄f:(󰔄A,a󰎘♯)→(󰔄B,b♯) が考えられる。 ここで、 仮定から忘却関手 WB:PMon(󰒚/B⫫)→󰒚/B⫫ には左随伴関手 LB が存在する。 これを用いて ((󰔄X,x♯),m󰎙,u󰎙):=LB(󰔄A,a󰎘♯) とおけば、 随伴によって、 Hom󰒚/B⫫((󰔄A,a󰎘♯),(B,b♯))≅HomPMon(󰒚/B⫫)(((󰔄X,x♯),m󰎙,u󰎙),((B,b♯),m󰎘,u󰎘)) が成り立つ。 󰔄f はこの右辺に属するから、 それに対応する左辺の元として 󰔄p:((󰔄X,x♯),m󰎙,u󰎙)→((B,b♯),m󰎘,u󰎘) がとれ、 随伴の単位から定まる射を ξ:(󰔄A,a󰎘♯)→(󰔄X,x♯) とおけば、 󰔄A󰔄B󰔄X󰔄f󰔄pξ は可換である。 したがって、 命題 6.7 によって 󰔄p は PMon(󰒚/B⫫) における商対象である。

以上の議論により、 PComon(Chu(󰒚,⫫)) における ((A,󰔄A,a),(d,m),(e,u)) の部分対象 (f,󰔄f) に対し、 󰄘f∈SubPComon(󰒚)((A,d,e))(B,d󰎘,e󰎘):=dom(f)󰄘a󰎘♯∈Hom󰒚(A,B⫫)QuotPMon(󰒚/B⫫)(LB(A,a󰎘♯)) の元 (f,a󰎘♯,󰔄p) が 1 つ定まり、 この対応は単射である。 仮定から PComon(󰒚) は冪化可能で PMon(󰒚/B⫫) は余冪化可能であるから、 上のクラスは集合である。 したがって、 ((A,󰔄A,a),(d,m),(e,u)) の部分対象は集合サイズしかない。

仮定から 󰒚 は完備かつ余完備だから、 Chu(󰒚,⫫) は特に余完備であり、 さらに忘却関手 U:PComon(Chu(󰒚,⫫))→Chu(󰒚,⫫) が余極限を生成することから PComon(Chu(󰒚,⫫)) も余完備である。 さらに、 仮定と命題 6.8 によって PComon(Chu(󰒚,⫫)) は冪化可能である。 また、 仮定から PComon(Chu(󰒚,⫫)) は全射単射分解をもつ。 最後に、 PComon(Chu(󰒚,⫫))=Sol(F,G,φ,ψ) と表したときの F は忘却関手だったから、 これは余極限を保存する。 以上によって命題 6.5 が使えるので、 PComon(Chu(󰒚,⫫)) は余反射的であり、 これは I に右随伴関手が存在するということである。

仮定と定理 6.9 から、 包含関手 I:Comon(Chu(󰒚,⫫))→PComon(Chu(󰒚,⫫)) は右随伴関手をもつ。 さらに、 仮定と定理 5.3 から、 忘却関手 U:PComon(Chu(󰒚,⫫))→Chu(󰒚,⫫) も右随伴関手をもつ。 したがって、 これらの合成 U∘I も右随伴関手をもつが、 これは Chu(󰒚,⫫) が Lafont 圏であるということである。