Chuangjie Xu, 2012

\begin{code}

module MiniLibrary where

\end{code}

Universe levels:

\begin{code}

postulate
 Level : Set
 zer   : Level
 suc   : Level → Level
 max   : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zer   #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  max   #-}

\end{code}

Identity function and function composition

\begin{code}

id : {X : Set} → X → X
id x = x


infixl  _∘_

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

\end{code}

Subset relation

\begin{code}

Subset : Set → Set₁
Subset X = X → Set

_∈_ : {X : Set} → X → Subset X → Set
x ∈ A = A x

\end{code}

Universe polymorphic sigma type

\begin{code}

infixr  _,_

record Σ {i j : Level} {I : Set i} (X : I → Set j) : Set (max i j) where
  constructor _,_
  field
   π₀ : I
   π₁ : X π₀

open Σ public

\end{code}

Cartesian products and conjunctions are defined using Σ types.

\begin{code}

infixr  _×_

_×_ : Set → Set → Set
X × Y = Σ \(x : X) → Y

infixr  _∧_

_∧_ : Set → Set → Set
X ∧ Y = Σ \(x : X) → Y

∧-elim₀ : {A₀ A₁ : Set} → A₀ ∧ A₁ → A₀
∧-elim₀ = π₀

∧-elim₁ : {A₀ A₁ : Set} → A₀ ∧ A₁ → A₁
∧-elim₁ = π₁

∧-intro : {A₀ A₁ : Set} → A₀ → A₁ → A₀ ∧ A₁
∧-intro a₀ a₁ = (a₀ , a₁)

\end{code}

Existential quantifier:

\begin{code}

∃ : {X : Set} → (A : X → Set) → Set
∃ = Σ

∃-intro : {X : Set}{A : X → Set} → (x₀ : X) → A x₀ → ∃ \(x : X) → A x
∃-intro x a = (x , a)

∃-witness : {X : Set}{A : X → Set} → (∃ \(x : X) → A x) → X
∃-witness = π₀

∃-elim : {X : Set}{A : X → Set} → (proof : ∃ \(x : X) → A x) → A (∃-witness proof)
∃-elim = π₁

\end{code}

Identity type and related lemmas:

\begin{code}

infix   _≡_

data _≡_ {X : Set} : X → X → Set where
  refl : {x : X} → x ≡ x

