\subsection{Some Preliminaries in Agda}
\label{sec:appl:agda-preliminaries}

\AgdaHide{
\begin{code}
{-# OPTIONS --without-K #-}
\end{code}
}

This first section is devoted to the introduction of the propositions-as-types
interpretation in Agda syntax.
We will interleave the given Agda code with the necessary explanation.
All the indented code is formally verified in Agda and will be explained as we
go.

We start off by introducing the propositions-as-types interpretation in its own
module called \AgdaModule{PropsAsTypes}.
Agda allows the separation of code into modules that can be imported in other
files, as we will see later.
\begin{code}
module PropsAsTypes where
\end{code}

Inside the module, we now introduce our first type, which implements the
dependent sum that we encountered earlier.
The following code declares a new inductive data type called $\Sigma$
with two parameters $I$ and $X$.
So far, we denoted the universe of valid types by $\univ{i}$, whereas Agda uses
the notation \AgdaFunction{Set} instead.
Thus, $I$ is a type parameter.
The parameter $X$, on the other hand, is a family of types.
In our syntax, we would denote this by $X : \pType[(i : I)]$ and instantiation
of $X$ with a parameter $t$ would be written as $X \inst t$.
Agda uses for types with parameters the same notation as for the
function space,\endnote{%
  In fact, $X \from I \to \mathrm{Set}$ is a function in Agda, only that it is
  a type in the universe $\mathrm{Set}_1$.
  This is similar to the situation in category theory, where a family of sets
  can be given by a functor from $I$, seen as a discrete category, to the
  category of sets.
  Such a functor is then an object in the large category of functors between
  categories.
}
so that the instantiation of $X$ is written as $X \> t$.

Another mechanism of Agda that appears in the definition of $\Sigma$ is that
$I$ is an implicit parameter, signified by the curly braces, and that $X$ is
an explicit parameter.
The idea of the implicit parameter mechanism is that Agda ought to be able to
infer the argument $I$ from the context.
For example, if we have a type $U : \NatT \to \mathrm{Set}$, then Agda can
infer from the instantiation $\Sigma \> U$ that $I$ needs to be instantiated
with $\NatT$.
Should this inference not be possible, then one can always resort to writing
$\Sigma \> \{\NatT\} \> U$ to explicitly give the parameter $I$.
We will see this below in the definition of the binary product.

The type $\Sigma$ itself has one constructor ``$,$'' with two arguments, where
the argument positions are marked by the underscores.
This allows us to write $(i, x)$ if $i : I$ and $x : X \> i$, thereby resembling
the pairing notation that we used before.
\begin{code}
data Σ {I : Set} (X : I → Set) : Set where
  _,_ : (i : I) → X i → Σ X
\end{code}

In \exRef{exists-quant-encode}, we denoted the type $\Sigma$ by $\exists$ to
emphasise its relation to existential quantification.
This was done in the light of the fact that the iteration scheme for that
type corresponded exactly to the usual elimination rule the existential
quantifier.
Later we introduced dependent iteration, which we could use in
\exRef{dep-it-exist-quant} to define both projections from the existential
type.
In this section, we will distinguish between $\Sigma$ as a data type, which
has both projections, and the existential quantifier as a proposition.
The latter will only come with the non-dependent elimination principle.

We now give the dependent iteration scheme for the dependent sum type
$\Sigma$.
Let $A$ be a type family that depends on $\Sigma \> X$, that is,
$A : \Sigma \> X \to \mathrm{Set}$.
Recall from \exRef{dep-it-exist-quant} that, if we want to eliminate
$\Sigma \> X$ into $A$, then we need to provide a term of type $A \> (i , x)$
with parameters $i : I$ and $x : X \> i$.
Such a term can equivalently be given as a dependent function $f$ of type
$\PiT{i : I} \PiT{x : X \> i} A \> (i, x)$.
In Agda, this function type is written as
\AgdaSymbol{(}\AgdaBound{i} \AgdaSymbol{:} \AgdaBound{I}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{x} \AgdaSymbol{:} \AgdaBound{X} \AgdaBound{i}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaBound{A} \AgdaSymbol{(}\AgdaBound{i} \AgdaInductiveConstructor{,} \AgdaBound{x}\AgdaSymbol{)},
in the style of de~Bruijn's telescopes~\cite{deBruijn1968:LangAutomath}.
Conveniently, we can define the dependent iteration scheme in Agda then
by using pattern matching as follows.
\begin{code}
drec-Σ :  {I : Set} {X : I → Set} {A : Σ X → Set} →
          ((i : I) → (x : X i) → A (i , x)) →
          (u : Σ X) → A u
drec-Σ f (i , x) = f i x
\end{code}

It is also straightforward to define, as we did in \exRef{dep-it-exist-quant},
the two projections for the dependent sum by appealing to dependent iteration.
\begin{code}
π₁ : {I : Set} {X : I → Set} → Σ X → I
π₁ = drec-Σ (λ i x → i)

π₂ : {I : Set} {X : I → Set} → (u : Σ X) → X (π₁ u)
π₂ = drec-Σ (λ i x → x)
\end{code}

From the dependent sum type we can also derive the binary product type.
Note that we introduced this type before as a coinductive type.
It saves us here, however, some work to define the binary product in terms of
the dependent sum.
\begin{code}
_×_ : Set → Set → Set
A × B = Σ {A} λ _ → B
\end{code}

In the propositions-as-types interpretation, one uses a type system to
represent logical propositions.
To make clear whenever we write a proof of a proposition that has been
internalised into Agda, we will use \AgdaFunction{Prop} instead of
\AgdaFunction{Set}.
Thus, if $\varphi$ is a proposition that we encoded in Agda, we will
denote this as $\varphi : \AgdaFunction{Prop}$.
This notation is introduced by the following definition.
\begin{code}
Prop = Set
\end{code}

An important logical connective that we will need later is conjunction.
Even though conjunction is defined in terms the binary product, we use
separate notations to emphasise its logical nature.
\begin{code}
_∧_ : Prop → Prop → Prop
A ∧ B = A × B

∧-elim₁ : {A₁ A₂ : Prop} → A₁ ∧ A₂ → A₁
∧-elim₁ = π₁

∧-elim₂ : {A₁ A₂ : Prop} → A₁ ∧ A₂ → A₂
∧-elim₂ = π₂

∧-intro : {A₁ A₂ : Prop} → A₁ → A₂ → A₁ ∧ A₂
∧-intro a₁ a₂ = (a₁ , a₂)
\end{code}

As already mentioned, we also introduce a separate notation for the existential
quantifier.
\begin{code}
∃ : {X : Set} → (A : X → Prop) → Prop
∃ = Σ
\end{code}

Agda allows us to provide a syntax for the existential quantifier that matches
the usual notation with explicit quantification domain.
It is not so relevant to precisely understand the following definition, the
reader should just remember that we can write ∃[ x ∈ X ] A instead of
$\exist{x : X} A$ for propositions $A$ with a free occurrence of $x$.
\begin{code}
∃-syntax : ∀ X → (X → Prop) → Prop
∃-syntax X A = ∃ A

syntax ∃-syntax X (λ x → A) = ∃[ x ∈ X ] A
\end{code}

From the pairing constructor and the iteration scheme for
the dependent sum type we obtain the usual introduction and elimination
rules for the existential quantifier that we already discussed in
\exRef{exists-quant-encode}.
For convenience, we also provide a scheme for the simultaneous elimination
of two existential quantifiers.
None of these definitions should come at a surprise to the reader at this
stage.
\begin{code}
∃-intro : {X : Set} {A : X → Prop} → (x : X) → A x → ∃[ x ∈ X ] (A x)
∃-intro x a = (x , a)

∃-elim :  {X : Set} {A : X → Prop} {B : Prop} →
          ((x : X) → A x → B) → ∃[ x ∈ X ] (A x) → B
∃-elim = drec-Σ

∃₂-elim :  {X Y : Set} {A : X → Prop} {B : Y → Prop} {C : Prop} →
           ((x : X) (y : Y) → A x → B y → C) →
           ∃[ x ∈ X ] (A x) → ∃[ x ∈ Y ] (B x) → C
∃₂-elim f p q = ∃-elim (λ x p' → ∃-elim (λ y q' → f x y p' q') q) p

\end{code}

\AgdaHide{
\begin{code}
infix  _⇔_
\end{code}
}

Finally, we define bi-implication between propositions, which is is of
course just given as the conjunction of implications in both directions.
\begin{code}
_⇔_ : Prop → Prop → Prop
A ⇔ B = (A → B) ∧ (B → A)

equivalence : {A B : Prop} → (A → B) → (B → A) → A ⇔ B
equivalence = ∧-intro
\end{code}

Having set up the necessary definitions of the propositions-as-types
interpretation, we can now move to more interesting topics.

%%% Local Variables:
%%% ispell-local-dictionary: "british"
%%% End: