Implicative algebras II:
completeness w.r.t. Set-based triposes

Alexandre Miquel Instituto de Matemática y Estadística Prof. Ing. Rafael Laguardia
Facultad de Ingeniería – Universidad de la República
Julio Herrera y Reissig 565 – Montevideo C.P. 11300 – URUGUAY

(Date: November, 2020)

Abstract.

We prove that all $\mathbf{Set}$ -based triposes are implicative triposes.

1. Introduction

In [3], we introduced the notion of implicative algebra, a simple algebraic structure that is intended to factorize the model constructions underlying forcing and realizability, both in intuitionistic and classical logic. We showed that this algebraic structure induces a large class of ( $\mathbf{Set}$ -based) triposes—the implicative triposes—, that encompasses all (intuitionistic and classical) forcing triposes, all classical realizability triposes (both in the sense of Streicher [6] and Krivine [3]) as well as all the intuitionistic realizability triposes induced by partial combinatory algebras (in the style of Hyland, Johnstone and Pitts [2]).

The aim of this paper is to prove that the class of implicative triposes actually encompasses all $\mathbf{Set}$ -based triposes, in the sense that:

Theorem 1.1.

Each $\mathbf{Set}$ -based tripos is (isomorphic to) an implicative tripos.

For that, we first recall some notions about triposes and implicative algebras.

1.1. $\mathbf{Set}$ -based triposes

In what follows, we write:

•

$\mathbf{Set}$ the category of sets equipped with all functions;
•

$\mathbf{Pos}$ the category of posets equipped with monotonic functions;
•

$\mathbf{HA}$ the category of Heyting algebras equipped with the corresponding morphisms.

In the category $\mathbf{Set}$ , we write:

•

$1$ the terminal object (i.e. a fixed singleton);
•

$1_{X}:X\to 1$ the unique map from a given set $X$ to $1$ ;
•

$X\times Y$ the Cartesian product of two sets $X$ and $Y$ , and
•

$\pi_{X,Y}:X\times Y\to X$ and $\pi^{\prime}_{X,Y}:X\times Y\to Y$ the associated projections.
•

Finally, given two functions $f:Z\to X$ and $g:Z\to Y$ , we write $\langle f,g\rangle:Z\to X\times Y$ the unique function such that $\pi_{X,Y}\circ\langle f,g\rangle=f$ and $\pi^{\prime}_{X,Y}\circ\langle f,g\rangle=g$ .

Definition 1.2 ( $\mathbf{Set}$ -based triposes).

A $\mathbf{Set}$ -based tripos is a functor $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ that fulfills the following three conditions:

(1)

For each map $f:X\to Y$ ( $X,Y\in\mathbf{Set}$ ), the corresponding map $\mathsf{P}{f}:\mathsf{P}{Y}\to\mathsf{P}{X}$ has left and right adjoints in $\mathbf{Pos}$ , that are monotonic maps $\exists{f},\forall{f}:\mathsf{P}{X}\to\mathsf{P}{Y}$ such that

(for all ​ p \in 𝖯 ​ X, q \in 𝖯 ​ Y)

\begin{array}[]{rcl}\exists{f}(p)\leq q&\Leftrightarrow&p\leq\mathsf{P}{f}(q)\\[3.0pt] q\leq\forall{f}(p)&\Leftrightarrow&\mathsf{P}{f}(q)\leq p\\ \end{array}

(2)

Beck-Chevalley condition. Each pullback square in $\mathbf{Set}$ (on the left-hand side) induces the following two commutative diagrams in $\mathbf{Pos}$ (on the right-hand side):

