Documentation

>>> runLoud $ spec_ (MartinLof 0) >> equalityScript
-- 1. Non-dependent elimination: if
-----------------------------------
--
λ» :define if : ∀ r → 𝔹 → r → r → r
              = λ r b t f → 𝔹-elim (λ _ → r) t f b
--
-- 2. Negation, not
-------------------
--
λ» :define not : 𝔹 → 𝔹 = λ b → if 𝔹 b false true
--
λ» :example not
↪ λ b → 𝔹-elim (λ _ → 𝔹) false true b : 𝔹 → 𝔹
--
λ» :example not true
↪ false : 𝔹
--
λ» :example not false
↪ true : 𝔹
--
-- 3. Simple equality examples
------------------------------
--
λ» :example refl : Eq 𝔹 (not true) false
↪ refl : Eq 𝔹 false false
--
λ» :example refl : Eq 𝔹 (not false) true
↪ refl : Eq 𝔹 true true
--
-- 4. Lemma: Not is involutive
------------------------------
--
λ» :define not-inv
: ∏ (b : 𝔹) → Eq 𝔹 b (not (not b))
= λ b → 𝔹-elim (λ x → Eq 𝔹 x (not (not x))) refl refl b
--
-- 5. Example with exists
-------------------------
--
λ» :define not-surj
: ∏ (x : 𝔹) → ∑ (y : 𝔹) → Eq 𝔹 x (not y)
= λ x → 𝔹-elim (λ b → ∑ (y : 𝔹) → Eq 𝔹 b (not y))
               (pair false refl)
               (pair true refl)
               x
∎

OPLSS 2014 Type Theory

>>> runLoud $ spec_ (MartinLof 0) >> equivalenceScript
-- 1. Symmetry
--------------
--
λ» :define SYM
: 𝓤 → 𝓤 = λ A → ∏ (x : A) → ∏ (y : A) → Eq A x y → Eq A y x
λ» :define sym
: ∀ A → SYM A
= λ A x y p → J A (λ u v w → Eq A v u) (λ q → refl) x y p
--
-- 1.1. Example
--
λ» :define nat-fold
: ∀ r → ℕ → (r → r) → r → r
= λ r n s z → ℕ-elim (λ _ → r) z (λ l → s) n
λ» :define succ : ℕ → ℕ = λ n → S n
λ» :define plus : ℕ → ℕ → ℕ = λ x y → nat-fold ℕ x succ y
--
λ» :example refl : Eq ℕ (plus 3 1) (plus 1 3)
↪ refl : Eq ℕ 4 4
--
λ» :example sym ℕ (plus 3 1) (plus 1 3) refl
↪ refl : Eq ℕ 4 4
--
-- 2. Transitivity
------------------
--
λ» :define TRANS : 𝓤 → 𝓤 = λ A → ∏ (x : A) →
                                 ∏ (y : A) →
                                 ∏ (z : A) →
                                 Eq A x y →
                                 Eq A y z →
                                 Eq A x z
λ» :define trans
: ∀ A → TRANS A
= λ A x y z p →
      J A (λ u v w → Eq A v z → Eq A u z) (λ _ r → r) x y p
--
λ» :example trans ℕ (plus 1 3) (plus 2 2) (plus 3 1) refl
↪ λ r → r : Eq ℕ 4 4 → Eq ℕ 4 4
∎

>>> runLoud $ spec_ CoCStar >> leibnizScript
-- 1. Leibniz
-------------
--
-- We can define Leibniz equality
-- in the systems with impredicative bottom universe.
-- TODO: define CComega, and make conversions
λ» :define Leibniz
: ∀ A → A → A → ⋆ = λ A x y → ∏ (C : (A → ⋆)) → C x → C y
--
-- 1.1. Reflexivity
--
λ» :define REFL : ⋆ → ⋆ = λ A → ∏ (x : A) → Leibniz A x x
λ» :define refl₁ : ∀ A → REFL A = λ A x C Cx → Cx
--
-- 1.2. Symmetry
--
λ» :define SYM : ⋆ → ⋆ = λ A → ∏ (x : A) →
                               ∏ (y : A) →
                               Leibniz A x y →
                               Leibniz A y x
λ» :define sym
: ∀ A → SYM A = λ A x y xy → xy (λ z → Leibniz A z x)
                                (refl₁ A x)
--
-- 1.3. Transitivity
--
-- An exercise!
∎

>>> runLoud $ spec_ (MartinLof 0) >> inequalityScript
-- Proving inequalities is difficult!
λ» :define if₁ : ∏ (r : 𝓤₁) → 𝔹 → r → r → r
               = λ r b t f → 𝔹-elim (λ _ → r) t f b
--
-- Important thing is to find proper motive for induction
λ» :define motive
: 𝔹 → 𝔹 → 𝓤 = λ u v → if₁ 𝓤 u (if₁ 𝓤 v ⊤ ⊥) ⊤
--
-- With proper motive, proof is almost trivial
λ» :define true-is-not-false
: Eq 𝔹 true false → ⊥
= λ p → J 𝔹
          (λ u v w → motive u v)
          (λ b → 𝔹-elim (λ c → motive c c) I I b)
          true
          false
          p
--
λ» :example true-is-not-false
↪ λ p →
      J 𝔹
        (λ u v w →
             𝔹-elim (λ _ → 𝓤) (𝔹-elim (λ _ → 𝓤) ⊤ ⊥ v) ⊤ u)
        (λ b → 𝔹-elim (λ c → 𝔹-elim (λ _ → 𝓤)
                                    (𝔹-elim (λ _ → 𝓤) ⊤ ⊥ c)
                                    ⊤
                                    c)
                      I
                      I
                      b)
        true
        false
        p
: Eq 𝔹 true false → ⊥
∎