transport : {X : Set}{Y : X → Set}{x x' : X} → x ≡ x' → Y x → Y x'
transport refl y = y

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

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

ap : {X Y : Set} → ∀(f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
ap f refl = refl

fun-ap : {X Y : Set} → ∀{f g : X → Y} → f ≡ g → ∀(x : X) → f x ≡ g x
fun-ap r x = ap (λ h → h x) r

transport-refl : (A : Set) → (P : A → Set) → (a : A) → (p : P a) →
                 transport {A} {P} refl p ≡ p
transport-refl A P a p = refl

Lemma[transport] : (X : Set) → (P : X → Set) → (Q : (x : X) → P x → Set) →
                (x x' : X) → (eq : x ≡ x') → (p : P x) →
                  Q x p → Q x' (transport {X} {P} eq p)
Lemma[transport] X P Q x .x refl p q = q

Lemma[≡-Σ] : {X : Set}{P : X → Set}{x x' : X}{p : P x}{p' : P x'} →
              (e : x ≡ x') → transport {X} {P} e p ≡ p' → (x , p) ≡ (x' , p')
Lemma[≡-Σ] refl refl = refl

Lemma[≡-∧] : {A₀ A₁ : Set}{a₀ a₀' : A₀}{a₁ a₁' : A₁} → a₀ ≡ a₀' → a₁ ≡ a₁' → ∧-intro a₀ a₁ ≡ ∧-intro a₀' a₁'
Lemma[≡-∧] refl refl = refl

Lemma[≡-Σ]₀ : {X : Set}{P : X → Set}{w w' : Σ \(x : X) → P x} →
              w ≡ w' → π₀ w ≡ π₀ w'
Lemma[≡-Σ]₀ refl = refl

Lemma[≡-Σ]₁ : {X : Set}{P : X → Set}{w w' : Σ \(x : X) → P x} →
              (ew : w ≡ w') → transport {X} {P} (Lemma[≡-Σ]₀ ew) (π₁ w) ≡ π₁ w'
Lemma[≡-Σ]₁ refl = refl

\end{code}

Empty type:

\begin{code}

data ∅ : Set where

∅-elim : {i : Level}{A : Set i} → ∅ → A
∅-elim = λ ()

¬ : Set → Set
¬ X = X → ∅

infix  _≠_
_≠_ : {A : Set} → A → A → Set
A ≠ B = ¬ (A ≡ B)

\end{code}

Singleton type:

\begin{code}

data ⒈ : Set where
 ⋆ : ⒈

unit : {X : Set} → X → ⒈
unit x = ⋆

singleton : ∀(x x' : ⒈) → x ≡ x'
singleton ⋆ ⋆ = refl

\end{code}

Binary numbers, or booleans, and if-then function:

\begin{code}

data ₂ : Set where
 ₀ : ₂
 ₁ : ₂

if : {X : Set} → X → X → ₂ → X
if x x' ₀ = x
if x x' ₁ = x'

Lemma[₀≠₁] : ₀ ≠ ₁
Lemma[₀≠₁] ()

Lemma[₂-≡] : ∀{b b' : ₂} → (p q : b ≡ b') → p ≡ q
Lemma[₂-≡] refl refl = refl


\end{code}

Natural numbers and some operations on them:
 
\begin{code}

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

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}

pred : ℕ → ℕ
pred  = 
pred (succ n) = n

succ-injective : ∀{i j : ℕ} → succ i ≡ succ j → i ≡ j
succ-injective = ap pred

rec : {X : Set} → X → (ℕ → X → X) → ℕ → X
rec x f         = x
rec x f (succ n) = f n (rec x f n)

infixl  _+_

_+_ : ℕ → ℕ → ℕ
n +  = n
n + (succ m) = succ(n + m)

Lemma[0+m=m] : ∀(m : ℕ) →  + m ≡ m
Lemma[0+m=m]  = refl
Lemma[0+m=m] (succ m) = ap succ (Lemma[0+m=m] m)

Lemma[n+1+m=n+m+1] : ∀(n m : ℕ) → succ n + m ≡ n + succ m
Lemma[n+1+m=n+m+1] n  = refl
Lemma[n+1+m=n+m+1] n (succ m) = ap succ (Lemma[n+1+m=n+m+1] n m)

Lemma[n+m=m+n] : ∀(n m : ℕ) → n + m ≡ m + n
Lemma[n+m=m+n] n         = sym (Lemma[0+m=m] n)
Lemma[n+m=m+n] n (succ m) = trans (ap succ (Lemma[n+m=m+n] n m))
                                  (sym (Lemma[n+1+m=n+m+1] m n))

maximum : ℕ → ℕ → ℕ
maximum  m = m
maximum n  = n
maximum (succ n) (succ m) = succ (maximum n m)

\end{code}

Vectors and finite sequences:

\begin{code}

infixr  _∷_

data Vec (X : Set) : ℕ → Set where
 ⟨⟩ : Vec X 
 _∷_ : {n : ℕ} → X → Vec X n → Vec X (succ n)

head : {X : Set}{n : ℕ} → Vec X (succ n) → X
head (x ∷ _) = x

tail : {X : Set}{n : ℕ} → Vec X (succ n) → Vec X n
tail (_ ∷ xs) = xs

Lemma[Vec-≡] : ∀{n : ℕ}{X : Set} → ∀{v v' : Vec X (succ n)} →
                head v ≡ head v' → tail v ≡ tail v' → v ≡ v'
Lemma[Vec-≡] {n} {X} {x ∷ xs} {.x ∷ .xs} refl refl = refl

Vtake : {X : Set} → (n k : ℕ) → Vec X (n + k) → Vec X k
Vtake n         v       = ⟨⟩
Vtake n (succ k) (h ∷ t) = h ∷ Vtake n k t

Vdrop : {X : Set} → (n k : ℕ) → Vec X (n + k) → Vec X n
Vdrop n         v       = v
Vdrop n (succ k) (h ∷ t) = Vdrop n k t

\end{code}

Disjoint union:

\begin{code}

infixr  _⊎_
infixr  _∨_

data _⊎_ (X₀ X₁ : Set) : Set where
  in₀ : X₀ → X₀ ⊎ X₁
  in₁ : X₁ → X₀ ⊎ X₁

_∨_ : Set → Set → Set
_∨_ = _⊎_

case : {X₀ X₁ Y : Set} → (X₀ → Y) → (X₁ → Y) → X₀ ∨ X₁ → Y
case f₀ f₁ (in₀ x₀) = f₀ x₀
case f₀ f₁ (in₁ x₁) = f₁ x₁

equality-cases : {X₀ X₁ : Set} → {A : Set} →
    ∀(y : X₀ ∨ X₁) → (∀ x₀ → y ≡ in₀ x₀ → A) → (∀ x₁ → y ≡ in₁ x₁ → A) → A
equality-cases (in₀ x₀) f₀ f₁ = f₀ x₀ refl
equality-cases (in₁ x₁) f₀ f₁ = f₁ x₁ refl

cases : {X₀ X₁ Y₀ Y₁ : Set} → (X₀ → Y₀) → (X₁ → Y₁) → X₀ ∨ X₁ → Y₀ ∨ Y₁
cases f₀ f₁ (in₀ x₀) = in₀ (f₀ x₀)
cases f₀ f₁ (in₁ x₁) = in₁ (f₁ x₁)

Lemma[⊎] : {X₀ X₁ : Set} → (x : X₀ ⊎ X₁) →
             (∃ \(x₀ : X₀) → x ≡ in₀ x₀) ∨ (∃ \(x₁ : X₁) → x ≡ in₁ x₁)
Lemma[⊎] (in₀ x₀) = in₀ (x₀ , refl)
Lemma[⊎] (in₁ x₁) = in₁ (x₁ , refl)

\end{code}

Definitions of decidability, disrectess, hproposition and hset:

\begin{code}

decidable : Set → Set
decidable A = A ∨ (¬ A)

discrete : Set → Set
discrete A = ∀(a a' : A) → decidable (a ≡ a')

hprop : Set → Set
hprop X = (x y : X) → x ≡ y

hset : Set → Set
hset X = (x y : X) → hprop (x ≡ y)

\end{code}

Both ℕ and ₂ are hsets and discrete.

\begin{code}

ℕ-discrete : discrete ℕ
ℕ-discrete   = in₀ refl
ℕ-discrete  (succ m) = in₁ (λ ())
ℕ-discrete (succ n)  = in₁ (λ ())
ℕ-discrete (succ n) (succ m) = step (ℕ-discrete n m)
 where
  step : decidable(n ≡ m) → decidable (succ n ≡ succ m)
  step (in₀ r) = in₀ (ap succ r)
  step (in₁ f) = in₁ (λ s → f (succ-injective s))

Lemma[n≡0∨n≡m+1] : ∀(n : ℕ) → n ≡  ∨ (∃ \(m : ℕ) → n ≡ succ m)
Lemma[n≡0∨n≡m+1]         = in₀ refl
Lemma[n≡0∨n≡m+1] (succ n) = in₁ (n , refl)

≡ℕ-discrete : {m n : ℕ} → discrete (m ≡ n)
≡ℕ-discrete refl refl = in₀ refl

ℕ-hset : hset ℕ
ℕ-hset n .n refl refl = refl

₂-discrete : discrete ₂
₂-discrete ₀ ₀ = in₀ refl
₂-discrete ₀ ₁ = in₁ (λ ())
₂-discrete ₁ ₀ = in₁ (λ ())
₂-discrete ₁ ₁ = in₀ refl

≡₂-discrete : {b b' : ₂} → discrete (b ≡ b')
≡₂-discrete refl refl = in₀ refl

₂-hset : hset ₂
₂-hset b .b refl refl = refl

Lemma[b≡₀∨b≡₁] : ∀(b : ₂) → (b ≡ ₀) ∨ (b ≡ ₁)
Lemma[b≡₀∨b≡₁] ₀ = in₀ refl
Lemma[b≡₀∨b≡₁] ₁ = in₁ refl

\end{code}

Finite sets:

\begin{code}

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

toℕ : {n : ℕ} → Fin n → ℕ
toℕ zero     = 
toℕ (succ i) = succ (toℕ i)

fromℕ : (n : ℕ) → Fin (succ n)
fromℕ         = zero
fromℕ (succ n) = succ (fromℕ n)

\end{code}