\begin{array}[]{@{}c@{}}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 12.18057pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-7.53471pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\hbox to0.0pt{\vbox to0.0pt{\hbox to6.0pt{\vbox to6.0pt{\hbox to6.0pt{\hfil}\vfil\hrule}\hskip-0.4pt\vrule}\vss}\hss}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.84442pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.93471pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-12.18057pt\raise-19.31888pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-28.80444pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 32.93471pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 41.86942pt\raise-19.31888pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 41.86942pt\raise-28.80444pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-8.93471pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 15.13976pt\raise-43.82524pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g_{2}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 34.85553pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 34.85553pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y}$}}}}}}}\ignorespaces}}}}\ignorespaces\\ \end{array}\qquad{\Rightarrow}\qquad\begin{array}[]{c@{\qquad}c}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 16.94447pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-10.9375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 15.46945pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\exists{f_{1}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 36.3375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 36.3375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X_{1}}}$}}}}}}}{\hbox{\kern-12.3375pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X_{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-16.94447pt\raise-19.31888pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\mathsf{P}{f_{2}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 15.76477pt\raise-44.74886pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\exists{g_{2}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 38.25832pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 38.25832pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{Y}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 48.67499pt\raise-19.31888pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.71112pt\hbox{$\scriptstyle{\mathsf{P}{g_{1}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 48.67499pt\raise-4.80444pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces&\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 16.94447pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-10.9375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 15.46945pt\raise 6.1111pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\forall{f_{1}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 36.3375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 36.3375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X_{1}}}$}}}}}}}{\hbox{\kern-12.3375pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X_{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-16.94447pt\raise-19.31888pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\mathsf{P}{f_{2}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 15.76477pt\raise-44.74886pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\forall{g_{2}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 38.25832pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 38.25832pt\raise-38.63776pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{Y}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 48.67499pt\raise-19.31888pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.71112pt\hbox{$\scriptstyle{\mathsf{P}{g_{1}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 48.67499pt\raise-4.80444pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces\\ \end{array}

That is: $\exists{f_{1}}\circ\mathsf{P}{f_{2}}~{}=~{}\mathsf{P}{g_{1}}\circ\exists{g_{2}}$ and $\forall{f_{1}}\circ\mathsf{P}{f_{2}}~{}=~{}\mathsf{P}{g_{1}}\circ\forall{g_{2}}$ .

(3)

The functor $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ has a generic predicate, that is: a predicate $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ (for some set $\Sigma$ ) such that for all sets $X$ , the following map is surjective:

\begin{array}[]{r@{~{}~}c@{~{}~}l}\Sigma^{X}~{}{}&\to\hfil~{}{}&\mathsf{P}{X}\\ \sigma~{}{}&\mapsto\hfil~{}{}&\mathsf{P}\sigma(\textit{tr}_{\Sigma})\\ \end{array}

Remarks 1.3.

(1) Given a map $f:X\to Y$ , the left and right adjoints $\exists{f},\forall{f}:\mathsf{P}{X}\to\mathsf{P}{Y}$ of the substitution map $\mathsf{P}{f}:\mathsf{P}{Y}\to\mathsf{P}{X}$ are always monotonic functions (due to the adjunction), but in general they are not morphisms of Heyting algebras. Moreover, both correspondences $f\mapsto\exists{f}$ and $f\mapsto\forall{f}$ are functorial, in the sense that

\begin{array}[]{c@{\qquad\qquad}c}\exists(g\circ f)~{}=~{}\exists{g}\circ\exists{f}&\exists\mathrm{id}_{X}~{}=~{}\mathrm{id}_{\mathsf{P}{X}}\\ \forall(g\circ f)~{}=~{}\forall{g}\circ\forall{f}&\forall\mathrm{id}_{X}~{}=~{}\mathrm{id}_{\mathsf{P}{X}}\\ \end{array}

for all sets $X$ , $Y$ , $Z$ and for all maps $f:X\to Y$ and $g:Y\to Z$ . So that we can see $\exists$ and $\forall$ as covariant functors from $\mathbf{Set}$ to $\mathbf{Pos}$ , whose action on sets is given by $\exists{X}=\forall{X}=\mathsf{P}{X}$ .

(2) When defining the notion of tripos, some authors [5] require that the Beck-Chevalley condition hold only for the pullback squares of the form

(in ​ 𝐒𝐞𝐭)

\begin{array}[]{@{}c@{}}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 25.08615pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-17.41661pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z\times X\hbox to0.0pt{\vbox to0.0pt{\hbox to6.0pt{\vbox to6.0pt{\hbox to6.0pt{\hfil}\vfil\hrule}\hskip-0.4pt\vrule}\vss}\hss}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 21.71696pt\raise 5.57916pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.43472pt\hbox{$\scriptstyle{\pi_{Z,X}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 54.18661pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-25.08615pt\raise-19.2222pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.74722pt\hbox{$\scriptstyle{f\times\mathrm{id}_{X}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-27.05554pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 54.18661pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 60.95744pt\raise-19.2222pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 60.95744pt\raise-27.05554pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-17.07553pt\raise-38.44441pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z^{\prime}\times X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 21.16586pt\raise-44.24579pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.21251pt\hbox{$\scriptstyle{\pi_{Z^{\prime},X}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 53.41661pt\raise-38.44441pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 53.41661pt\raise-38.44441pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Z^{\prime}}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{array}

Here, we follow [2, 3] by requiring that the Beck-Chevalley condition hold more generally for all pullback squares in $\mathbf{Set}$ .

(3) The meaning of the generic predicate $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ will be explained in Section 2.1.

Let us also recall that:

Definition 1.4 (Isomorphism of triposes).

Two triposes $\mathsf{P},\mathsf{P}^{\prime}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ are isomorphic when there is a natural isomorphism $\varphi:\mathsf{P}\Rightarrow\mathsf{P}^{\prime}$ .

Remark 1.5.

By a natural isomorphism $\varphi:\mathsf{P}\Rightarrow\mathsf{P}^{\prime}$ , we mean any family of isomorphisms $\varphi_{X}:\mathsf{P}{X}\to\mathsf{P}^{\prime}{X}$ (indexed by $X\in\mathbf{Set}$ ) such that for all maps $f:X\to Y$ ( $X,Y\in\mathbf{Set}$ ), the following diagram commutes:

Note that here, the notion of isomorphism can be taken indifferently in the sense of $\mathbf{HA}$ or $\mathbf{Pos}$ , since a map $\varphi_{X}:\mathsf{P}{X}\to\mathsf{P}^{\prime}{X}$ is an isomorphism of Heyting algebras if and only if it is an isomorphism between the underlying posets.

To conclude this presentation of triposes, we recall a few facts about left and right adjoints:

Lemma 1.6.

For all maps $f:X\to Y$ and for all predicates $p,p^{\prime}\in\mathsf{P}{X}$ , we have:

\begin{array}[]{l@{\qquad\qquad}l}\exists{f}(p\lor p^{\prime})~{}=~{}\exists{f}(p)\lor\exists{f}(p^{\prime})&\exists{f}(\bot_{X})~{}=~{}\bot_{Y}\\[3.0pt] \forall{f}(p\land p^{\prime})~{}=~{}\forall{f}(p)\land\forall{f}(p^{\prime})&\forall{f}(\top_{X})~{}=~{}\top_{Y}\\ \end{array}

Proof.

Let us treat the case of $\exists{f}$ . For all $q\in\mathsf{P}{Y}$ , we have

\begin{array}[]{r@{\quad}c@{\quad}l}\exists{f}(p\lor p^{\prime})\leq q&\text{iff}&p\lor p^{\prime}\leq\mathsf{P}{f}(q)\\ &\text{iff}&p\leq\mathsf{P}{f}(q)~{}{}~{}\text{and}~{}{}~{}p^{\prime}\leq\mathsf{P}{f}(q)\\ &\text{iff}&\exists{f}(p)\leq q~{}{}~{}\text{and}~{}{}~{}\exists{f}(p^{\prime})\leq q\\ &\text{iff}&\exists{f}(p)\lor\exists{f}(p^{\prime})\leq q\\ \end{array}

hence $\exists{f}(p\lor p^{\prime})=\exists{f}(p)\lor\exists{f}(p^{\prime})$ . Moreover, we have $\bot_{X}\leq\mathsf{P}{f}(\bot_{Y})$ , hence $\exists{f}(\bot_{X})\leq\bot_{Y}$ , and thus $\exists{f}(\bot_{X})=\bot_{Y}$ . The proofs of the corresponding properties for $\forall{f}$ proceed dually. ∎

Lemma 1.7.

Given a map $f:X\to Y$ :

(1)

If $f$ has an inverse (i.e. $f$ is bijective), then $\exists{f}$ and $\forall{f}$ are the inverse of $\mathsf{P}{f}$ :

$\exists{f}~{}=~{}\forall{f}~{}=~{}\mathsf{P}{f^{-1}}~{}=~{}(\mathsf{P}{f})^{-1}\,.$
(2)

If $f$ has a right inverse, then $\exists{f}$ and $\forall{f}$ are left inverses of $\mathsf{P}{f}$ :

$\exists{f}\circ\mathsf{P}{f}~{}=~{}\forall{f}\circ\mathsf{P}{f}~{}=~{}\mathrm{id}_{\mathsf{P}{Y}}\,.$
(3)

If $f$ has a left inverse, then $\exists{f}$ and $\forall{f}$ are right inverses of $\mathsf{P}{f}$ :

$\mathsf{P}{f}\circ\exists{f}~{}=~{}\mathsf{P}{f}\circ\forall{f}~{}=~{}\mathrm{id}_{\mathsf{P}{X}}\,.$

Proof.

(1) If $f:X\to Y$ is bijective, then for all $p\in\mathsf{P}{X}$ and $q\in\mathsf{P}{Y}$ , we have

•

$\exists{f}(p)\leq q~{}{}~{}\text{iff}~{}{}~{}p\leq\mathsf{P}{f}(q)~{}{}~{}\text{iff}~{}{}~{}(\mathsf{P}{f})^{-1}(p)\leq q$ , hence: $\exists{f}=(\mathsf{P}{f})^{-1}(p)=\mathsf{P}{f^{-1}}(p).$
•

$q\leq\forall{f}(p)~{}{}~{}\text{iff}~{}{}~{}\mathsf{P}{f}(q)\leq p~{}{}~{}\text{iff}~{}{}~{}q\leq(\mathsf{P}{f})^{-1}(p)$ , hence: $\forall{f}=(\mathsf{P}{f})^{-1}(p)=\mathsf{P}{f^{-1}}(p).$

(2) Let $g:Y\to X$ such that $f\circ g=\mathrm{id}_{Y}$ . By functoriality, we get $\mathsf{P}{g}\circ\mathsf{P}{f}=\mathrm{id}_{\mathsf{P}{Y}}$ , hence the map $\mathsf{P}{f}:\mathsf{P}{Y}\to\mathsf{P}{X}$ is an embedding of posets. For all $q,q^{\prime}\in\mathsf{P}{Y}$ , we thus have:

•

$\exists{f}(\mathsf{P}{f}(q))\leq q^{\prime}~{}{}~{}\text{iff}~{}{}~{}\mathsf{P}{f}(q)\leq\mathsf{P}{f}(q^{\prime})~{}{}~{}\text{iff}~{}{}~{}q\leq q^{\prime}$ , hence $\exists{f}\circ\mathsf{P}{f}=\mathrm{id}_{\mathsf{P}{Y}}$ .
•

$q^{\prime}\leq\forall{f}(\mathsf{P}{f}(q))~{}{}~{}\text{iff}~{}{}~{}\mathsf{P}{f}(q^{\prime})\leq\mathsf{P}{f}(q)~{}{}~{}\text{iff}~{}{}~{}q^{\prime}\leq q$ , hence $\forall{f}\circ\mathsf{P}{f}=\mathrm{id}_{\mathsf{P}{Y}}$ .

(3) Let $g:Y\to X$ such that $g\circ f=\mathrm{id}_{X}$ . By functoriality, we get $\forall{g}\circ\forall{f}=\exists{g}\circ\exists{f}=\mathrm{id}_{\mathsf{P}{X}}$ , hence $\exists{f},\forall{f}:\mathsf{P}{X}\to\mathsf{P}{Y}$ are embeddings of posets. For all $p,p^{\prime}\in\mathsf{P}{X}$ , we thus have:

•

$p^{\prime}\leq\mathsf{P}{f}(\exists{f}(p))~{}{}~{}\text{iff}~{}{}~{}\exists{f}(p^{\prime})\leq\exists{f}(p)~{}{}~{}\text{iff}~{}{}~{}p^{\prime}\leq p$ , hence $\mathsf{P}{f}\circ\exists{f}=\mathrm{id}_{\mathsf{P}{X}}$ .
•

$\mathsf{P}{f}(\forall{f}(p))\leq p^{\prime}~{}{}~{}\text{iff}~{}{}~{}\forall{f}(p)\leq\forall{f}(p^{\prime})~{}{}~{}\text{iff}~{}{}~{}p\leq p^{\prime}$ , hence $\mathsf{P}{f}\circ\forall{f}=\mathrm{id}_{\mathsf{P}{X}}$ .∎

1.2. Implicative algebras

Recall that:

•
An implicative structure is a complete (meet-semi)lattice $(\mathscr{A},{\preccurlyeq})$ equipped with a binary operation $({\to}):\mathscr{A}^{2}\to\mathscr{A}$ such that:
1. (1)
  
  If $a^{\prime}\preccurlyeq a$ and $b\preccurlyeq b^{\prime}$ , then $(a\to b)\preccurlyeq(a^{\prime}\to b^{\prime})$ .
2. (2)
  
  For all $a\in\mathscr{A}$ and $B\subseteq\mathscr{A}$ , we have: $\displaystyle a\to\bigcurlywedge_{b\in B}\!\!b~{}=~{}\bigcurlywedge_{b\in B}\!(a\to b)$ .
•
A separator of an implicative structure $(\mathscr{A},{\preccurlyeq},{\to})$ is a subset $S\subseteq\mathscr{A}$ such that:
1. (1)
  
  If $a\in S$ and $a\preccurlyeq a^{\prime}$ , then $a^{\prime}\in S$ .
2. (2)
  
  $\bigcurlywedge_{a,b\in\mathscr{A}}(a\to b\to c)~{}{}~{}({=}~{}\mathbf{K}^{\mathscr{A}})~{}\in~{}S$ and
  $\bigcurlywedge_{a,b,c\in\mathscr{A}}((a\to b\to c)\to(a\to b)\to a\to c)~{}{}~{}({=}~{}\mathbf{S}^{\mathscr{A}})~{}\in~{}S$ .
3. (3)
  
  If $(a\to b)\in S$ and $a\in S$ , then $b\in S$ .
Moreover, we say that a separator $S\subseteq\mathscr{A}$ is classical when
1. (4)
  
  $\bigcurlywedge_{a,b\in\mathscr{A}}(((a\to b)\to a)\to a)~{}{}~{}({=}~{}\mathbf{cc}^{\mathscr{A}})~{}\in~{}S$ .
•

An implicative algebra is a quadruple $(\mathscr{A},{\preccurlyeq},{\to},S)$ where $(\mathscr{A},{\preccurlyeq},{\to})$ is an implicative structure and where $S\subseteq\mathscr{A}$ is a separator. An implicative algebra is classical when the underlying separator $S\subseteq\mathscr{A}$ is classical.

In [3, §4], we have seen that each implicative algebra $(\mathscr{A},{\preccurlyeq},{\to},S)$ induces a $\mathbf{Set}$ -based tripos $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ that is defined as follows:

•

For each set $X$ , the corresponding Heyting algebra $\mathsf{P}{X}$ is defined as the poset reflection of the preordered set $(\mathscr{A}^{X},\vdash_{S[X]})$ whose preorder $\vdash_{S[X]}$ is given by

$(for all a, b \in 𝒜^{X})$ $a\vdash_{S[X]}b\quad\Leftrightarrow\quad\bigcurlywedge_{x\in X}(a_{x}\to b_{x})~{}\in~{}S$

The quotient $\mathscr{A}^{X}/{\mathrel{{\dashv}{\vdash}}_{S[X]}}~{}({=}~{}\mathsf{P}{X})$ is also written $\mathscr{A}^{X}/S[X]$ .
•

For each map $f:X\to Y$ , the corresponding substitution map $\mathsf{P}{f}:\mathsf{P}{Y}\to\mathsf{P}{X}$ is the (unique) morphism of Heyting algebras that factors the map $\mathscr{A}^{f}:\mathscr{A}^{Y}\to\mathscr{A}^{X}$ through the quotients $\mathsf{P}{Y}=\mathscr{A}^{Y}/S[Y]$ and $\mathsf{P}{X}=\mathscr{A}^{X}/S[X]$ .

The aim of this paper is thus to show that all $\mathbf{Set}$ -based triposes are of this form.

2. Anatomy of a $\mathbf{Set}$ -based tripos

The results presented in this section are essentially taken from [2, 4].

2.1. The generic predicate

From now on, we work with a fixed tripos $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ .

From the definition, $\mathsf{P}$ has a generic predicate, that is: a predicate $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ (for some set $\Sigma$ ) such that for each set $X$ , the corresponding ‘decoding map’ is surjective:

\begin{array}[]{r@{~{}~}c@{~{}~}l}\llbracket\_\rrbracket_{X}~{}:~{}\Sigma^{X}~{}{}&\to\hfil~{}{}&\mathsf{P}{X}\\ \sigma~{}{}&\mapsto\hfil~{}{}&\mathsf{P}\sigma(\textit{tr}_{\Sigma})\\ \end{array}

Intuitively, $\Sigma$ can be thought of as the set of (codes of) propositions, whereas $\Sigma^{X}$ can be thought of as the set of propositional functions over $X$ . The above condition thus expresses that each predicate $p\in\mathsf{P}{X}$ is represented by at least one propositional function $\sigma\in\Sigma^{X}$ such that $\llbracket\sigma\rrbracket_{X}=p$ , which we shall call a code for the predicate $p$ .

Notation 2.1.

Given a code $\sigma\in\Sigma^{X}$ , the predicate $\llbracket\sigma\rrbracket_{X}\in\mathsf{P}{X}$ will be often written $\llbracket\sigma_{x}\rrbracket_{x\in{X}}$ . In particular, given an individual code $\xi\in\Sigma$ , we write $(\xi)_{\_\in 1}\in\Sigma^{1}$ the corresponding constant family indexed by the singleton $1$ , and $\llbracket\xi\rrbracket_{\_\in 1}\in\mathsf{P}{1}$ the associated predicate.

Fact 2.2 (Naturality of $\llbracket\_\rrbracket_{X}$ ).

The decoding map $\llbracket\_\rrbracket_{X}:\Sigma^{X}\to\mathsf{P}{X}$ is natural in $X$ , in the sense that for each map $f:X\to Y$ , the following diagram commutes:

(σ \in Σ^{Y})

\begin{array}[]{@{}c@{}}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 21.18057pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-9.15056pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma^{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 8.23013pt\raise 7.5pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\llbracket\_\rrbracket_{X}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 33.15056pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 33.15056pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{X}}$}}}}}}}{\hbox{\kern-8.85889pt\raise-38.74664pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Sigma^{Y}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 8.43848pt\raise-46.24664pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\llbracket\_\rrbracket_{Y}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 33.67139pt\raise-38.74664pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern-21.18057pt\raise-19.37332pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\_\circ f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 33.67139pt\raise-38.74664pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathsf{P}{Y}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 44.08806pt\raise-19.37332pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\mathsf{P}{f}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 44.08806pt\raise-3.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces\\ \end{array}\qquad\llbracket\sigma\circ f\rrbracket_{X}~{}=~{}\mathsf{P}{f}(\llbracket\sigma\rrbracket_{Y})

Proof.

For all $\sigma\in\Sigma^{Y}$ , we have $\llbracket\sigma\circ f\rrbracket_{X}=\mathsf{P}(\sigma\circ f)(\textit{tr}_{\Sigma})=\mathsf{P}{f}(\mathsf{P}\sigma(\textit{tr}_{\Sigma}))=\mathsf{P}{f}(\llbracket\sigma\rrbracket_{Y})$ . ∎

Remarks 2.3 (Non-uniqueness of generic predicates).

It is important to observe that in a $\mathbf{Set}$ -based tripos $\mathsf{P}$ , the generic predicate is never unique.

•

Indeed, given a generic predicate $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ and a surjection $h:\Sigma^{\prime}\to\Sigma$ , we can always construct another generic predicate $\textit{tr}_{\Sigma^{\prime}}\in\mathsf{P}\Sigma^{\prime}$ by letting $\textit{tr}_{\Sigma^{\prime}}=\mathsf{P}{h}(\textit{tr}_{\Sigma})$ ¹¹1To prove that $\textit{tr}_{\Sigma^{\prime}}\in\mathsf{P}\Sigma^{\prime}$ is another generic predicate, we actually need a right inverse of $h:\Sigma^{\prime}\to\Sigma$ , which exists by (AC). Without (AC), the same argument works by replacing ‘surjective’ with ‘having a right inverse’..
•

More generally, if $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ and $\textit{tr}_{\Sigma^{\prime}}\in\mathsf{P}\Sigma^{\prime}$ are two generic predicates of the same tripos $\mathsf{P}$ , then there always exist two conversion maps $h:\Sigma^{\prime}\to\Sigma$ and $h^{\prime}:\Sigma\to\Sigma^{\prime}$ such that $\textit{tr}_{\Sigma^{\prime}}=\mathsf{P}{h}(\textit{tr}_{\Sigma})$ and $\textit{tr}_{\Sigma}=\mathsf{P}{h^{\prime}}(\textit{tr}_{\Sigma^{\prime}})$ .

In what follows, we will work with a fixed generic predicate $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ .

2.2. Defining connectives on $\Sigma$

We want to show that the operations $\land$ , $\lor$ and $\to$ on each Heyting algebra $\mathsf{P}{X}$ ( $X\in\mathbf{Set}$ ) can be derived from analogous operations on the generic set $\Sigma$ of propositions. For that, we pick codes $({\mathbin{\dot{{\land}}}}),({\mathbin{\dot{{\lor}}}}),({\mathbin{\dot{{\to}}}})\in\Sigma^{\Sigma\times\Sigma}$ such that

\begin{array}[]{r@{~{}~}c@{~{}~}l}\llbracket\mathbin{\dot{{\land}}}\rrbracket_{\Sigma\times\Sigma}~{}{}&=\hfil~{}{}&\llbracket\pi\rrbracket_{\Sigma\times\Sigma}\land\llbracket\pi^{\prime}\rrbracket_{\Sigma\times\Sigma}\\[3.0pt] \llbracket\mathbin{\dot{{\lor}}}\rrbracket_{\Sigma\times\Sigma}~{}{}&=\hfil~{}{}&\llbracket\pi\rrbracket_{\Sigma\times\Sigma}\lor\llbracket\pi^{\prime}\rrbracket_{\Sigma\times\Sigma}\\[3.0pt] \llbracket\mathbin{\dot{{\to}}}\rrbracket_{\Sigma\times\Sigma}~{}{}&=\hfil~{}{}&\llbracket\pi\rrbracket_{\Sigma\times\Sigma}\to\llbracket\pi^{\prime}\rrbracket_{\Sigma\times\Sigma}\\ \end{array}\begin{array}[]{r@{}}({\in}~{}\mathsf{P}(\Sigma\times\Sigma))\\[3.0pt] ({\in}~{}\mathsf{P}(\Sigma\times\Sigma))\\[3.0pt] ({\in}~{}\mathsf{P}(\Sigma\times\Sigma))\\ \end{array}

writing $\pi,\pi^{\prime}:\Sigma\times\Sigma\to\Sigma$ the two projections from $\Sigma\times\Sigma$ to $\Sigma$ .

Proposition 2.4.

Let $X$ be a set. For all codes $\sigma,\tau\in\Sigma^{X}$ , we have

\begin{array}[]{r@{~{}~}c@{~{}~}l}\llbracket\sigma_{x}\mathbin{\dot{{\land}}}\tau_{x}\rrbracket_{x\in X}~{}{}&=\hfil~{}{}&\llbracket\sigma\rrbracket_{X}\land\llbracket\tau\rrbracket_{X}\\[3.0pt] \llbracket\sigma_{x}\mathbin{\dot{{\lor}}}\tau_{x}\rrbracket_{x\in X}~{}{}&=\hfil~{}{}&\llbracket\sigma\rrbracket_{X}\lor\llbracket\tau\rrbracket_{X}\\[3.0pt] \llbracket\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}\rrbracket_{x\in X}~{}{}&=\hfil~{}{}&\llbracket\sigma\rrbracket_{X}\to\llbracket\tau\rrbracket_{X}\\ \end{array}\begin{array}[]{r@{}}({\in}~{}\mathsf{P}{X})\\[3.0pt] ({\in}~{}\mathsf{P}{X})\\[3.0pt] ({\in}~{}\mathsf{P}{X})\\ \end{array}

Proof.

Let us treat (for instance) the case of implication:

∎

\begin{array}[b]{r@{~{}~}c@{~{}~}l}\llbracket\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}\rrbracket_{x\in X}~{}{}&=\hfil~{}{}&\llbracket({\mathbin{\dot{{\to}}}})\circ\langle\sigma,\tau\rangle\rrbracket_{X}~{}=~{}\mathsf{P}\langle\sigma,\tau\rangle\llbracket{\mathbin{\dot{{\to}}}}\rrbracket_{\Sigma\times\Sigma}\\ ~{}{}&=\hfil~{}{}&\mathsf{P}\langle\sigma,\tau\rangle\bigl{(}\llbracket\pi\rrbracket_{\Sigma\times\Sigma}\to\llbracket\pi^{\prime}\rrbracket_{\Sigma\times\Sigma}\bigr{)}\\ ~{}{}&=\hfil~{}{}&\mathsf{P}\langle\sigma,\tau\rangle\bigl{(}\llbracket\pi\rrbracket_{\Sigma\times\Sigma}\bigr{)}\to\mathsf{P}\langle\sigma,\tau\rangle\bigl{(}\llbracket\pi^{\prime}\rrbracket_{\Sigma\times\Sigma}\bigr{)}\\ ~{}{}&=\hfil~{}{}&\llbracket\pi\circ\langle\sigma,\tau\rangle\rrbracket_{X}\to\llbracket\pi^{\prime}\circ\langle\sigma,\tau\rangle\rrbracket_{X}~{}=~{}\llbracket\sigma\rrbracket_{X}\to\llbracket\tau\rrbracket_{X}\,.\\ \end{array}

Similarly, we pick codes $\dot{\bot},\dot{\top}\in\Sigma$ such that

\llbracket\dot{\bot}\rrbracket_{\_\in 1}=\bot_{1}\in\mathsf{P}(1)\qquad\text{and}\qquad\llbracket\dot{\top}\rrbracket_{\_\in 1}=\top_{1}\in\mathsf{P}(1)\,.

Again, we easily check that:

Proposition 2.5.

For each set $X$ , we have:

\begin{array}[]{r@{~{}~}r@{~{}~}c@{~{}~}l}\llbracket\dot{\bot}\rrbracket_{x\in X}~{}{}&=~{}{}&\bot_{X}\hfil~{}{}\\[3.0pt] \llbracket\dot{\top}\rrbracket_{x\in X}~{}{}&=~{}{}&\top_{X}\hfil~{}{}\\ \end{array}\begin{array}[]{r@{}}({\in}~{}\mathsf{P}{X})\\[3.0pt] ({\in}~{}\mathsf{P}{X})\\ \end{array}

Proof.

Let us treat (for instance) the case of $\top$ :

\llbracket\dot{\top}\rrbracket_{x\in X}~{}=~{}\llbracket(\dot{\top})_{\_\in 1}\circ 1_{X}\rrbracket_{X}~{}=~{}\mathsf{P}{1_{X}}(\llbracket\dot{\top}\rrbracket_{\_\in 1})~{}=~{}\mathsf{P}{1_{X}}(\top_{1})~{}=~{}\top_{X}

(writing $1_{X}:X\to 1$ the unique map from $X$ to $1$ ). ∎

2.3. Defining quantifiers on $\Sigma$

In this section, we propose to show that the adjoints

(for each ​ f : X \to Y)

\exists{f},\forall{f}~{}:~{}\mathsf{P}{X}\to\mathsf{P}{Y}

can be derived from suitable quantifiers on the generic set $\Sigma$ of propositions. For that, we consider the membership relation $E:=\{(\xi,s):\xi\in s\}\subseteq\Sigma\times\mathfrak{P}(\Sigma)$ and write $e_{1}:E\to\Sigma$ and $e_{2}:E\to\mathfrak{P}(\Sigma)$ the corresponding projections. We pick two codes $\mathbin{\dot{{\bigvee}}},\mathbin{\dot{{\bigwedge}}}\in\Sigma^{\mathfrak{P}(\Sigma)}$ such that

\begin{array}[]{r@{~~}c@{~~}l}\llbracket\mathbin{\dot{{\bigvee}}}\rrbracket_{\mathfrak{P}(\Sigma)}~{}~{}&=\hfil~{}~{}&\exists{e_{2}}(\llbracket e_{1}\rrbracket_{E})\\[3.0pt] \llbracket\mathbin{\dot{{\bigwedge}}}\rrbracket_{\mathfrak{P}(\Sigma)}~{}~{}&=\hfil~{}~{}&\forall{e_{2}}(\llbracket e_{1}\rrbracket_{E})\\ \end{array}\begin{array}[]{r@{}}({\in}~{}\mathsf{P}(\mathfrak{P}(\Sigma)))\\[3.0pt] ({\in}~{}\mathsf{P}(\mathfrak{P}(\Sigma)))\\ \end{array}

Proposition 2.6.

Given a code $\sigma\in\Sigma^{X}$ and a map $f:X\to Y$ , we have:

\begin{array}[]{r@{~{}~}c@{~{}~}l}\bigl{\llbracket}\mathbin{\dot{{\bigvee}}}\{\sigma_{x}:x\in f^{-1}(y)\}\bigr{\rrbracket}_{y\in Y}~{}{}&=\hfil~{}{}&\exists{f}(\llbracket\sigma\rrbracket_{X})\\[6.0pt] \bigl{\llbracket}\mathbin{\dot{{\bigwedge}}}\{\sigma_{x}:x\in f^{-1}(y)\}\bigr{\rrbracket}_{y\in Y}~{}{}&=\hfil~{}{}&\forall{f}(\llbracket\sigma\rrbracket_{X})\\ \end{array}\begin{array}[]{r@{}}({\in}~{}\mathsf{P}{Y})\\[6.0pt] ({\in}~{}\mathsf{P}{Y})\\ \end{array}

Proof.

Let us define the map $h:Y\to\mathfrak{P}(\Sigma)$ by $h(y):=\{\sigma_{x}:x\in f^{-1}(y)\}$ for all $y\in Y$ . From this definition and from the definitions of $\mathbin{\dot{{\bigvee}}}$ , $\mathbin{\dot{{\bigwedge}}}$ , we get

\begin{array}[]{rcl}\llbracket\mathbin{\dot{{\bigvee}}}\{\sigma_{x}:x\in f^{-1}(y)\}\rrbracket_{y\in Y}&=&\llbracket{\mathbin{\dot{{\bigvee}}}}\circ h\rrbracket_{Y}~{}=~{}\mathsf{P}{h}\bigl{(}\llbracket\mathbin{\dot{{\bigvee}}}\rrbracket_{\mathfrak{P}(\Sigma)}\bigr{)}~{}=~{}\mathsf{P}{h}\bigl{(}\exists{e_{2}}(\llbracket e_{1}\rrbracket_{E})\bigr{)}\\[3.0pt] \llbracket\mathbin{\dot{{\bigwedge}}}\{\sigma_{x}:x\in f^{-1}(y)\}\rrbracket_{y\in Y}&=&\llbracket{\mathbin{\dot{{\bigwedge}}}}\circ h\rrbracket_{Y}~{}=~{}\mathsf{P}{h}\bigl{(}\llbracket\mathbin{\dot{{\bigwedge}}}\rrbracket_{\mathfrak{P}(\Sigma)}\bigr{)}~{}=~{}\mathsf{P}{h}\bigl{(}\forall{e_{2}}(\llbracket e_{1}\rrbracket_{E})\bigr{)}\\ \end{array}

Let us now consider the set $G\subseteq\Sigma\times Y$ defined by $G:=\{(\sigma_{x},f(x)):x\in X\}$ as well as the two functions $g:G\to Y$ and $g^{\prime}:G\to E$ given by

(for all ​ (ξ, y) \in G)

g(\xi,y)~{}:=~{}y\qquad\text{and}\qquad g^{\prime}(\xi,y)~{}:=~{}(\xi,h(y))

We observe that the following diagram is a pullback in $\mathbf{Set}$ :

Hence $\mathsf{P}{h}\circ\exists{e_{2}}=\exists{g}\circ\mathsf{P}{g^{\prime}}$ and $\mathsf{P}{h}\circ\forall{e_{2}}=\forall{g}\circ\mathsf{P}{g^{\prime}}$ (Beck-Chevalley), and thus:

\begin{array}[]{rcl}\bigl{\llbracket}\mathbin{\dot{{\bigvee}}}\{\sigma_{x}:x\in f^{-1}(y)\}\bigr{\rrbracket}_{y\in Y}&=&(\mathsf{P}{h}\circ\exists{e_{2}})(\llbracket e_{1}\rrbracket_{E})~{}=~{}(\exists{g}\circ\mathsf{P}{g^{\prime}})(\llbracket e_{1}\rrbracket_{E})\\[3.0pt] \bigl{\llbracket}\mathbin{\dot{{\bigwedge}}}\{\sigma_{x}:x\in f^{-1}(y)\}\bigr{\rrbracket}_{y\in Y}&=&(\mathsf{P}{h}\circ\forall{e_{2}})(\llbracket e_{1}\rrbracket_{E})~{}=~{}(\forall{g}\circ\mathsf{P}{g^{\prime}})(\llbracket e_{1}\rrbracket_{E})\\ \end{array}

Now we consider the map $q:X\to G$ defined by $q(x)=(\sigma_{x},f(x))$ for all $x\in X$ . Since $q$ is surjective, it has a right inverse by (AC), hence we have $\exists{q}\circ\mathsf{P}{q}=\forall{q}\circ\mathsf{P}{q}=\mathrm{id}_{\mathsf{P}{G}}$ by Lemma 1.7 (2). Therefore:

\begin{array}[]{r@{~~}c@{~~}l}\bigl{\llbracket}\mathbin{\dot{{\bigvee}}}\{\sigma_{x}:x\in f^{-1}(y)\}\bigr{\rrbracket}_{y\in Y}~{}~{}&=\hfil~{}~{}&(\exists{g}\circ\mathsf{P}{g^{\prime}})(\llbracket e_{1}\rrbracket_{E})~{}=~{}(\exists{g}\circ\exists{q}\circ\mathsf{P}{q}\circ\mathsf{P}{g^{\prime}})(\llbracket e_{1}\rrbracket_{E})\\ ~{}~{}&=\hfil~{}~{}&\bigl{(}\exists(g\circ q)\circ\mathsf{P}(g^{\prime}\circ q)\bigr{)}(\llbracket e_{1}\rrbracket_{E})~{}=~{}\exists{f}\bigl{(}\mathsf{P}(g^{\prime}\circ q)(\llbracket e_{1}\rrbracket_{E})\bigr{)}\\ ~{}~{}&=\hfil~{}~{}&\exists{f}\bigl{(}\llbracket e_{1}\circ g^{\prime}\circ q\rrbracket_{X}\bigr{)}~{}=~{}\exists{f}(\llbracket\sigma\rrbracket_{X})\\ \end{array}

(since $g\circ q=f$ and $e_{1}\circ g^{\prime}\circ q=\sigma$ ). And similarly for ${\forall}$ . ∎

2.4. Defining the ‘filter’ $\Phi$

In Sections 2.2 and 2.3, we introduced codes $({\mathbin{\dot{{\land}}}}),({\mathbin{\dot{{\lor}}}}),(\mathbin{\dot{{\to}}})\in\Sigma^{\Sigma\times\Sigma}$ and $\mathbin{\dot{{\bigvee}}},\mathbin{\dot{{\bigwedge}}}\in\Sigma^{\mathfrak{P}(\Sigma)}$ such that for all sets $X$ and for all predicates $p,q\in\mathsf{P}{X}$ :

•

If $\sigma,\tau\in\Sigma^{X}$ are codes for $p,q\in\mathsf{P}{X}$ , respectively, then:

\begin{array}[]{l@{\quad}l@{\qquad}l@{\qquad}l@{\quad}l}(\sigma_{x}\mathbin{\dot{{\land}}}\tau_{x})_{x\in X}&({\in}~{}\Sigma^{X})&\text{is a code for}&p\land q&({\in}~{}\mathsf{P}{X})\\[3.0pt] (\sigma_{x}\mathbin{\dot{{\lor}}}\tau_{x})_{x\in X}&({\in}~{}\Sigma^{X})&\text{is a code for}&p\lor q&({\in}~{}\mathsf{P}{X})\\[3.0pt] (\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x})_{x\in X}&({\in}~{}\Sigma^{X})&\text{is a code for}&p\to q&({\in}~{}\mathsf{P}{X})\\ \end{array}

•

If $\sigma\in\Sigma^{X}$ is a code for $p\in\mathsf{P}{X}$ and if $f:X\to Y$ is any map, then:

\begin{array}[]{l@{\quad}l@{\qquad}l@{\qquad}l@{\quad}l}\Bigl{(}{\textstyle\mathbin{\dot{{\bigvee}}}}\bigl{\{}\sigma_{x}:x\in f^{-1}(y)\bigr{\}}\Bigr{)}_{y\in Y}&({\in}~{}\Sigma^{Y})&\text{is a code for}&\exists{f}(p)&({\in}~{}\mathsf{P}{Y})\\[6.0pt] \Bigl{(}{\textstyle\mathbin{\dot{{\bigwedge}}}}\bigl{\{}\sigma_{x}:x\in f^{-1}(y)\bigr{\}}\Bigr{)}_{y\in Y}&({\in}~{}\Sigma^{Y})&\text{is a code for}&\forall{f}(p)&({\in}~{}\mathsf{P}{Y})\\ \end{array}

It now remains to characterize the ordering on each Heyting algebra $\mathsf{P}{X}$ from the above constructions in $\Sigma$ . For that, we consider the set $\Phi\subseteq\Sigma$ defined by $\Phi:=\{\xi\in\Sigma:\llbracket\xi\rrbracket_{\_\in 1}=\top_{1}\}$ , writing $\top_{1}$ the top element of $\mathsf{P}{1}$ . We check that:

Proposition 2.7.

For all $X\in\mathbf{Set}$ and $\sigma,\tau\in\Sigma^{X}$ , we have

\llbracket\sigma\rrbracket_{X}\leq\llbracket\tau\rrbracket_{X}\qquad\text{iff}\qquad{\textstyle\mathbin{\dot{{\bigwedge}}}}\{\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}:x\in X\}\in\Phi\,.

Proof.

Writing $1_{X}:X\to 1$ the unique map from $X$ to $1$ , we have:

∎

\begin{array}[b]{r@{\quad}c@{\quad}l}\llbracket\sigma\rrbracket_{X}\leq\llbracket\tau\rrbracket_{X}&\text{iff}&\top_{X}\leq\llbracket\sigma\rrbracket_{X}\to\llbracket\tau\rrbracket_{X}\\ &\text{iff}&\mathsf{P}{1_{X}}(\top_{1})\leq\llbracket\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}\rrbracket_{x\in X}\\ &\text{iff}&\top_{1}\leq\forall{1_{X}}\bigl{(}\llbracket\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}\rrbracket_{x\in X}\bigr{)}\\ &\text{iff}&\top_{1}\leq\bigl{\llbracket}\mathbin{\dot{{\bigwedge}}}\{\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}:x\in X\}\bigr{\rrbracket}_{\_\in 1}\\ &\text{iff}&\mathbin{\dot{{\bigwedge}}}\{\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x}:x\in X\}\in\Phi\\ \end{array}

