Chuangjie Xu, July 2016

\begin{code}

module Preliminaries where

\end{code}

Function composition

\begin{code}

infixr  _∘_

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
f ∘ g = λ x → f (g x)

\end{code}

Σ-type and product

\begin{code}

infixr  _,_

record Σ {A : Set} (B : A → Set) : Set where
 constructor _,_
 field
  pr₁ : A
  pr₂ : B pr₁

open Σ public

infixr  _×_

_×_ : Set → Set → Set
A × B = Σ \(a : A) → B

\end{code}

Coproduct

\begin{code}

infixr  _+_

data _+_ (A B : Set) : Set where
 inl : A → A + B
 inr : B → A + B

case : {A B C : Set} → (A → C) → (B → C) → A + B → C
case f g (inl a) = f a
case f g (inr b) = g b

\end{code}

Singleton and empty types

\begin{code}

data 𝟙 : Set where
 ⋆ : 𝟙

data 𝟘 : Set where

𝟘-elim : {A : Set} → .𝟘 → A
𝟘-elim ()

¬ : Set → Set
¬ A = A → 𝟘

\end{code}

Identity type

\begin{code}

infix  _≡_ _≢_

data _≡_ {ℓ} {A : Set ℓ} (a : A) : A → Set ℓ where
 refl : a ≡ a

_≢_ : {A : Set} → A → A → Set
a ≢ b = ¬ (a ≡ b)

transport : {A : Set} (P : A → Set) {x y : A}
          → x ≡ y → P x → P y
transport P refl p = p

transport² : {A B : Set} (P : A → B → Set) {x y : A} {u v : B}
           → x ≡ y → u ≡ v → P x u → P y v
transport² P refl refl p = p

ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl

ap² : {A B : Set} {f g : A → B} {x y : A} → f ≡ g → x ≡ y → f x ≡ g y
ap² refl refl = refl

ap₂ : {A B C : Set} (f : A → B → C) {x x' : A} {y y' : B}
    → x ≡ x' → y ≡ y' → f x y ≡ f x' y'
ap₂ f refl refl = refl

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

pair⁼ : {A B : Set} {a a' : A} {b b' : B}
      → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
pair⁼ refl refl = refl

\end{code}