I'm having trouble understanding this definition.
I use Hyperdoctrine in the sense of Pitts. I know the word hyperdoctrine is very loaded so let me give some definitions before the actual question just in case.
Definitions
Definition (Hyperdoctrine):
A hyperdoctrine is a pair $(C,P)$ where $C$ is a cartesian category and $P$ is a functor from $C^{op}$ to some desired subcategory of $Cat$, depending on which kind of logic you want to work with. Let's consider the subcategory $HA$ for simplicity, the category of heyting algebras and heyting morphisms.
We can add more stuff to this definition (e.g: Beck-Chevalley condition) but let's stick with this for simplicity. It can be brought up if necessary.
Definition (Structure in a hyperdoctrine):
Given a signature $Sg$ of typed function symbols $f : σ_1 × \dots × σ_n → τ$ and typed relation symbols $R ⊆ σ_1 × \dots × σ_n$, a structure over a hyperdoctrine $(C,P)$ is defined by giving an object of $C$ $[\![ σ ]\!]$ for each sort $σ$, an arrow $[\![f]\!] : [\![ σ_1 ]\!] × \dots × [\![ σ_n ]\!] → [\![ τ ]\!]$ for each arrow symbol $f : σ_1 × \dots × σ_n → τ$, and an object $[\![R]\!] ∈ P\ ([\![ σ_1 ]\!] × \dots × [\![ σ_n ]\!])$ for each relation symbol $R ⊆ σ_1 × \dots × σ_n$.
Then you can define by induction the rest of the well formed formulas over a context $ \Gamma $ and these will also satisfy $[\![\Gamma\ |\ φ]\!] ∈ P\ [\![\Gamma]\!]$.
The same is done for well formed terms.
I'm pretty sure that I've seen the following definition somewhere, but I don't recall where, I think it was some slides, not an actual book nor paper, and maybe I'm missing something, so I appreciate it if I'm corrected:
Definition (Morphism of hyperdoctrines):
Given two hyperdoctrines (with the same codomain, say $HA$) $(C,P)$ and $(D,Q)$, we define a morphism between them as a cartesian functor $F : C → D$ together with a natural transformation $α : P → Q ◦ F^{op}$. (We may ask of this natural transformation to preserve adjoints as well.)
Question
I've seen that for equational theories (without formulas other than equalities) you can define structures over them with the classifying category, namely a structure over some signature $Sg$ in a category $C$ can be thought of as a cartesian functor $\mathcal Cl\ Sg → C$.
I was wondering if we could do the same with hyperdoctrines, namely define a "classifying hyperdoctrine" (this exact keyword doesn't give results in google), probably as a hyperdoctrine such that its category is the classifying category of your signature (or theory) and the functor should encode syntactically the relation symbols somehow, but I just haven't found out what this definition should be exactly.
Then a structure should be a morphism of hyperdoctrines such that its domain is this "classifying hyperdoctrine".
(It's clear that what's missing is what to do with formulas and relation symbols, the terms and function symbols are dealt with the functor out of the classifying category.)
The following seems to work.
For each context we may construct a "free" heyting algebra generated by the formulas over that context.
This gives us a map from the objects of $\mathcal Cl\ Sg$ to the objects of $HA$. Call it $P$.
To make it into a contravariant functor we construct a $HA$ morphism $P\ ts : P\ \Delta \rightarrow P\ \Gamma$ for each multiterm $ts : \Gamma \rightarrow \Delta$.
Over relation symbols $R (Ms) : P\ \Delta$ it outputs $R (Ms \circ ts) : P\ \Gamma$.
We must also extend this map accordingly to the rest of the formulas.
We would expect this functor to give us an adjunction between signatures and hyperdoctrines (which can be thought of as a subcategory of $Cat/HA$), which would give us the desired universal property.