So that we can complete the above correspondence between the operations on the Heyting algebra $\mathsf{P}{X}$ and the analogous operations on the set $\Sigma$ by concluding that:

•

If $\sigma,\tau\in\Sigma^{X}$ are codes for $p,q\in\mathsf{P}{X}$ , respectively, then:

p\leq q\quad({\in}~{}\mathsf{P}{X})\qquad\text{iff}\qquad\mathop{\mathbin{\dot{{\bigwedge}}}}\limits_{x\in X}(\sigma_{x}\mathbin{\dot{{\to}}}\tau_{x})~{}\in~{}\Phi\quad({\subseteq}~{}\Sigma)

Remark 2.8.

At this stage, it would be tempting to see the set $\Sigma$ as a complete Heyting algebra whose structure is given by the operations ${\mathbin{\dot{{\land}}}},{\mathbin{\dot{{\lor}}}},{\mathbin{\dot{{\to}}}},\mathbin{\dot{{\bigvee}}},\mathbin{\dot{{\bigwedge}}}$ , while seeing the subset $\Phi\subseteq\Sigma$ as a particular filter of $\Sigma$ . Alas, the above operations come with absolutely no algebraic property, since in general we have

\xi\mathbin{\dot{{\land}}}\xi\neq\xi,\qquad\xi\mathbin{\dot{{\land}}}\xi^{\prime}\neq\xi^{\prime}\mathbin{\dot{{\land}}}\xi,\qquad\xi\mathbin{\dot{{\to}}}\xi\neq\dot{\top},\qquad{\textstyle\mathbin{\dot{{\bigvee}}}}\{\xi\}\neq{\textstyle\mathbin{\dot{{\bigwedge}}}}\{\xi\}\neq\xi,\qquad\text{etc.}

