Chuangjie Xu, January 2016

We define some neccessary preliminaries for the exploration of the
Dialectica interpretation.

\begin{code}

module Preliminaries where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)

\end{code}

Function composition

\begin{code}

infixl  _∘_ 

_∘_ : {i j k : Level} {X : Set i} {Y : X → Set j} {Z : (x : X) → Y x → Set k} →
      ({x : X} → (y : Y x) → Z x y) → (f : (x : X) → Y x) →
      (x : X) → Z x (f x)
g ∘ f = λ x → g(f x)

\end{code}

Identity types

\begin{code}

infixl  _≡_
infixl  _·_

data _≡_ {i : Level} {A : Set i} : A → A → Set i where
 refl : {a : A} → a ≡ a

_⁻¹ : {i : Level} {A : Set i} {a b : A} → a ≡ b → b ≡ a
refl ⁻¹ = refl

_·_ : {i : Level} {A : Set i} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
refl · refl = refl

ap : {i j : Level} {A : Set i} {B : Set j} {a a' : A} (f : A → B) → a ≡ a' → f a ≡ f a'
ap f refl = refl

ap² : {i j k : Level} {A : Set i} {B : Set j} {C : Set k} {a a' : A} {b b' : B}
    → (f : A → B → C) → a ≡ a' → b ≡ b' → f a b ≡ f a' b'
ap² f refl refl = refl

transport : {i j : Level} {A : Set i} (P : A → Set j) {a b : A} → a ≡ b → P a → P b
transport P refl p = p

transport² : {i j k : Level} {A : Set i} {B : Set j} (P : A → B → Set k) {a a' : A} {b b' : B}
           → a ≡ a' → b ≡ b' → P a b → P a' b'
transport² P refl refl p = p

\end{code}

Σ-types and bianry products

\begin{code}

infixr  _,_

record Σ {i j : Level} {A : Set i} (B : A → Set j) : Set (i ⊔ j) where
  constructor _,_
  field
   pr₀ : A
   pr₁ : B pr₀

open Σ public

infixl  _×_

_×_ : {i j : Level} → Set i → Set j → Set (i ⊔ j)
A × B = Σ \(_ : A) → B

uncurry : {i j k : Level} {A : Set i} {B : A → Set j} {C : Σ B → Set k}
        → ((a : A) → (b : B a) → C (a , b))
        → (w : Σ B) → C w
uncurry f (a , b) = f a b

\end{code}

Singleton type

\begin{code}

data 𝟙 : Set where
 ⋆ : 𝟙

\end{code}

Natrual numbers

\begin{code}

data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

rec : {A : ℕ → Set} → A  → ((n : ℕ) → A n → A (succ n)) → (n : ℕ) → A n
rec a f zero = a
rec a f (succ n) = f n (rec a f n)

\end{code}

Finite lists

\begin{code}

infixl  _₊_
infixl  _₊₊_

data List {i : Level} (A : Set i) : Set i where
 ε : List A
 _₊_ : List A → A → List A

₊⁼ : {i : Level} {A : Set i} {ρ ρ' : List A} {a a' : A}
   → ρ ≡ ρ' → a ≡ a' → (ρ ₊ a) ≡ (ρ' ₊ a')
₊⁼ refl refl = refl

_₊₊_ : {i : Level} {A : Set i} → List A → List A → List A
ρ ₊₊ ε = ρ
ρ ₊₊ (ρ' ₊ a) = (ρ ₊₊ ρ') ₊ a

len : {i : Level} {A : Set i} → List A → ℕ
len ε = 
len (ρ ₊ _) = succ (len ρ)

data Fin : ℕ → Set where
 zero : {n : ℕ} → Fin (succ n)
 succ : {n : ℕ} → Fin n → Fin (succ n)

Index : {i : Level} {A : Set i} → List A → Set
Index ρ = Fin (len ρ)

_₍_₎ : {i : Level} {A : Set i} → (ρ : List A) → Index ρ → A
ε ₍ () ₎
(ρ ₊ a) ₍ zero ₎   = a
(ρ ₊ a) ₍ succ i ₎ = ρ ₍ i ₎

\end{code}