======================
= =
= §0 Mini library =
= =
======================
Chuangjie Xu
A small library for the Agda development of the paper
A Gentzen-style monadic translation of Gödel's System T
by Chuangjie Xu.
\begin{code}
{-# OPTIONS --without-K --safe #-}
module Preliminaries where
\end{code}
■ Identity types
\begin{code}
infix 2 _≡_
data _≡_ {ℓ} {A : Set ℓ} (a : A) : A → Set ℓ where
refl : a ≡ a
ap : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl
ap² : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''}
→ (f : A → B → C) {x y : A} {u v : B} → x ≡ y → u ≡ v → f x u ≡ f y v
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 p = p
transport : ∀ {ℓ ℓ'} {A : Set ℓ} (P : A → Set ℓ') {x y : A}
→ x ≡ y → P x → P y
transport P refl p = p
infix 1 begin_
infix 3 _∎
infixr 2 _≡⟨_⟩_
begin_ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x ≡ y
begin x≡y = x≡y
_≡⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
_∎ : ∀ {ℓ} {A : Set ℓ} (x : A) → x ≡ x
_∎ _ = refl
\end{code}
■ More operations and types
\begin{code}
_∘_ : {A : Set} {B : A → Set} {C : {a : A} → B a → Set}
→ ({a : A} (b : B a) → C b) → (f : (a : A) → B a) → (a : A) → C (f a)
f ∘ g = λ a → f (g a)
record Σ {A : Set} (B : A → Set) : Set where
constructor _,_
field
pr₁ : A
pr₂ : B pr₁
open Σ public
infixr 1 _×_ _,_
_×_ : Set → Set → Set
A × B = Σ \(_ : A) → B
data _+_ (A B : Set) : Set where
inl : A → A + B
inr : B → A + B
case : ∀{ℓ} {A B : Set} {C : Set ℓ}
→ (A → C) → (B → C) → A + B → C
case f g (inl a) = f a
case f g (inr b) = g b
data 𝟘 : Set where
𝟘-elim : {A : Set} → 𝟘 → A
𝟘-elim ()
¬ : Set → Set
¬ A = A → 𝟘
data 𝟙 : Set where
⋆ : 𝟙
\end{code}
■ Natural numbers
\begin{code}
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
rec : {A : Set} → A → (ℕ → A → A) → ℕ → A
rec a f 0 = a
rec a f (suc n) = f n (rec a f n)
ind : ∀ {ℓ} {P : ℕ → Set ℓ} → P 0 → (∀ n → P n → P (suc n)) → ∀ n → P n
ind p f 0 = p
ind p f (suc n) = f n (ind p f n)
not-zero-is-suc : {n : ℕ} → ¬ (n ≡ 0) → Σ \m → suc m ≡ n
not-zero-is-suc {0} f = 𝟘-elim (f refl)
not-zero-is-suc {suc n} f = n , refl
infix 5 _≤_ _<_ _≥_ _>_
data _≤_ : ℕ → ℕ → Set where
≤zero : {n : ℕ} → 0 ≤ n
≤suc : {n m : ℕ} → n ≤ m → suc n ≤ suc m
_<_ _≥_ _>_ : ℕ → ℕ → Set
n < m = suc n ≤ m
n ≥ m = m ≤ n
n > m = m < n
≤refl : {n : ℕ} → n ≤ n
≤refl {0} = ≤zero
≤refl {suc n} = ≤suc ≤refl
≤refl' : {n m : ℕ} → n ≡ m → n ≤ m
≤refl' refl = ≤refl
≤trans : {n m l : ℕ} → n ≤ m → m ≤ l → n ≤ l
≤trans ≤zero _ = ≤zero
≤trans (≤suc r) (≤suc s) = ≤suc (≤trans r s)
≤-cases : {n m : ℕ} → n ≤ m → (n ≡ m) + (n < m)
≤-cases {0} {0} ≤zero = inl refl
≤-cases {0} {suc m} ≤zero = inr (≤suc ≤zero)
≤-cases {suc n} {suc m} (≤suc r) with ≤-cases r
... | inl refl = inl refl
... | inr s = inr (≤suc s)
≤suc' : {n m : ℕ} → n ≤ m → n ≤ suc m
≤suc' ≤zero = ≤zero
≤suc' (≤suc r) = ≤suc (≤suc' r)
\end{code}
■ Infinite sequences
\begin{code}
_ᴺ : Set → Set
A ᴺ = ℕ → A
ℕᴺ : Set
ℕᴺ = ℕ ᴺ
0ʷ : ℕᴺ
0ʷ = λ i → 0
infixr 30 _✶_
_✶_ : {A : Set} → A → A ᴺ → A ᴺ
a ✶ u = rec a (λ i _ → u i)
head : {A : Set} → A ᴺ → A
head α = α 0
tail : {A : Set} → A ᴺ → A ᴺ
tail α i = α (suc i)
data _≡[_]_ {A : Set} : A ᴺ → ℕ → A ᴺ → Set where
≡[zero] : {α β : A ᴺ} → α ≡[ 0 ] β
≡[suc] : {α β : A ᴺ} {n : ℕ} → head α ≡ head β → tail α ≡[ n ] tail β → α ≡[ suc n ] β
≡[≤] : {A : Set} {α β : A ᴺ} {n m : ℕ}
→ α ≡[ n ] β → m ≤ n → α ≡[ m ] β
≡[≤] en ≤zero = ≡[zero]
≡[≤] (≡[suc] e en) (≤suc r) = ≡[suc] e (≡[≤] en r)
≡[]-< : {A : Set} {α β : A ᴺ} {n i : ℕ}
→ α ≡[ n ] β → suc i ≤ n → α i ≡ β i
≡[]-< (≡[suc] e en) (≤suc ≤zero) = e
≡[]-< (≡[suc] e en) (≤suc (≤suc r)) = ≡[]-< en (≤suc r)
≡[]-refl : {n : ℕ} {A : Set} {α : A ᴺ}
→ α ≡[ n ] α
≡[]-refl {0} = ≡[zero]
≡[]-refl {suc n} = ≡[suc] refl ≡[]-refl
\end{code}