So that in the end, these operations fail to endow the set $\Sigma$ with the structure of a (complete) Heyting algebra—although they are sufficient in practice to characterize the whole structure of the tripos $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ via the pseudo-filter $\Phi\subseteq\Sigma$ . However, we shall see in Section 3 that the set $\Sigma$ generates an implicative algebra $\mathscr{A}$ whose operations (arbitrary meets and implication) capture the whole structure of the tripos $\mathsf{P}$ in a more natural way.

2.5. Miscellaneous properties

In this section, we present some properties of the set $\Sigma$ that will be useful to construct the implicative algebra $\mathscr{A}$ .

Proposition 2.9 (Merging quantifications).

\begin{array}[]{r@{~{}~}c@{~{}~}l}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\bigl{\{}{\mathbin{\dot{{\bigvee}}}}s:s\in S\bigr{\}}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\bigl{(}{\bigcup}S\bigr{)}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}\\[3.0pt] \bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}{\mathbin{\dot{{\bigwedge}}}}s:s\in S\bigr{\}}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{(}{\bigcup}S\bigr{)}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}\\ \end{array}

Proof.

Let us consider:

•

The membership relation $E:=\{(\xi,s):\xi\in s\}\subseteq\Sigma\times\mathfrak{P}(\Sigma)$ equipped with the projections $e_{1}:E\to\Sigma$ and $e_{2}:E\to\mathfrak{P}(\Sigma)$ (see Section 2.3 above);
•

The membership relation $F:=\{(s,S):s\in S\}\subseteq\mathfrak{P}(\Sigma)\times\mathfrak{P}(\mathfrak{P}(\Sigma))$ equipped with the projections $f_{1}:F\to\mathfrak{P}(\Sigma)$ and $f_{2}:F\to\mathfrak{P}(\mathfrak{P}(\Sigma))$ ;
•

The composed membership relation $G:=\{(\xi,s,S):\xi\in s\in S\}\subseteq\Sigma\times\mathfrak{P}(\Sigma)\times\mathfrak{P}(\mathfrak{P}(\Sigma))$ equipped with the functions $g_{1}:G\to E$ and $g_{2}:G\to F$ defined by $g_{1}(\xi,s,S)=(\xi,s)$ and $g_{2}(\xi,s,S)=(s,S)$ for all $(\xi,s,S)\in G$ .

By construction, we have the following pullback:

hence $\mathsf{P}{f_{1}}\circ\exists{e_{2}}=\exists{g_{2}}\circ\mathsf{P}{g_{1}}$ and $\mathsf{P}{f_{1}}\circ\forall{e_{2}}=\forall{g_{2}}\circ\mathsf{P}{g_{1}}$ (Beck-Chevalley). Therefore:

\begin{array}[b]{@{}r@{~{}~}c@{~{}~}l@{\hskip-10pt}}\bigl{\llbracket}\mathbin{\dot{{\bigvee}}}\bigl{\{}{\mathbin{\dot{{\bigvee}}}}s:s\in S\}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}~{}{}&=\hfil~{}{}&\bigl{\llbracket}\mathbin{\dot{{\bigvee}}}\bigl{\{}{\mathbin{\dot{{\bigvee}}}}f_{1}(z):z\in f_{2}^{-1}(S)\bigr{\}}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}~{}=~{}\exists{f_{2}}\bigl{(}\llbracket\mathbin{\dot{{\bigvee}}}\circ f_{1}\rrbracket_{F}\bigr{)}\hfil\hskip-10.\\ ~{}{}&=\hfil~{}{}&(\exists{f_{2}}\circ\mathsf{P}{f_{1}})\bigl{(}\llbracket\mathbin{\dot{{\bigvee}}}\rrbracket_{\mathfrak{P}(\Sigma)}\bigr{)}~{}=~{}(\exists{f_{2}}\circ\mathsf{P}{f_{1}}\circ\exists{e_{2}})\bigl{(}\llbracket e_{1}\rrbracket_{E}\bigr{)}\hfil\hskip-10.\\ ~{}{}&=\hfil~{}{}&(\exists{f_{2}}\circ\exists{g_{2}}\circ\mathsf{P}{g_{1}})\bigl{(}\llbracket e_{1}\rrbracket_{E}\bigr{)}~{}=~{}\exists(f_{2}\circ g_{2})\bigl{(}\llbracket e_{1}\circ g_{1}\rrbracket_{G}\bigr{)}\hfil\hskip-10.\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}\mathbin{\dot{{\bigvee}}}\{(e_{1}\circ g_{1})(z):z\in(f_{2}\circ g_{2})^{-1}(S)\}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}\hfil\hskip-10.\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\bigl{(}\bigcup{S}\bigr{)}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}\hfil\hskip-10.\\ \end{array}

And similarly for $\forall$ . ∎

The following proposition expresses that the codes for universal quantification and implication fulfill the usual property of distributivity (on the right-hand side of implication):

Proposition 2.10.

We have: $\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\{\theta\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in s\}\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}~{}=~{}\bigl{\llbracket}\theta\mathbin{\dot{{\to}}}{\mathbin{\dot{{\bigwedge}}}}s\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}$ .

Proof.

Let us consider the set $G:=\{(\theta,\xi,s):\xi\in s\}\subseteq\Sigma\times\Sigma\times\mathfrak{P}(\Sigma)$ with the corresponding projections $g_{1},g_{2}:G\to\Sigma$ and $g_{3}:G\to\mathfrak{P}(\Sigma)$ . We also write $\pi:\Sigma\times\mathfrak{P}(\Sigma)\to\Sigma$ the first projection from $\Sigma\times\mathfrak{P}(\Sigma)$ to $\Sigma$ . For all $p\in\mathsf{P}(\Sigma\times\mathfrak{P}(\Sigma))$ , we observe that:

