Documentation

>>> runLoud $ spec_ (MartinLof 0) >> eitherScript
-- If we have Booleans and dependent pair, we can make Either
--
-- 1. Boolean prelude
---------------------
--
λ» :define if : ∀ r → 𝔹 → r → r → r
              = λ r b t f → 𝔹-elim (λ _ → r) t f b
--
-- We a need variant in higher universe too
λ» :define if₁ : ∏ (r : 𝓤₁) → 𝔹 → r → r → r
               = λ r b t f → 𝔹-elim (λ _ → r) t f b
--
-- 2. Type
----------
--
λ» :define Either
: 𝓤 → 𝓤 → 𝓤 = λ A B → ∑ (t : 𝔹) → if₁ 𝓤 t A B
--
-- 2.1. Example
--
λ» :define A = Either 𝔹 ℕ
--
λ» :example A
↪ ∑ (t : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ t : 𝓤
--
-- 3. 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
--
-- 3.1. Examples
--
λ» :define x : A = left 𝔹 ℕ true
λ» :define y : A = left 𝔹 ℕ false
λ» :define u : A = right 𝔹 ℕ 1
λ» :define v : A = right 𝔹 ℕ 2
--
λ» :example x
↪ pair true true : ∑ (t : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ t
--
λ» :example y
↪ pair true false : ∑ (t : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ t
--
λ» :example u
↪ pair false 1 : ∑ (t : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ t
--
λ» :example v
↪ pair false 2 : ∑ (t : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ t
--
-- 4. 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)
--
-- 4.1. Example
--
λ» :define boolToNat : 𝔹 → ℕ = λ b → if ℕ b 0 1
λ» :define toNat
: A → ℕ = either 𝔹 ℕ ℕ boolToNat (λ n → S n)
--
λ» :example toNat x
↪ 0 : ℕ
--
λ» :example toNat y
↪ 1 : ℕ
--
λ» :example toNat u
↪ 2 : ℕ
--
λ» :example toNat v
↪ 3 : ℕ
--
-- 5. Reduction
---------------
--
-- Note how much type annotations we don't have to write in Haskell
λ» :define redex₁
: ∀ A → ∀ B → ∀ C → (A → C) → (B → C) → A → C
= λ A B C f g x → either A B C f g (left A B x)
--
-- it reduces!
λ» :example redex₁
↪ λ A B C f g x → f x
: ∀ A → ∀ B → ∀ C → (A → C) → (B → C) → A → C
--
λ» :define redex₂
: ∀ A → ∀ B → ∀ C → (A → C) → (B → C) → B → C
= λ A B C f g y → either A B C f g (right A B y)
--
λ» :example redex₂
↪ λ A B C f g y → g y
: ∀ A → ∀ B → ∀ C → (A → C) → (B → C) → B → C
∎

>>> runLoud $ spec_ (MartinLof 0) >> pairScript
-- Non dependent pair
--
-- 1. Type
----------
--
λ» :define Pair : 𝓤 → 𝓤 → 𝓤 = λ A B → ∑ (_ : A) → B
--
-- 2. Constructor
-----------------
--
λ» :define mkPair : ∀ A → ∀ B → A → B → Pair A B
                  = λ A B x y → pair x y
--
-- 3. Projections
-----------------
--
λ» :define fst : ∀ A → ∀ B → Pair A B → A
               = λ A B p → match p (λ x y → x)
λ» :define snd : ∀ A → ∀ B → Pair A B → B
               = λ A B p → match p (λ x y → y)
--
-- 4. Reduction
---------------
--
λ» :define redex₁ : ∀ A → ∀ B → A → B → A
                  = λ A B x y → fst A B (mkPair A B x y)
--
λ» :example redex₁
↪ λ A B x y → x : ∀ A → ∀ B → A → B → A
--
λ» :define redex₂ : ∀ A → ∀ B → A → B → B
                  = λ A B x y → snd A B (mkPair A B x y)
--
λ» :example redex₂
↪ λ A B x y → y : ∀ A → ∀ B → A → B → B
∎