「依存型理論で述語論理が出来てしまう理由」において、2つの圏をもとにしてハイパードクトリンを構成する方法の概略を示しました。このハイパードクトリンは、依存型理論と述語論理のどちらも記述できる汎用的な機構になっています。銀河（型をホストする圏…