\begin{array}[b]{l@{\quad}l}&p~{}\leq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\{\theta\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in s\}\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\\ \text{iff}&p~{}\leq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}g_{1}(z)\mathbin{\dot{{\to}}}g_{2}(z)~{}:~{}z\in\langle g_{1},g_{3}\rangle^{-1}(\theta,s)\bigr{\}}\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\\ \text{iff}&p~{}\leq~{}\forall\langle g_{1},g_{3}\rangle\bigl{(}\llbracket g_{1}\rrbracket_{G}\to\llbracket g_{2}\rrbracket_{G}\bigr{)}\\ \text{iff}&\mathsf{P}\langle g_{1},g_{3}\rangle(p)~{}\leq~{}\llbracket g_{1}\rrbracket_{G}\to\llbracket g_{2}\rrbracket_{G}\\ \text{iff}&\mathsf{P}\langle g_{1},g_{3}\rangle(p)\land\llbracket g_{1}\rrbracket_{G}~{}\leq~{}\llbracket g_{2}\rrbracket_{G}\\ \text{iff}&\mathsf{P}\langle g_{1},g_{3}\rangle(p)\land\llbracket\pi\circ\langle g_{1},g_{3}\rangle\rrbracket_{G}~{}\leq~{}\llbracket g_{2}\rrbracket_{G}\\ \text{iff}&\mathsf{P}\langle g_{1},g_{3}\rangle\bigl{(}p\land\llbracket\pi\rrbracket_{\Sigma\times\mathfrak{P}(\Sigma)}\bigr{)}~{}\leq~{}\llbracket g_{2}\rrbracket_{G}\\ \text{iff}&p\land\llbracket\pi\rrbracket_{\Sigma\times\mathfrak{P}(\Sigma)}~{}\leq~{}\forall\langle g_{1},g_{3}\rangle(\llbracket g_{2}\rrbracket_{G})\\ \text{iff}&p~{}\leq~{}\llbracket\pi\rrbracket_{\Sigma\times\mathfrak{P}(\Sigma)}\to\forall\langle g_{1},g_{3}\rangle(\llbracket g_{2}\rrbracket_{G})\\ \text{iff}&p~{}\leq~{}\llbracket\theta\rrbracket_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\to\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}g_{2}(z)~{}:~{}z\in\langle g_{1},g_{3}\rangle^{-1}(\theta,s)\bigr{\}}\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\\ \text{iff}&p~{}\leq~{}\llbracket\theta\rrbracket_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\to\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}\xi~{}:~{}\xi\in s\bigr{\}}\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\\ \text{iff}&p~{}\leq~{}\bigl{\llbracket}\theta\mathbin{\dot{{\to}}}{\mathbin{\dot{{\bigwedge}}}}s\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\\ \end{array}

From which we get the desired equality. ∎

Corollary 2.11.

Given a set $X$ and two families $\sigma\in\Sigma^{X}$ and $t\in\mathfrak{P}(\Sigma)^{X}$ , we have:

\textstyle\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\{\sigma_{x}\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in t_{x}\}\bigr{\rrbracket}_{x\in X}~{}=~{}\bigl{\llbracket}\sigma_{x}\mathbin{\dot{{\to}}}{\mathbin{\dot{{\bigwedge}}}}t_{x}\bigr{\rrbracket}_{x\in X}

Proof.

Indeed, we have

\begin{array}[b]{r@{~{}~}c@{~{}~}l}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\{\sigma_{x}\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in t_{x}\}\bigr{\rrbracket}_{x\in X}~{}{}&=\hfil~{}{}&\mathsf{P}(\langle\sigma,t\rangle)\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\{\theta\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in s\}\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\bigr{)}\\ ~{}{}&=\hfil~{}{}&\mathsf{P}(\langle\sigma,t\rangle)\bigl{(}\bigl{\llbracket}\theta\mathbin{\dot{{\to}}}{\mathbin{\dot{{\bigwedge}}}}s\bigr{\rrbracket}_{(\theta,s)\in\Sigma\times\mathfrak{P}(\Sigma)}\bigr{)}\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}\sigma_{x}\mathbin{\dot{{\to}}}{\mathbin{\dot{{\bigwedge}}}}t_{x}\bigr{\rrbracket}_{x\in X}\\ \end{array}\begin{tabular}[b]{r@{}}(by Prop.~{}\ref{p:DistrForallImp})\\ \mbox{\qed}\\ \end{tabular}

From now on, we consider the inclusion relation $F:=\{(s,s^{\prime}):s\subseteq s^{\prime}\}\subseteq\mathfrak{P}(\Sigma)\times\mathfrak{P}(\Sigma)$ together with the corresponding projections $f_{1}:F\to\mathfrak{P}(\Sigma)$ and $f_{2}:F\to\mathfrak{P}(\Sigma)$ . The following proposition expresses that the operators ${\mathbin{\dot{{\bigvee}}}}:\mathfrak{P}(\Sigma)\to\Sigma$ and ${\mathbin{\dot{{\bigwedge}}}}:\mathfrak{P}(\Sigma)\to\Sigma$ are respectively monotonic and antitonic w.r.t. the domain of quantification:

Proposition 2.12.

$\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}\leq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{2}\bigr{\rrbracket}_{F}$ and $\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}\geq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{2}\bigr{\rrbracket}_{F}$ .

Proof.

Let us consider the set $G:=\{(\xi,\xi^{\prime},(s,s^{\prime})):\xi\in s,~{}\xi^{\prime}\in s^{\prime},~{}(s,s^{\prime})\in F\}\subseteq\Sigma\times\Sigma\times F$ equipped with the three projections $g_{1},g_{2}:G\to\Sigma$ and $g_{3}:G\to F$ . We have

\begin{array}[]{r@{~{}~}c@{~{}~}l}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\bigl{\{}g_{1}(z):z\in g_{3}^{-1}(s,s^{\prime})\bigr{\}}\bigr{\rrbracket}_{(s,s^{\prime})\in F}~{}=~{}\exists{g_{3}}(\llbracket g_{1}\rrbracket_{G})\\ \bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{2}\bigr{\rrbracket}_{F}~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\bigl{\{}g_{2}(z):z\in g_{3}^{-1}(s,s^{\prime})\bigr{\}}\bigr{\rrbracket}_{(s,s^{\prime})\in F}~{}=~{}\exists{g_{3}}(\llbracket g_{2}\rrbracket_{G})\\ \bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}g_{1}(z):z\in g_{3}^{-1}(s,s^{\prime})\bigr{\}}\bigr{\rrbracket}_{(s,s^{\prime})\in F}~{}=~{}\forall{g_{3}}(\llbracket g_{1}\rrbracket_{G})\\ \bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}g_{2}(z):z\in g_{3}^{-1}(s,s^{\prime})\bigr{\}}\bigr{\rrbracket}_{(s,s^{\prime})\in F}~{}=~{}\forall{g_{3}}(\llbracket g_{2}\rrbracket_{G})\\ \end{array}

Let us now consider the function $g:G\to G$ defined by $g(\xi,\xi^{\prime},(s,s^{\prime}))=(\xi,\xi,(s,s^{\prime}))$ for all $(\xi,\xi^{\prime},(s,s^{\prime}))\in G$ . Since $g_{2}\circ g=g_{1}$ , we have $\mathsf{P}{g}(\llbracket g_{2}\rrbracket_{G})=\llbracket g_{2}\circ g\rrbracket_{G}=\llbracket g_{1}\rrbracket_{G}$ and thus

(by left/right adjunction)

\exists{g}(\llbracket g_{1}\rrbracket_{G})~{}\leq~{}\llbracket g_{2}\rrbracket_{G}~{}\leq~{}\forall{g}(\llbracket g_{1}\rrbracket_{G})

Combining the above inequalities with the fact that $g_{3}\circ g=g_{3}$ , we deduce that:

∎

\begin{array}[b]{l}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}=~{}\exists{g_{3}}(\llbracket g_{1}\rrbracket_{G})~{}=~{}\exists{g_{3}}(\exists{g}(\llbracket g_{1}\rrbracket_{G}))~{}\leq~{}\exists{g_{3}}(\llbracket g_{2}\rrbracket_{G})~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{2}\bigr{\rrbracket}_{F}\\ \bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{1}\bigr{\rrbracket}_{F}~{}=~{}\forall{g_{3}}(\llbracket g_{1}\rrbracket_{G})~{}=~{}\forall{g_{3}}(\forall{g}(\llbracket g_{1}\rrbracket_{G}))~{}\geq~{}\forall{g_{3}}(\llbracket g_{2}\rrbracket_{G})~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{2}\bigr{\rrbracket}_{F}\,.\\ \end{array}

Corollary 2.13.

Given a set $X$ and two families $a,b\in\mathfrak{P}(\Sigma)^{X}$ such that $a_{x}\subseteq b_{x}$ for all $x\in X$ , we have: $\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ a\bigr{\rrbracket}_{X}~{}\leq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ b\bigr{\rrbracket}_{X}$ and $\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ a\bigr{\rrbracket}_{X}~{}\geq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ b\bigr{\rrbracket}_{X}$ .

Proof.

Let $c:=(a_{x},b_{x})_{x\in X}\in F^{X}$ . From Prop. 2.12 we get:

∎

\begin{array}[b]{@{}l@{}}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ a\bigr{\rrbracket}_{X}=\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{1}\circ c\bigr{\rrbracket}_{X}=\mathsf{P}{c}\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{1}\bigr{\rrbracket}\bigr{)}\leq\mathsf{P}{c}\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{2}\bigr{\rrbracket}\bigr{)}=\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ f_{2}\circ c\bigr{\rrbracket}_{X}=\bigl{\llbracket}{\mathbin{\dot{{\bigvee}}}}\circ b\bigr{\rrbracket}_{X}\\ \bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ a\bigr{\rrbracket}_{X}=\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{1}\circ c\bigr{\rrbracket}_{X}=\mathsf{P}{c}\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{1}\bigr{\rrbracket}\bigr{)}\geq\mathsf{P}{c}\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{2}\bigr{\rrbracket}\bigr{)}=\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ f_{2}\circ c\bigr{\rrbracket}_{X}=\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ b\bigr{\rrbracket}_{X}\\ \end{array}

3. Extracting the implicative algebra

In Section 2.4, we have seen that the structure of the tripos $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ can be fully characterized from the binary operations $({\mathbin{\dot{{\land}}}}),({\mathbin{\dot{{\lor}}}}),({\mathbin{\dot{{\to}}}}):\Sigma\times\Sigma\to\Sigma$ and the infinitary operations $({\mathbin{\dot{{\bigvee}}}}),({\mathbin{\dot{{\bigwedge}}}}):\mathfrak{P}(\Sigma)\to\Sigma$ via some subset $\Phi\subseteq\Sigma$ (the ‘pseudo-filter’). However, these operations fail to endow the set $\Sigma$ itself with the structure of a complete Heyting algebra, for they lack the most basic algebraic properties that are required by such a structure.

In this section, we shall construct a particular implicative structure $\mathscr{A}=(\mathscr{A},{\preccurlyeq},{\to})$ from the set $\Sigma$ equipped with the only operations $({\mathbin{\dot{{\to}}}}):\Sigma\times\Sigma\to\Sigma$ and $({\mathbin{\dot{{\bigwedge}}}}):\mathfrak{P}(\Sigma)\to\Sigma$ , using a construction that is reminiscent from the construction of graph models [1]. As we shall see, the main interest of such a construction is that:

(1)

The carrier set $\mathscr{A}$ can be used as an alternative set of propositions, for it possesses its own generic predicate $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ .
(2)

The two operations $({\to}):\mathscr{A}\times\mathscr{A}\to\mathscr{A}$ and $({\bigcurlywedge}):\mathfrak{P}(\mathscr{A})\to\mathscr{A}$ that naturally come with the implicative structure $\mathscr{A}$ constitute codes (in the sense of the new generic predicate $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ ) for implication and universal quantification in the tripos $\mathsf{P}$ .
(3)

The ordering on each Heyting algebra $\mathsf{P}{X}$ (for $X\in\mathbf{Set}$ ) can be characterized from the above two operations via a particular separator $S\subseteq\mathscr{A}$ .

From the above properties, we shall easily conclude that the tripos $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ is isomorphic to the tripos induced by the implicative algebra $(\mathscr{A},{\preccurlyeq},{\to},S)$ .

3.1. Defining the set $\mathscr{A}_{0}$ of atoms

The construction of the implicative structure $\mathscr{A}$ is achieved in two steps. First we construct from the set $\Sigma$ of propositions a (larger) set $\mathscr{A}_{0}$ of atoms equipped with a preorder $\leq$ . Then we let $\mathscr{A}:=\mathfrak{P}_{\uparrow}(\mathscr{A}_{0})$ , where $\mathfrak{P}_{\uparrow}(\mathscr{A}_{0})$ denotes the set of all upwards closed subsets of $\mathscr{A}_{0}$ w.r.t. the preorder $\leq$ . Formally, the set $\mathscr{A}_{0}$ of atoms is inductively defined from the following two clauses:

(1)

If $\xi\in\Sigma$ , then $\dot{\xi}\in\mathscr{A}_{0}$ ²²2Here, we use the dot notation $\dot{\xi}$ only to distinguish the code $\xi\in\Sigma$ from its image $\dot{\xi}\in\mathscr{A}_{0}$ . (base case).
(2)

If $s\in\mathfrak{P}(\Sigma)$ and $\alpha\in\mathscr{A}_{0}$ , then $(s\mapsto\alpha)\in\mathscr{A}_{0}$ (inductive case).

In other words, each atom $\alpha\in\mathscr{A}_{0}$ is a finite list of subsets of $\Sigma$ terminated by an element of $\Sigma$ , that is: $\alpha=s_{1}\mapsto\cdots\mapsto s_{n}\mapsto\dot{\xi}$ for some $s_{1},\ldots,s_{n}\in\mathfrak{P}(\Sigma)$ and $\xi\in\Sigma$ . The set $\mathscr{A}_{0}$ is equipped with the binary relation $\alpha\leq\beta$ that is inductively defined from the two rules

\dot{\xi}\leq\dot{\xi}\qquad\qquad s\mapsto\alpha~{}\leq~{}s^{\prime}\mapsto\alpha^{\prime}\lx@proof@logical@and s\subseteq s^{\prime}\quad\alpha\leq\alpha^{\prime}

Fact 3.1.

The relation $\alpha\leq\beta$ is a preorder on $\mathscr{A}_{0}$ .

Proof.

