Triposes
1 Notation
Let \(\mathcal{C}\) be a cartesian-closed category and \(P : \mathcal{C}^\texttt{op}→ \textrm{HeytAlg}\) a functor between poset-enriched categories. Also, we will call objects of \(\mathcal{C}\) types. We also fix a choice of finite products and exponents in \(\mathcal{C}\).
2 Definition of a tripos
A functor \(P\) is a tripos when it satisfies the following:
For all types \(X\) and \(Y\) and maps \(f : X → Y\), the map \(Pf\) has monotone left and right adjoints, \(∃_f\) and \(∀_f\) respectively
These further satisfy the Beck-Chevalley condition: If
\[ \begin{tikzcd} X \ & Y \\ Z \ & W \arrow["f", from=1-1, to=1-2] \arrow["g"', from=1-1, to=2-1] \arrow["h", from=1-2, to=2-2] \arrow["k"', from=2-1, to=2-2] \end{tikzcd} \]is a pullback square then \(∀_f ∘Pg = Ph ∘∀_k\)
There is a type \(\Sigma \) and an element \(\sigma ∈ P(\Sigma )\) such that for every object \(X\) and every \(φ ∈ P(X)\) there is a morphism \([φ] : X → \Sigma \) such that \(φ = P([φ])(\sigma )\)
3 Definition of a tripos language
A context is a list of pairs of variables and objects of \(\mathcal{C}\). We write it like \(x₁ : X₁,… , xₙ : Xₙ\), where \(xᵢ\) are some variables and \(Xᵢ\) some types.
Let \(Γ = x₁ : X₁,… , xₙ : Xₙ\) be an arbitrary context.
Terms of type \(X\) in context \(Γ\) are
variables \(xᵢ\),
the unique element of the terminal type \(\texttt{tt}\),
ordered pairs \(⟨a, b⟩\), where \(a\) and \(b\) are also terms in context \(Γ\),
the first and second pojections of terms \(\texttt{fst}\) and \(\texttt{snd}\), or
terms \(f(t)\), where \(t\) is a term of type \(Y\) in context \(Γ\) and \(f : Y → X\) a morphism.
Write \(Γ ⊢_t t\) to mean “the term \(t\) in context \(Γ\)”.
We can define the evaluation of terms of type \(X\) in context \(Γ\) to morphisms \(X₁×\dots × Xₙ → X\):
\(Γ ⊢_t xᵢ \Downarrow πᵢ\), where \(πᵢ\) is the projection from \(X₁×\dots × Xₙ\) ommitting the \(i\)-th component,
\(Γ ⊢_t \texttt{tt} \Downarrow !_{X₁×\dots × Xₙ}\),
\(Γ ⊢_t ⟨a, b⟩ \leadsto ⟨Γ ⊢_t a, Γ ⊢_t b⟩\), where \(⟨⟩\) on the right-hand side is the pairing function in \(\mathcal{C}\),
\(Γ ⊢_t \texttt{fst} \Downarrow π\) and \(Γ ⊢_t \texttt{snd} \Downarrow π'\), where \(π\) and \(π'\) are the first and second projections in \(\mathcal{C}\) respectively, and
\(Γ ⊢_t f(t) \leadsto f∘(Γ ⊢_t t)\).
Formulas of type \(X\) in context \(Γ\) are
\(R(t)\), where \(t\) is a term of type \(Y\) in context \(Γ\) and \(R ∈ P(Y)\),
one of the usual Heyting algebra formers, or
the quantifiers \(∃ x : X,\ φ\) and \(∀ x : X,\ φ\), where \(φ\) is a formula.
Write \(Γ ⊢_f t\) to mean “the formula \(t\) in context \(Γ\)”.
Again we can define the evaluation of formulas in context \(Γ\) to elements of Heyting algebras:
\(Γ ⊢_f R(t) \Downarrow P(t)(R)\),
the Heyting algebra formers get evaluated to themselves in the obvious way,
if \(x\) is a free variable in \(φ\) then \(Γ ⊢_f Q x : X,\ φ \Downarrow Q_f (Γ, x : X ⊢_f φ)\), where \(Q\) is a quantifier, and
if \(x\) is not a free variable in \(φ\) then \(Γ ⊢_f Q x : X,\ φ \Downarrow Q_π(π^*(Γ, x : X ⊢_f φ))\), where \(Q\) is a quantifier.
Also, let \(P(Γ)\) mean the same as \(P(X₁,…,Xₙ)\).
Note: due to implementation issues, there is an intermediary type of formulas, defined inductively with the above constructions, quotiented with equivalence up to evaluation by the above rules. This gives us a type equivalent to the Heyting algebras \(P(X)\), but it behaves much better with rewriting in Lean.
We call a formula \(φ\) in context \(Γ\) true when it evaluates to the top element of \(P(Γ)\). We denote this by \(Γ ⊢ φ\).
Showing \(Γ ⊢ φ ⇒ ψ\) is equivalent to showing \((Γ ⊢_f φ) ≤ (Γ ⊢_f ψ)\).
The expression \(Γ ⊢ φ ⇒ ψ\) is defined to be \(⊤ = (Γ ⊢_f φ ⇒ ψ) = (Γ ⊢_f φ) ⇒ (Γ ⊢_f ψ)\). Equality with \(⊤\) is the same as being greater than \(⊤\). Now using that \(⊓\) is left adjoint to \(⇒\) we get \((Γ ⊢_f φ) ≤ (Γ ⊢_f ψ)\).
4 Definition of a partial equivalence relation
A partial equivalence relation (PER) on the type \(X\) over a tripos \(P\) is an element \(ρ_X ∈ P(X × X)\) that satisfies
\(x : X, y : X ⊢ ρ_X(x,y) ⇒ ρ_X(y,x)\)
\(x : X, y : X, z : Z ⊢ ρ_X(x,y) ⊓ ρ_X(y,z) ⇒ ρ_X(x,z)\)
The first condition is called symmerty and the second transitivity, so a PER indeed a partial equivalence relation in the internal language.
From now on we will write \(x =_X y\) to mean \(ρ_X(x,y)\), ommitting the subscript where the underlying type is obvious.
A morphism between PER’s \(ρ_X\) and \(ρ_Y\) over \(P\) is an element \(f : P(X × Y)\) that satisfies
\(x : X, x' : X, y : Y ⊢ x = x' ⊓ f(x', y) ⇒ f(x, y)\)
\(x : X, y : Y, y' : Y ⊢ f(x, y) ⊓ y = y' ⇒ f(x, y')\)
\(x : X, y : Y, y' : Y ⊢ f(x, y) ⊓ f(x, y') ⇒ y = y'\)
\(x : X ⊢ x = x ⇒ ∃ y : Y,\ f(x, y)\)
Again, we will write \(f(x) = y\) to mean \(f(x, y)\). We will also write \(f : ρ_X → ρ_Y\) to mean “a morphism \(f\) betweens PER’s \(ρ_X\) and \(ρ_Y\)”.
The first two properties here say the morphism is coherent with the PERs on the domain and codomain, and the other two are uniqueness and totality of a relation. So morphisms are defined as “functional relations internal to \(P\)”.
Let \(f : ρ_X → ρ_Y\) and \(g : ρ_Y → ρ_Z\) be PER morphisms. Their composite is defined to be the composte of relations in the internal language, in other words
Had we shown a soundness theorem, we could just say “it is constructively true that the composition of functional relations is a functional relation”, and be done with the proof. Nonetheless, the proof itself is relatively straight-forward.
To save space we will ommit the context in the following derivations. Also, to avoid ambiguity, we will denote eqality in a Heyting algebra using \(≡\).
The identity morphism on \(ρX\) is \(ρX\) itself.
In this proof we break convention and will use letters \(a\), \(b\),… to denote elements of \(X\).
The last property to show \(ρX\) is a PER morphism, \(a = a ≤ ∃ b : X,\ ρX(a) = b\), is somewhat tricky to prove using just the internal language, so we need to annotate a few things.
The LHS is actually \(δ^*ρX\) and the RHS is \(∃_π ρX\), where \(δ : X → X×X\) is the diagonal morphism and \(π : X×X → X\) the fist projection.
So we wish to show \(δ^*ρX ≤ ∃_π ρX\). By the \(f^* \dashv ∀_f\) adjunction, this is equivalent to \(ρX ≤ ∀_δ ∃_π ρX = ∀_δ δ^* π^* ∃_π ρX\). But this follows immediately from the units of the \(∀\) and \(∃\) adjunctions.
All that is left is to show composition with the identity is the identity. We only prove one identity law, since the proof of the other one is symmetric.
5 Tripos to topos construction
To a tripos \(P\) (over a category \(\mathcal{C}\)) we can associate the category \(\mathcal{C}[P]\) of types along with partial equivalence relations over \(P\) with morphisms as above.
The category \(\mathcal{C}[P]\) is a topos.