Lecture-2.agda

module Lecture-2 where

data ⊤ : Set where --\top
  tt : ⊤

data ⊥ : Set where --\bot

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = λ ()

implies₁ : ⊤ → ⊤
implies₁ x = x

implies₂ : ⊥ → ⊥
implies₂ x = x

implies₃ : ⊥ → ⊤
implies₃ x = ⊥-elim x

-- implies₄ : ⊤ → ⊥
-- implies₄ x = ?

proof₁ : {A : Set} → A → A
proof₁ a = a

-- !proof₁ : {A B : Set} → A → B
-- !proof₁ = ?

proof₂ : {A B : Set} → A → (B → B)
proof₂ _ = λ x → x

axiom₁ : {A B : Set} → A → (B → A)
axiom₁ a = λ _ → a

axiom₂ : {A B C : Set} → (A → B) → ((B → C) → (A → C))
axiom₂ f g h =  g (f h)

data _×_ (A : Set) (B : Set) : Set where --\x
    <_,_> : A → B → (A × B)

axiom₃ : {A B : Set} → A → (B → A × B)
axiom₃ a b = < a , b >

axiom₄ : {A B : Set} → (A × B) → A
axiom₄  < a , b > = a

axiom₅ : {A B : Set} → (A × B) → B
axiom₅  < a , b > = b


data _∣_ (A B : Set) : Set where --\|
   Left : A → A ∣ B
   Right : B → A ∣ B

axiom₆ : {A B : Set} → A → A ∣ B
axiom₆ = Left

axiom₇ : {A B : Set} → B → A ∣ B
axiom₇ = Right

axiom₈ : {A B C : Set} → (A → C) → ((B → C) → (A ∣ B → C))
axiom₈ f g (Left a) = f a
axiom₈ f g (Right b) = g b

¬ : Set → Set -- for ¬ type \neg
¬ A = A → ⊥

axiom₉ : {A B : Set} → (A → B) → ((A → ¬ B) → ¬ A)
axiom₉ f g h = g h (f h)
-- (A → B) → (A → B → ⊥) → A → ⊥

axiom₁₀ : {A B : Set} → ¬ A → (A → B)
axiom₁₀ f a = ⊥-elim (f a)
-- (A → ⊥) → A → B

axiom₁₁ : {A : Set}{P : A → Set} →
          (∀ (a : A) → P a) → (a₁ : A) → P a₁
axiom₁₁ f = f

data Σ (A : Set) (P : A → Set) : Set where
 ⟨_,_⟩ : (a : A) → P a → Σ A P --\< \>

∃ : (A : Set) → (P : A → Set) → Set
∃ A P = Σ A P

axiom₁₂ : (A : Set) → (P : A → Set) → Set
axiom₁₂ = ∃