Documentation

>>> runLoud $ spec_ (MartinLof 0) >> evenOrOddScript
-- 1. double
------------
--
λ» :define succ : ℕ → ℕ = λ n → S n
λ» :define double
: ℕ → ℕ = λ n → ℕ-elim (λ _ → ℕ) 0 (λ _ m → succ (succ m)) n
--
λ» :example double 0
↪ 0 : ℕ
--
λ» :example double 1
↪ 2 : ℕ
--
λ» :example double 5
↪ 10 : ℕ
--
-- 2. Even
----------
--
λ» :define Even
: ℕ → 𝓤 = λ n → ∑ (m : ℕ) → Eq ℕ n (double m)
λ» :define zero-is-even : Even 0 = pair 0 refl
--
λ» :example pair 1 refl : Even 2
↪ pair 1 refl
: ∑ (m : ℕ) →
  Eq ℕ 2 (ℕ-elim (λ _ → ℕ) 0 (λ _ m → S (S m)) m)
--
-- 3. Odd
---------
--
λ» :define Odd
: ℕ → 𝓤 = λ n → ∑ (m : ℕ) → Eq ℕ n (S (double m))
--
λ» :example pair 3 refl : Odd 7
↪ pair 3 refl
: ∑ (m : ℕ) →
  Eq ℕ 7 (S (ℕ-elim (λ _ → ℕ) 0 (λ _ m → S (S m)) m))
--
-- 4. Congruence
----------------
--
λ» :define congruence
: ∀ A →
  ∀ B →
  ∏ (f : (A → B)) →
  ∏ (x : A) →
  ∏ (y : A) →
  Eq A x y →
  Eq B (f x) (f y)
= λ A B f x y p →
      J A (λ u v _ → Eq B (f u) (f v)) (λ _ → refl) x y p
--
-- 5. Succ Even is Odd
----------------------
--
λ» :define succ-even-is-odd
: ∏ (n : ℕ) → Even n → Odd (S n)
= λ n even-n →
      match even-n
            (λ m proof →
                 pair m (congruence
                             ℕ ℕ succ n (double m) proof))
λ» :define succ-odd-is-even
: ∏ (n : ℕ) → Odd n → Even (S n)
= λ n odd-n →
      match
          odd-n
          (λ m proof →
               pair
                   (succ m)
                   (congruence
                        ℕ ℕ succ n (succ (double m)) proof))
--
-- 6. Boolean
-------------
--
λ» :define if₁ : ∏ (r : 𝓤₁) → 𝔹 → r → r → r
               = λ r b t f → 𝔹-elim (λ _ → r) t f b
--
-- 7. Either
------------
--
-- 7.1. Type
--
λ» :define Either
: 𝓤 → 𝓤 → 𝓤 = λ A B → ∑ (t : 𝔹) → if₁ 𝓤 t A B
--
-- 7.2. Constructors
--
λ» :define left : ∀ A → ∀ B → A → Either A B
                = λ A B x → pair true x
λ» :define right : ∀ A → ∀ B → B → Either A B
                 = λ A B y → pair false y
--
-- 7.3. Non-dependent elimination
--
λ» :define either
: ∀ A → ∀ B → ∀ C → (A → C) → (B → C) → Either A B → C
= λ A B C f g e →
      match e (λ t v → (𝔹-elim (λ t₁ → if₁ 𝓤 t₁ A B → C)
                               (λ x → f x)
                               (λ y → g y)
                               t)
                           v)
--
-- 8. All number are either even or odd
---------------------------------------
--
λ» :define theorem
: ∏ (n : ℕ) → Either (Even n) (Odd n)
= λ n →
      ℕ-elim
          (λ m → Either (Even m) (Odd m))
          (pair true zero-is-even)
          (λ l H →
               either
                   (Even l)
                   (Odd l)
                   (Either (Even (succ l)) (Odd (succ l)))
                   (λ p → pair false (succ-even-is-odd l p))
                   (λ p → pair true (succ-odd-is-even l p))
                   H)
          n
--
λ» :example theorem 0
↪ pair true (pair 0 refl)
: ∑ (t : 𝔹) →
  𝔹-elim
      (λ _ → 𝓤)
      (∑ (m : ℕ) →
       Eq ℕ 0 (ℕ-elim (λ _ → ℕ) 0 (λ _ m → S (S m)) m))
      (∑ (m : ℕ) →
       Eq ℕ 0 (S (ℕ-elim (λ _ → ℕ) 0 (λ _ m → S (S m)) m)))
      t
--
λ» :example theorem 100
↪ pair true (pair 50 refl)
: ∑ (t : 𝔹) →
  𝔹-elim
      (λ _ → 𝓤)
      (∑ (m : ℕ) →
       Eq ℕ 100 (ℕ-elim (λ _ → ℕ) 0 (λ _ m → S (S m)) m))
      (∑ (m : ℕ) →
       Eq ℕ 100 (S (ℕ-elim
                        (λ _ → ℕ) 0 (λ _ m → S (S m)) m)))
      t
--
λ» :example theorem 113
↪ pair false (pair 56 refl)
: ∑ (t : 𝔹) →
  𝔹-elim
      (λ _ → 𝓤)
      (∑ (m : ℕ) →
       Eq ℕ 113 (ℕ-elim (λ _ → ℕ) 0 (λ _ m → S (S m)) m))
      (∑ (m : ℕ) →
       Eq ℕ 113 (S (ℕ-elim
                        (λ _ → ℕ) 0 (λ _ m → S (S m)) m)))
      t
∎