Sub(1)実現問題の随伴化

## Trigger chatgptで「任意のHeyting algebraは小さいelementary toposの(mathrm{Sub}(1))として実現できるか」というPittsの問題を検討した際，洞が，既存の具体的構成を追うより [ mathcal Elongmapsto mathrm{Sub}_{mathcal E}(1) ] を2-functorとして書き，その随伴を見る方が構造的ではないかと提案した． ## Idea 適切な2-category of small elementary topoiとHeyting algebrasを選び， [ T:mathbf{ETop}^{mathrm{log}}_{mathrm{sm}}longrightarrowmathbf{Heyt}, qquad T(mathcal E)=mathrm{Sub}_{mathcal E}(1) ] を定義する．(T)にleft biadjoint (L) が存在するかを調べ，存在すればclosure-like endofunctor [ C:=T L ] を解析する．Pittsのessential-surjectivity問題を，unit (H o C(H)) が同型になる条件，または(C(H) woheadrightarrow H)という自然なretraction／quotientを構成する問題へ移す． (mathrm{Sub}(1))だけではsubstitutionを失うため，必要なら対象をhyperdoctrine [ mathcal Elongmapsto mathrm{Sub}_{mathcal E}(-) ] へ持ち上げ，その後global truth-value部分へ戻す． ## Goal Heyting algebraのtopos実現問題を，個別構成ではなく2-adjunction・monad・essential imageの問題として再定式化する．2-categoryの射の選択，smallness，biadjointの存在が最初の技術課題である．