```module Logic where

-- The universe of propositions is denoted by Ω. By the Curry-Howard
-- isomorphism, it is the universe of types, sometimes called Sets in
-- Agda.

Ω = Set

-- False:

data ⊥ : Ω where
-- nothing defined here: there are no constructors of this type.

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

¬_ : Ω → Ω
¬ A = (A → ⊥)

infix  50 ¬_

-- True, with proof ⋆:

data ⊤ : Ω where
* : ⊤

data _∧_ (A₀ A₁ : Ω) : Ω where
∧-intro : A₀ → A₁ → A₀ ∧ A₁

infixr 10 _∧_

∧-elim₀ : {A₀ A₁ : Ω} →
-------------
A₀ ∧ A₁ → A₀
-------------
∧-elim₀ (∧-intro a₀ a₁) = a₀

∧-elim₁ : {A₀ A₁ : Ω} →
-------------
A₀ ∧ A₁ → A₁
-------------
∧-elim₁ (∧-intro a₀ a₁) = a₁

data _∨_ (A₀ A₁ : Ω) : Ω where
∨-intro₀ : A₀ → A₀ ∨ A₁
∨-intro₁ : A₁ → A₀ ∨ A₁

infixr 20 _∨_

∨-elim : {A₀ A₁ B : Ω} →
----------------------------------
(A₀ → B) → (A₁ → B) → A₀ ∨ A₁ → B
----------------------------------
∨-elim f₀ f₁ (∨-intro₀ a₀) = f₀ a₀
∨-elim f₀ f₁ (∨-intro₁ a₁) = f₁ a₁

data ∃ {X : Set} (A : X → Ω) : Ω where
∃-intro : (x₀ : X) → A x₀ → ∃ \(x : X) → A x

∃-witness : {X : Set} {A : X → Ω} →
------------------------
(∃ \(x : X) → A x) → X
------------------------

∃-witness (∃-intro x a) = x

∃-elim : {X : Set} {A : X → Ω} →
--------------------------------------------------
(proof : ∃ \(x : X) → A x) → A (∃-witness proof)
--------------------------------------------------
∃-elim (∃-intro x a) = a

-- Some basic logical facts:

_∘_ : {A B : Ω} {C : B → Ω} →
----------------------------------------------------
(∀(b : B) → C b) → ∀(f : A → B) → ∀(a : A) → C(f a)
----------------------------------------------------
g ∘ f = λ x → g(f x)

infixl 30 _∘_

id : {A : Ω} →
------
A → A
------
id x = x

-- The following is usually used with R=⊥:

contra-positive : {R A B : Ω} →
----------------------------
(A → B) → (B → R) → (A → R)
----------------------------
contra-positive f p = p ∘ f
```