Disjunction and Existence Properties via Gluing Constructions

This thesis gives a uniform categorical proof of the disjunction property (DP) and of the existence property (EP) for intuitionistic predicate logic, Heyting arithmetic HA, the arithmetic of finite types HAω (extensional and intensional) and higher order Heyting arithmetic HAH. These results are known; we recover them in the language of doctrines by Maietti and Rosolini. We start from the construction in the notes by Maietti. Then for HA we develop the gluing by Shirasu in terms of first order doctrines. Our original contribution is to adopt the Shirasu gluing for HA and HAω and the generalization of the Shirasu’s gluing as comma object in the 2-category of the primary doctrines with some condition for the generalized gluing to preserve triposes.