By induction on $\alpha\in\mathscr{A}_{0}$ , we successively prove (1) that $\alpha\leq\alpha$ and (2) that $\alpha\leq\beta$ and $\beta\leq\gamma$ together imply that $\alpha\leq\gamma$ , for all $\beta,\gamma\in\mathscr{A}_{0}$ . ∎

Finally, the set $\mathscr{A}_{0}$ is equipped with a conversion function $\varphi_{0}:\mathscr{A}_{0}\to\Sigma$ that is defined by

\varphi_{0}(\dot{\xi})~{}:=~{}\xi\qquad\text{and}\qquad\varphi_{0}(s\mapsto\alpha)~{}:=~{}\bigl{(}{\textstyle\mathbin{\dot{{\bigwedge}}}{s}}\bigr{)}\mathbin{\dot{{\to}}}\varphi_{0}(\alpha)

(Note that by construction, this function is surjective.)

Remark 3.2 (Relationship with graph models).

In the theory of graph models [1], the set of atoms $\mathscr{A}_{0}$ would be naturally defined from the grammar

(ξ \in Σ)

\alpha,\beta\in\mathscr{A}_{0}\quad::=\quad\dot{\xi}\quad|\quad\{\alpha_{1},\ldots,\alpha_{n}\}\mapsto\beta

that is, as the least solution of the set-theoretic equation $\mathscr{A}_{0}=\Sigma+\mathfrak{P}_{\text{fin}}(\mathscr{A}_{0})\times\mathscr{A}_{0}$ . However, such a construction would yield an applicative structure upon the set $\mathscr{A}=\mathfrak{P}_{\uparrow}(\mathscr{A}_{0})$ —it would even constitute a ( $D_{\infty}$ -like) model of the $\lambda$ -calculus—, but it would not yield an implicative structure, for the restriction to the finite subsets of $\mathscr{A}_{0}$ in the left-hand side of the construction $\{a_{1},\ldots,\alpha_{n}\}\mapsto\beta$ actually prevents defining an implication with the desired properties.

To fix this problem, it would be natural to relax the condition of finiteness, by considering instead the equation $\mathscr{A}_{0}=\Sigma+\mathfrak{P}(\mathscr{A}_{0})\times\mathscr{A}_{0}$ . Alas, such an equation has no solution (for obvious cardinality reasons), so that the trick consists to replace arbitrary subsets of $\mathscr{A}_{0}$ (in the left-hand side of the construction $s\mapsto\beta$ ) by arbitrary subsets of $\Sigma$ , using the fact that the subsets of $\mathscr{A}_{0}$ can always be converted (element-wise) into subsets of $\Sigma$ , via the conversion function $\varphi_{0}:\mathscr{A}_{0}\to\Sigma$ . So that in the end, we obtain the set-theoretic equation $\mathscr{A}_{0}=\Sigma+\mathfrak{P}(\Sigma)\times\mathscr{A}_{0}$ , whose least solution is precisely the set $\mathscr{A}_{0}$ we defined above.

3.2. Defining the implicative structure $(\mathscr{A},{\preccurlyeq},{\to})$

Let $\mathscr{A}:=\mathfrak{P}_{\uparrow}(\mathscr{A}_{0})$ be the set of upwards closed subsets of $\mathscr{A}_{0}$ (w.r.t. the preorder $\leq$ on $\mathscr{A}_{0}$ ), equipped with the ordering $a\preccurlyeq b$ defined by $a\preccurlyeq b$ iff $a\supseteq b$ (reverse inclusion) for all $a,b\in\mathscr{A}$ . It is clear that:

Proposition 3.3.

The poset $(\mathscr{A},{\preccurlyeq})=(\mathfrak{P}_{\uparrow}(\mathscr{A}_{0}),{\supseteq})$ is a complete lattice.

Note that in this complete lattice, (finitary or infinitary) meets and joins are respectively given by unions and intersections. In particular, we have $\bot_{\mathscr{A}}=\mathscr{A}$ and $\top_{\mathscr{A}}=\varnothing$ .

Let $\tilde{\varphi}_{0}:\mathscr{A}\to\mathfrak{P}(\Sigma)$ be the function defined by $\tilde{\varphi}_{0}(a)=\{\varphi_{0}(\alpha):\alpha\in a\}$ for all $a\in\mathscr{A}$ . For each set of codes $s\in\mathfrak{P}(\Sigma)$ , we write $s^{\subseteq}:=\{s^{\prime}\in\mathfrak{P}(\Sigma):s\subseteq s^{\prime}\}$ . We now equip the complete lattice $(\mathscr{A},{\preccurlyeq})$ with the implication defined by

(for all ​ a, b \in 𝒜)

a\to b~{}:=~{}\bigl{\{}s\mapsto\beta~{}:~{}s\in\tilde{\varphi}_{0}(a)^{\subseteq},~{}\beta\in b\bigr{\}}

Note that by construction, we have $(a\to b)\in\mathscr{A}~{}({=}~{}\mathfrak{P}_{\uparrow}(\mathscr{A}_{0}))$ for all $a,b\in\mathscr{A}$ .

Proposition 3.4.

The triple $(\mathscr{A},{\preccurlyeq},{\to})$ is an implicative structure.

Proof.

Variance of implication. Let $a,a^{\prime},b,b^{\prime}\in\mathscr{A}$ such that $a^{\prime}\preccurlyeq a$ and $b\preccurlyeq b$ , that is: $a\subseteq a^{\prime}$ and $b^{\prime}\subseteq b$ . We observe that

\begin{array}[]{r@{~{}~}c@{~{}~}l}a^{\prime}\to b^{\prime}~{}{}&=\hfil~{}{}&\bigl{\{}s\mapsto\beta~{}:~{}s\in\tilde{\varphi}_{0}(a^{\prime})^{\subseteq},~{}\beta\in b^{\prime}\bigr{\}}\\ ~{}{}&\subseteq\hfil~{}{}&\bigl{\{}s\mapsto\beta~{}:~{}s\in\tilde{\varphi}_{0}(a)^{\subseteq},~{}\beta\in b\bigr{\}}~{}=~{}a\to b\\ \end{array}

(since $\tilde{\varphi}_{0}(a)\subseteq\tilde{\varphi}_{0}(a^{\prime})$ and $b^{\prime}\subseteq b$ ), which means that $(a\to b)\preccurlyeq(a^{\prime}\to b^{\prime})$ .

Distributivity of meets w.r.t. $\to$ . Given $a\in\mathscr{A}$ and $B\subseteq\mathscr{A}$ , we observe that

∎

\begin{array}[b]{r@{~{}~}c@{~{}~}l}a\to\bigcurlywedge\!B~{}{}&=\hfil~{}{}&\displaystyle\bigl{\{}s\mapsto\beta~{}:~{}s\in\tilde{\varphi}_{0}(a)^{\subseteq},~{}\beta\in{\textstyle\bigcup}B\bigr{\}}\\[6.0pt] ~{}{}&=\hfil~{}{}&\displaystyle\bigcup_{b\in B}\bigl{\{}s\mapsto\beta~{}:~{}s\in\tilde{\varphi}_{0}(a)^{\subseteq},~{}\beta\in b\bigr{\}}~{}=~{}\bigcurlywedge_{\!\!b\in B\!\!}(a\to b)\\ \end{array}

3.3. Viewing $\mathscr{A}$ as a new set of propositions

Let us now consider the two conversion functions $\varphi:\mathscr{A}\to\Sigma$ and $\psi:\Sigma\to\mathscr{A}$ defined by

\begin{array}[]{r@{~{}~}c@{~{}~}l}\varphi(a)~{}{}&:=\hfil~{}{}&\mathbin{\dot{{\bigwedge}}}\tilde{\varphi}_{0}(a)~{}=~{}\mathbin{\dot{{\bigwedge}}}\{\varphi_{0}(\alpha):\alpha\in a\}\\[3.0pt] \psi(\xi)~{}{}&:=\hfil~{}{}&\{\dot{\xi}\}\\ \end{array}\begin{array}[]{r@{}}(\text{for all}~{}a\in\mathscr{A})\\[3.0pt] (\text{for all}~{}\xi\in\Sigma)\\ \end{array}

as well as the predicate $\textit{tr}_{\mathscr{A}}:=\mathsf{P}\varphi(\textit{tr}_{\Sigma})~{}({=}~{}\llbracket\varphi\rrbracket_{\mathscr{A}})\in\mathsf{P}\mathscr{A}$ . We easily check that:

Lemma 3.5.

$\mathsf{P}\psi(\textit{tr}_{\mathscr{A}})=\textit{tr}_{\Sigma}$ .

Proof.

Since $\varphi(\psi(\xi))={\mathbin{\dot{{\bigwedge}}}}\{\xi\}$ for all $\xi\in\Sigma$ , we have:

∎

\begin{array}[b]{r@{~{}~}c@{~{}~}l}\mathsf{P}\psi(\textit{tr}_{\mathscr{A}})~{}{}&=\hfil~{}{}&\mathsf{P}\psi(\llbracket\varphi\rrbracket_{\mathscr{A}})~{}=~{}\llbracket\varphi\circ\psi\rrbracket_{\Sigma}~{}=~{}\bigl{\llbracket}\mathbin{\dot{{\bigwedge}}}\{\xi\}\bigr{\rrbracket}_{\xi\in\Sigma}~{}=~{}\bigl{\llbracket}\mathbin{\dot{{\bigwedge}}}\bigl{\{}\mathrm{id}(\xi^{\prime}):\xi^{\prime}\in\mathrm{id}^{-1}(\xi)\bigr{\}}\bigr{\rrbracket}_{\xi\in\Sigma}\\ ~{}{}&=\hfil~{}{}&\forall\mathrm{id}_{\Sigma}\bigl{(}\llbracket\mathrm{id}_{\Sigma}\rrbracket_{\Sigma}\bigr{)}~{}=~{}\llbracket\mathrm{id}_{\Sigma}\rrbracket_{\Sigma}~{}=~{}\mathsf{P}\mathrm{id}_{\Sigma}(\textit{tr}_{\Sigma})~{}=~{}\textit{tr}_{\Sigma}\,.\end{array}

Therefore:

Proposition 3.6.

The predicate $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ is a generic predicate for the tripos $\mathsf{P}$ .

Proof.

For each set $X$ , we want to show that the function $\langle\mskip-4.0mu\langle\_\rangle\mskip-4.0mu\rangle_{X}:\mathscr{A}^{X}\to\mathsf{P}{X}$ defined by $\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X}=\mathsf{P}{a}(\textit{tr}_{\mathscr{A}})$ for all $a\in\mathscr{A}^{X}$ is surjective. For that, we take $p\in\mathsf{P}{X}$ and pick a code $\sigma\in\Sigma^{X}$ such that $p=\llbracket\sigma\rrbracket_{X}=\mathsf{P}\sigma(\textit{tr}_{\Sigma})$ . From the above lemma, we get:

p~{}=~{}\mathsf{P}{\sigma}(\textit{tr}_{\Sigma})~{}=~{}\mathsf{P}{\sigma}(\mathsf{P}\psi(\textit{tr}_{\mathscr{A}}))~{}=~{}\mathsf{P}(\psi\circ\sigma)(\textit{tr}_{\mathscr{A}})~{}=~{}\langle\mskip-4.0mu\langle\psi\circ\sigma\rangle\mskip-4.0mu\rangle_{X}

hence $a:=\psi\circ\sigma\in\mathscr{A}^{X}$ is a code for $p$ in the sense of the predicate $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ . ∎

To sum up, we now have two sets of propositions $\Sigma$ and $\mathscr{A}$ , two generic predicates $\textit{tr}_{\Sigma}\in\mathsf{P}\Sigma$ and $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ , as well as two decoding functions $\llbracket\_\rrbracket_{X}:\Sigma^{X}\to\mathsf{P}{X}$ and $\langle\mskip-4.0mu\langle\_\rangle\mskip-4.0mu\rangle_{X}:\mathscr{A}^{X}\to\mathsf{P}{X}$ . As usual, we write $\varphi^{X}:\mathscr{A}^{X}\to\Sigma^{X}$ and $\psi^{X}:\Sigma^{X}\to\mathscr{A}^{X}$ (for $X\in\mathbf{Set}$ ) the natural transformations induced by the two maps $\varphi:\mathscr{A}\to\Sigma$ and $\psi:\Sigma\to\mathscr{A}$ . We easily check that:

Proposition 3.7.

For each set $X$ , the following two diagrams commute:

Proof.

For all $a\in\mathscr{A}^{X}$ , we have $\llbracket\varphi^{X}(a)\rrbracket_{X}=\llbracket\varphi\circ a\rrbracket_{X}=\mathsf{P}{a}(\mathsf{P}\varphi(\textit{tr}_{\Sigma}))=\mathsf{P}{a}(\textit{tr}_{\mathscr{A}})=\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X}$ .
And for all $\sigma\in\Sigma^{X}$ , we have $\langle\mskip-4.0mu\langle\psi^{X}(\sigma)\rangle\mskip-4.0mu\rangle_{X}=\langle\mskip-4.0mu\langle\psi\circ\sigma\rangle\mskip-4.0mu\rangle=\mathsf{P}{\sigma}(\mathsf{P}\psi(\textit{tr}_{\mathscr{A}}))=\mathsf{P}{\sigma}(\textit{tr}_{\Sigma})=\llbracket\sigma\rrbracket_{X}$ . ∎

