\,.\, \neg \varphi
        \end{aligned}$$ We assume that $\neg$ has the highest precedence.

-   The system ${\ensuremath{{\cal I}}}_s$ is given by the following rules and axioms, where $\Gamma$ is a finite set of terms, $t, \varphi, \psi,
        \alpha, \beta$, etc. are arbitrary terms. The notation $\Gamma,
        \varphi$ is a shorthand for $\Gamma \cup \{\varphi\}$. We use Greek letters $\varphi$, $\psi$, etc. to highlight that a term is to be intuitively interpreted as a proposition, and we use $\alpha$, $\beta$, etc. when it is to be interpreted as a type, but there is no a priori syntactic distinction. All judgements have the form $\Gamma {\ensuremath{\vdash}}t$ where $\Gamma$ is a set of terms and $t$ a term. In particular, $\Gamma {\ensuremath{\vdash}}t : \alpha$ is a shorthand for $\Gamma {\ensuremath{\vdash}}\mathrm{Is}\, t\, \alpha$, according to the convention from the previous point.

    [**Axioms**]{}

    -   $\Gamma, \varphi {\ensuremath{\vdash}}\varphi$

    -   $\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,t\,t\,}}$

    -   $\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Prop}}}: {\ensuremath{\mathrm{Type}}}$

    -   $\Gamma {\ensuremath{\vdash}}\iota : {\ensuremath{\mathrm{Type}}}$ for $\iota \in {\ensuremath{{\cal T}}}_I$

    -   $\Gamma {\ensuremath{\vdash}}o_i^\iota (c_i^\iota t_1 \ldots
              t_{n_i})$ if $c_i^\iota \in {\ensuremath{{\cal C}}}$ has arity $n_i$

    -   $\Gamma {\ensuremath{\vdash}}\neg (o_i^\iota (c_j^\iota t_1 \ldots
              t_{n_j}))$ if $i \ne j$ and $c_j^\iota \in {\ensuremath{{\cal C}}}$ has arity $n_j$

    -   $\Gamma {\ensuremath{\vdash}}{\ensuremath{\mathrm{Eq}\,(d_{i,k}^\iota (c_i^\iota t_1 \ldots
              t_{n_i}))\,t_k\,}}$ 