3.4. Universal quantification in $\mathscr{A}$

By analogy with the construction performed in Section 2.3, we now consider the membership relation $E^{\prime}:=\{(a,A):a\in A\}\subseteq\mathscr{A}\times\mathfrak{P}(\mathscr{A})$ together with the corresponding projections $e^{\prime}_{1}:E^{\prime}\to\mathscr{A}$ and $e^{\prime}_{2}:E^{\prime}\to\mathfrak{P}(\mathscr{A})$ .

The following proposition states that the operator $({\bigcurlywedge}):\mathfrak{P}(\mathscr{A})\to\mathscr{A}$ is a code for universal quantification in the sense of the generic predicate $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ :

Proposition 3.8.

$\bigl{\langle}\mskip-4.0mu\bigl{\langle}{\bigcurlywedge}A\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{A\in\mathfrak{P}(\mathscr{A})}=\forall{e^{\prime}_{2}}\bigl{(}\langle\mskip-4.0mu\langle e^{\prime}_{1}\rangle\mskip-4.0mu\rangle_{E^{\prime}}\bigr{)}$ .

Proof.

Indeed, we have:

\begin{array}[b]{r@{~{}~}c@{~{}~}l@{\hskip-5mm}}\bigl{\langle}\mskip-4.0mu\bigl{\langle}{\bigcurlywedge}A\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{A\in\mathfrak{P}(\mathscr{A})}~{}{}&=\hfil~{}{}&\bigl{\langle}\mskip-4.0mu\bigl{\langle}{\bigcup}A\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{A\in\mathfrak{P}(\mathscr{A})}~{}=~{}\bigl{\llbracket}\varphi\bigl{(}{\bigcup}A\bigr{)}\bigr{\rrbracket}_{A\in\mathfrak{P}(\mathscr{A})}~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\tilde{\varphi}_{0}\bigl{(}{\bigcup}A\bigr{)}\bigr{\rrbracket}_{A\in\mathfrak{P}(\mathscr{A})}\hfil\hskip-14.22636pt\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}{\bigcup}\mathfrak{P}\tilde{\varphi}_{0}(A)\bigr{\rrbracket}_{A\in\mathfrak{P}(\mathscr{A})}~{}=~{}\mathsf{P}(\mathfrak{P}\tilde{\varphi}_{0})\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}{\bigcup}S\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}\bigr{)}\hfil\hskip-14.22636pt\\ ~{}{}&=\hfil~{}{}&\mathsf{P}(\mathfrak{P}\tilde{\varphi}_{0})\bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}{\mathbin{\dot{{\bigwedge}}}}s:s\in S\bigr{\}}\bigr{\rrbracket}_{S\in\mathfrak{P}(\mathfrak{P}(\Sigma))}\bigr{)}\hfil\hskip-14.22636pt\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}{\mathbin{\dot{{\bigwedge}}}}\tilde{\varphi}_{0}(a):a\in A\bigr{\}}\bigr{\rrbracket}_{A\in\mathfrak{P}(\mathscr{A})}~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}\varphi(a):a\in A\bigr{\}}\bigr{\rrbracket}_{A\in\mathfrak{P}(\mathscr{A})}\hfil\hskip-14.22636pt\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\bigl{\{}\varphi(e^{\prime}_{1}(p)):p\in{e^{\prime}}_{2}^{-1}(A)\}\bigr{\rrbracket}_{A\in\mathfrak{P}(\mathscr{A})}\hfil\hskip-14.22636pt\\ ~{}{}&=\hfil~{}{}&\forall{e^{\prime}_{2}}\bigl{(}\llbracket\varphi\circ e^{\prime}_{1}\rrbracket_{E^{\prime}}\bigr{)}~{}=~{}\forall{e^{\prime}_{2}}\bigl{(}\langle\mskip-4.0mu\langle e^{\prime}_{1}\rangle\mskip-4.0mu\rangle_{E^{\prime}}\bigr{)}\,.\hfil\hskip-14.22636pt\\ \end{array}\begin{tabular}[b]{r@{}}(by Prop.~{}\ref{p:MergeQuantSigma})\\ \\ \\ \mbox{\qed}\\ \end{tabular}

From the above result, we deduce that:

Proposition 3.9.

Given a code $a\in\mathscr{A}^{X}$ and a map $f:X\to Y$ , we have:

(\in 𝖯 ​ Y)

\textstyle\bigl{\langle}\mskip-4.0mu\bigl{\langle}\bigcurlywedge\{a_{x}:x\in f^{-1}(y)\}\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{y\in Y}~{}=~{}\forall{f}(\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X})

Proof.

Same argument as for Prop. 2.6 p. 2.6. ∎

3.5. Implication in $\mathscr{A}$

It now remains to show that the operation $({\to}):\mathscr{A}\times\mathscr{A}\to\mathscr{A}$ is a code for implication in the sense of the generic predicate $\textit{tr}_{\mathscr{A}}\in\mathsf{P}\mathscr{A}$ . For that, we first need to prove the following technical lemma:

Lemma 3.10.

$\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s^{\prime}\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}s^{\prime}\in s^{\subseteq},~{}\xi\in t\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}=\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in t\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}$ .

Proof.

Let us consider the set $G:=\{(s,t,s^{\prime},\xi):s^{\prime}\supseteq s,~{}\xi\in t\}\subseteq\mathfrak{P}(\Sigma)\times\mathfrak{P}(\Sigma)\times\mathfrak{P}(\Sigma)\times\Sigma$ equipped with the four projections $g_{1},g_{2},g_{3}:G\to\mathfrak{P}(\Sigma)$ , $g_{4}:G\to\Sigma$ and the function $g:G\to G$ defined by $g(s,t,s^{\prime},\xi)=g(s,t,s,\xi)$ for all $(s,t,s^{\prime},\xi)\in G$ . We observe that

\begin{array}[]{l@{~{}~}l}\hfil~{}{}&\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s^{\prime}\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}s^{\prime}\in s^{\subseteq},~{}\xi\in t\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\\ =\hfil~{}{}&\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}g_{3}(z)\bigr{)}\mathbin{\dot{{\to}}}g_{4}(z)~{}:~{}z\in\langle g_{1},g_{2}\rangle^{-1}(s,t)\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\\ =\hfil~{}{}&\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}\\ \end{array}

whereas

\begin{array}[]{l@{~{}~}l}\hfil~{}{}&\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in t\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\\ =\hfil~{}{}&\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}g_{1}(z)\bigr{)}\mathbin{\dot{{\to}}}g_{4}(z)~{}:~{}z\in\langle g_{1},g_{2}\rangle^{-1}(s,t)\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\\ =\hfil~{}{}&\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}\\ \end{array}

So that we have to prove that $\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}~{}=~{}\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}$ .

$({\leq})$ We observe that

\textstyle\mathsf{P}{g}\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\circ g\bigr{\rrbracket}_{G}\to\llbracket g_{4}\circ g\rrbracket_{G}~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{F}\,,

since $g_{3}\circ g=g_{1}$ and $g_{4}\circ g=g_{4}$ . By right adjunction we thus get

\begin{array}[b]{r@{~{}~}c@{~{}~}l}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}~{}{}&\leq\hfil~{}{}&\forall{g}\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}\\ \forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}~{}{}&\leq\hfil~{}{}&(\forall\langle g_{1},g_{2}\rangle\circ\forall{g})\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}\\ \forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}~{}{}&\leq\hfil~{}{}&\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}\,,\\ \end{array}\begin{tabular}[b]{@{}l}hence\\[3.0pt] and thus\\ \end{tabular}

using the fact that $\langle g_{1},g_{2}\rangle\circ g=\langle g_{1}\circ g,g_{2}\circ g\rangle=\langle g_{1},g_{2}\rangle$ .

$({\geq})$ From Coro. 2.13, we get $\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\leq\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}$ (since $g_{1}(z)\subseteq g_{3}(z)$ for all $z\in G$ ). Hence $\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}~{}\geq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}$ , and thus:

∎

\textstyle\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{3}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}~{}\geq~{}\forall\langle g_{1},g_{2}\rangle\Bigl{(}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ g_{1}\bigr{\rrbracket}_{G}\to\llbracket g_{4}\rrbracket_{G}\Bigr{)}\,.

We can now state the desired property:

Proposition 3.11.

$\langle\mskip-4.0mu\langle a\to b\rangle\mskip-4.0mu\rangle_{(a,b)\in\mathscr{A}^{2}}=\langle\mskip-4.0mu\langle\pi\rangle\mskip-4.0mu\rangle_{\mathscr{A}^{2}}\to\langle\mskip-4.0mu\langle\pi^{\prime}\rangle\mskip-4.0mu\rangle_{\mathscr{A}^{2}}~{}({\in}~{}\mathsf{P}(\mathscr{A}\times\mathscr{A}))$ ,
writing $\pi,\pi^{\prime}:\mathscr{A}^{2}\to\mathscr{A}$ the two projections from $\mathscr{A}^{2}$ to $\mathscr{A}$ .

Proof.

Indeed, we have:

\begin{array}[b]{r@{~{}~}l@{~{}~}l@{\hskip-10mm}}\langle\mskip-4.0mu\langle a\to b\rangle\mskip-4.0mu\rangle_{(a,b)\in\mathscr{A}^{2}}~{}{}&=\hfil~{}{}&\llbracket\varphi(a\to b)\rrbracket_{(a,b)\in\mathscr{A}^{2}}\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\Bigl{\llbracket}\varphi\Bigl{(}\bigl{\{}s^{\prime}\mapsto\beta~{}:~{}s^{\prime}\in\tilde{\varphi}_{0}(a)^{\subseteq},~{}\beta\in b\bigr{\}}\Bigr{)}\Bigr{\rrbracket}_{(a,b)\in\mathscr{A}^{2}}\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s^{\prime}\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}s^{\prime}\in\tilde{\varphi}_{0}(a)^{\subseteq},~{}\xi\in\tilde{\varphi}_{0}(b)\Bigr{\}}\Bigr{\rrbracket}_{(a,b)\in\mathscr{A}^{2}}\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\mathsf{P}(\tilde{\varphi}_{0}\times\tilde{\varphi}_{0})\left(\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s^{\prime}\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}s^{\prime}\in s^{\subseteq},~{}\xi\in t\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\right)\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\mathsf{P}(\tilde{\varphi}_{0}\times\tilde{\varphi}_{0})\left(\Bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\Bigl{\{}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s\bigr{)}\mathbin{\dot{{\to}}}\xi~{}:~{}\xi\in t\Bigr{\}}\Bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\right)\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\mathsf{P}(\tilde{\varphi}_{0}\times\tilde{\varphi}_{0})\left(\bigl{\llbracket}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}s\bigr{)}\mathbin{\dot{{\to}}}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}t\bigr{)}\bigr{\rrbracket}_{(s,t)\in\mathfrak{P}(\Sigma)^{2}}\right)\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\bigl{\llbracket}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}\tilde{\varphi}_{0}(a)\bigr{)}\mathbin{\dot{{\to}}}\bigl{(}{\mathbin{\dot{{\bigwedge}}}}\tilde{\varphi}_{0}(b)\bigr{)}\bigr{\rrbracket}_{(a,b)\in\mathscr{A}^{2}}~{}=~{}\llbracket\varphi(a)\mathbin{\dot{{\to}}}\varphi(b)\rrbracket_{(a,b)\in\mathscr{A}^{2}}\hfil\hskip-28.45274pt\\ ~{}{}&=\hfil~{}{}&\llbracket\varphi\circ\pi\rrbracket_{\mathscr{A}^{2}}\to\llbracket\varphi\circ\pi^{\prime}\rrbracket_{\mathscr{A}^{2}}~{}=~{}\langle\mskip-4.0mu\langle\pi\rangle\mskip-4.0mu\rangle_{\mathscr{A}^{2}}\to\langle\mskip-4.0mu\langle\pi^{\prime}\rangle\mskip-4.0mu\rangle_{\mathscr{A}^{2}}\hfil\hskip-28.45274pt\\ \end{array}\begin{tabular}[b]{r@{}}(by Lemma~{}\ref{l:ImpTech})\\[5.0pt] (by Coro.~{}\ref{c:DistrForallImp})\\[3.0pt] \\ \mbox{\qed}\\ \end{tabular}

Proposition 3.12.

Let $X$ be a set. For all codes $a,b\in\mathscr{A}^{X}$ , we have

(\in 𝖯 ​ X)

\textstyle\langle\mskip-4.0mu\langle a_{x}\to b_{x}\rangle\mskip-4.0mu\rangle_{x\in X}~{}=~{}\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X}\to\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{X}

Proof.

Same argument as for Prop. 2.4 p. 2.4. ∎

3.6. Defining the separator $S\subseteq\mathscr{A}$

By analogy with the construction of the pseudo-filter $\Phi\subseteq\Sigma$ (cf Section 2.4), we let

(\subseteq 𝒜)

S~{}:=~{}\bigl{\{}a\in\mathscr{A}~{}:~{}\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{\_\in 1}=\top_{1}\bigr{\}}

writing $\top_{1}$ the top element of $\mathsf{P}{1}$ . Note that by construction, we have

S~{}=~{}\bigl{\{}a\in\mathscr{A}~{}:~{}\llbracket\varphi(a)\rrbracket_{\_\in 1}=\top_{1}\bigr{\}}~{}=~{}\bigl{\{}a\in\mathscr{A}~{}:~{}\varphi(a)\in\Phi\bigr{\}}~{}=~{}\varphi^{-1}(\Phi)\,.

Proposition 3.13.

The subset $S\subseteq\mathscr{A}$ is a separator of the implicative structure $(\mathscr{A},{\preccurlyeq},{\to})$ .

Proof.

$S$ is upwards closed. Let $a,b\in\mathscr{A}$ such that $a\in S$ and $a\preccurlyeq b$ (that is: $b\subseteq a$ ). From these assumptions, we have $\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{\_\in 1}=\top_{1}$ and $\tilde{\varphi}_{0}(b)\subseteq\tilde{\varphi}_{0}(a)$ , hence

\textstyle\top_{1}~{}=~{}\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{\_\in 1}~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\tilde{\varphi}_{0}(a)\bigr{\rrbracket}_{\_\in 1}~{}=~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ(\tilde{\varphi}_{0}(a))_{\_\in 1}\bigr{\rrbracket}_{1}~{}\leq~{}\bigl{\llbracket}{\mathbin{\dot{{\bigwedge}}}}\circ(\tilde{\varphi}_{0}(b))_{\_\in 1}\bigr{\rrbracket}_{1}~{}=~{}\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{\_\in 1}

(from Coro. 2.13) and thus $\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{\_\in 1}=\top_{1}$ . Therefore $b\in S$ .

$S$ contains $\mathbf{K}^{\mathscr{A}}$ and $\mathbf{S}^{\mathscr{A}}$ . We observe that

\begin{array}[]{r@{~{}~}c@{~{}~}l}\bigl{\langle}\mskip-4.0mu\bigl{\langle}\mathbf{K}^{\mathscr{A}}\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{\_\in 1}~{}{}&=\hfil~{}{}&\Bigl{\langle}\mskip-4.0mu\Bigl{\langle}\bigcurlywedge_{a\in\mathscr{A}}\bigcurlywedge_{b\in\mathscr{B}}(a\to b\to a)\Bigr{\rangle}\mskip-4.0mu\Bigr{\rangle}_{\_\in 1}\\[6.0pt] ~{}{}&=\hfil~{}{}&\forall{\pi_{1,\mathscr{A}}}\Bigl{(}\Bigl{\langle}\mskip-4.0mu\Bigl{\langle}\bigcurlywedge_{b\in\mathscr{B}}(a\to b\to a)\Bigr{\rangle}\mskip-4.0mu\Bigr{\rangle}_{(\_\,,a)\in 1\times\mathscr{A}}\Bigr{)}\\[6.0pt] ~{}{}&=\hfil~{}{}&\forall{\pi_{1,\mathscr{A}}}\bigl{(}\forall{\pi_{1\times\mathscr{A},\mathscr{A}}}\bigl{(}\bigl{\langle}\mskip-4.0mu\bigl{\langle}a\to b\to a\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{((\_\,,a),b)\in(1\times\mathscr{A})\times\mathscr{A}}\bigr{)}\bigr{)}\\[3.0pt] ~{}{}&=\hfil~{}{}&\forall{\pi_{1,\mathscr{A}}}\bigl{(}\forall{\pi_{1\times\mathscr{A},\mathscr{A}}}\bigl{(}\top_{(1\times\mathscr{A})\times\mathscr{A}}\bigr{)}\bigr{)}~{}=~{}\top_{1}\\ \end{array}

hence $\mathbf{K}^{\mathscr{A}}\in S$ . The proof that $\mathbf{S}^{\mathscr{A}}\in S$ is analogous.

$S$ is closed under modus ponens. Suppose that $(a\to b)\in S$ and $a\in S$ . This means that $\langle\mskip-4.0mu\langle a\to b\rangle\mskip-4.0mu\rangle_{\_\in 1}=\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{\_\in 1}\to\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{\_\in 1}=\top_{1}$ and $\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{\_\in 1}=\top_{1}$ . Hence $\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{\_\in 1}=\top_{1}$ , and thus $b\in S$ . ∎

Similarly to Prop. 2.7 p. 2.7, the following proposition characterizes the ordering on each Heyting algebra $\mathsf{P}{X}$ from the operations of $\mathscr{A}$ and the separator $S\subseteq\mathscr{A}$ :

Proposition 3.14.

For all sets $X$ and for all codes $a,b\in\mathscr{A}^{X}$ , we have:

\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X}\leq\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{X}\quad\text{iff}\quad\bigcurlywedge_{x\in X}(a_{x}\to b_{x})~{}\in~{}S\,.

Proof.

Writing $1_{X}:X\to 1$ the unique map from $X$ to $1$ , we have:

∎

\begin{array}[b]{r@{\quad}c@{\quad}l}\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X}\leq\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{X}&\text{iff}&\top_{X}\leq\langle\mskip-4.0mu\langle a\rangle\mskip-4.0mu\rangle_{X}\to\langle\mskip-4.0mu\langle b\rangle\mskip-4.0mu\rangle_{X}\\ &\text{iff}&\mathsf{P}{1_{X}}(\top_{1})\leq\langle\mskip-4.0mu\langle a_{x}\to b_{x}\rangle\mskip-4.0mu\rangle_{x\in X}\\ &\text{iff}&\top_{1}\leq\forall{1_{X}}\bigl{(}\langle\mskip-4.0mu\langle a_{x}\to b_{x}\rangle\mskip-4.0mu\rangle_{x\in X}\bigr{)}\\ &\text{iff}&\top_{1}\leq\bigl{\langle}\mskip-4.0mu\bigl{\langle}{\bigcurlywedge}\{a_{x}\to b_{x}:x\in X\}\bigr{\rangle}\mskip-4.0mu\bigr{\rangle}_{\_\in 1}\\ &\text{iff}&\displaystyle\bigcurlywedge_{x\in X}(a_{x}\to b_{x})~{}\in~{}S\,.\\ \end{array}

3.7. Constructing the isomorphism

Let us now write $\mathsf{P}^{\prime}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{HA}$ the tripos induced by the implicative algebra $(\mathscr{A},{\preccurlyeq},{\to},S)$ (Section 1.2). Recall that for each set $X$ , the Heyting algebra $\mathsf{P}^{\prime}{X}:=\mathscr{A}^{X}/S[X]$ is the poset reflection of the preordered set $(\mathscr{A}^{X},\vdash_{S[X]})$ whose preorder $\vdash_{S[X]}$ is given by

(for all ​ a, b \in 𝒜^{X})

a\vdash_{S[X]}b\quad\text{iff}\quad\bigcurlywedge_{x\in X}(a_{x}\to b_{x})~{}\in~{}S

It now remains to show that:

Proposition 3.15.

The implicative tripos $\mathsf{P}^{\prime}$ is isomorphic to the tripos $\mathsf{P}$ .

Proof.

Let us consider the family of maps $\rho_{X}:=\langle\mskip-4.0mu\langle\_\rangle\mskip-4.0mu\rangle_{X}:\mathscr{A}^{X}\to\mathsf{P}{X}$ , which is clearly natural in the parameter set $X$ . From Prop. 3.14, we have

(for all ​ a, b \in 𝒜^{X})

a\vdash_{S[X]}b\quad\text{iff}\quad\bigcurlywedge_{x\in X}(a_{x}\to b_{x})~{}\in~{}S\quad\text{iff}\quad\rho_{X}(a)\leq\rho_{X}(b)

hence $\rho_{X}:\mathscr{A}^{X}\to\mathsf{P}{X}$ induces an embedding of posets $\tilde{\rho}_{X}:\mathsf{P}^{\prime}{X}\to\mathsf{P}{X}$ through the quotient $\mathsf{P}^{\prime}{X}:=\mathscr{A}^{X}/S[X]$ . Moreover, the map $\tilde{\rho}_{X}:\mathsf{P}^{\prime}{X}\to\mathsf{P}{X}$ is surjective (since $\rho_{X}$ is), therefore it is an isomorphism from the tripos $\mathsf{P}^{\prime}$ to the tripos $\mathsf{P}$ . ∎

The proof of Theorem 1.1 p. 1.1 is now complete.

3.8. The case of classical triposes

In [3], we showed that each classical implicative tripos (that is: a tripos induced by a classical implicative algebra $\mathscr{A}$ ) is isomorphic to a Krivine tripos (that is: a tripos induced by an abstract Krivine structure). Combining this result with Theorem 1.1, we deduce that classical realizability provides a complete description of all classical triposes $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{BA}$ (writing $\mathbf{BA}\subset\mathbf{HA}$ the full subcategory of Boolean algebras):

Corollary 3.16.

Each classical tripos $\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{BA}$ is isomorphic to a Krivine tripos.

Acknowledgements

We would like to thank Étienne Miquey and Luc Pellissier for their useful remarks and corrections in an earlier version of this draft.

References

[1] E. Engeler. Algebras and combinators. Algebra Universalis, 13(1):389–392, 1981.
[2] J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. In Math. Proc. Cambridge Philos. Soc., volume 88, pages 205–232, 1980.
[3] A. Miquel. Implicative algebras: a new foundation for realizability and forcing. Math. Struct. Comput. Sci., 30(5):458–510, 2020.
[4] A. M. Pitts. The theory of triposes. PhD thesis, University of Cambridge, 1981.
[5] A. M. Pitts. Tripos theory in retrospect. Math. Struct. Comput. Sci., 12(3):265–279, 2002.
[6] T. Streicher. Krivine’s classical realisability from a categorical perspective. Math. Struct. Comput. Sci., 23(6):1234–1256, 2013.

Implicative algebras II: completeness w.r.t. Set-based triposes

Abstract.

1. Introduction

Theorem 1.1.

1.1. 𝐒𝐞𝐭\mathbf{Set}-based triposes

Definition 1.2 (𝐒𝐞𝐭\mathbf{Set}-based triposes).

Remarks 1.3.

Definition 1.4 (Isomorphism of triposes).

Remark 1.5.

Lemma 1.6.

Proof.

Lemma 1.7.

Proof.

1.2. Implicative algebras

2. Anatomy of a 𝐒𝐞𝐭\mathbf{Set}-based tripos

2.1. The generic predicate

Notation 2.1.

Fact 2.2 (Naturality of ⟦_⟧X\llbracket\_\rrbracket_{X}).

Proof.

Remarks 2.3 (Non-uniqueness of generic predicates).

2.2. Defining connectives on Σ\Sigma

Proposition 2.4.

Proof.

Proposition 2.5.

Proof.

2.3. Defining quantifiers on Σ\Sigma

Proposition 2.6.

Proof.

2.4. Defining the ‘filter’ Φ\Phi

Proposition 2.7.

Proof.

Remark 2.8.

2.5. Miscellaneous properties

Proposition 2.9 (Merging quantifications).

Proof.

Proposition 2.10.

Proof.

Corollary 2.11.

Proof.

Proposition 2.12.

Proof.

Corollary 2.13.

Proof.

3. Extracting the implicative algebra

3.1. Defining the set 𝒜0\mathscr{A}_{0} of atoms

Fact 3.1.

Proof.

Remark 3.2 (Relationship with graph models).

3.2. Defining the implicative structure (𝒜,≼,→)(\mathscr{A},{\preccurlyeq},{\to})

Proposition 3.3.

Proposition 3.4.

Proof.

3.3. Viewing 𝒜\mathscr{A} as a new set of propositions

Lemma 3.5.

Proof.

Proposition 3.6.

Proof.

Proposition 3.7.

Proof.

3.4. Universal quantification in 𝒜\mathscr{A}

Proposition 3.8.

Proof.

Proposition 3.9.

Proof.

3.5. Implication in 𝒜\mathscr{A}

Lemma 3.10.

Proof.

Proposition 3.11.

Proof.

Proposition 3.12.

Proof.

3.6. Defining the separator S⊆𝒜S\subseteq\mathscr{A}

Proposition 3.13.

Proof.

Proposition 3.14.

Proof.

3.7. Constructing the isomorphism

Proposition 3.15.

Proof.

3.8. The case of classical triposes

Implicative algebras II:
completeness w.r.t. Set-based triposes

1.1. $\mathbf{Set}$ -based triposes

Definition 1.2 ( $\mathbf{Set}$ -based triposes).

2. Anatomy of a $\mathbf{Set}$ -based tripos

Fact 2.2 (Naturality of $\llbracket\_\rrbracket_{X}$ ).

2.2. Defining connectives on $\Sigma$

2.3. Defining quantifiers on $\Sigma$

2.4. Defining the ‘filter’ $\Phi$

3.1. Defining the set $\mathscr{A}_{0}$ of atoms

3.2. Defining the implicative structure $(\mathscr{A},{\preccurlyeq},{\to})$

3.3. Viewing $\mathscr{A}$ as a new set of propositions

3.4. Universal quantification in $\mathscr{A}$

3.5. Implication in $\mathscr{A}$

3.6. Defining the separator $S\subseteq\mathscr{A}$