------------------------------------------------------------------------
-- The Agda standard library
--
-- An explanation about the `Axiom` modules.
------------------------------------------------------------------------

module README.Axiom where

open import Level using (Level)

private variable ℓ : Level

------------------------------------------------------------------------
-- Introduction

-- Several rules that are used without thought in written mathematics
-- cannot be proved in Agda. The modules in the `Axiom` folder
-- provide types expressing some of these rules that users may want to
-- use even when they're not provable in Agda.

------------------------------------------------------------------------
-- Example: law of excluded middle

-- In classical logic the law of excluded middle states that for any
-- proposition `P` either `P` or `¬P` must hold. This is impossible
-- to prove in Agda because Agda is a constructive system and so any
-- proof of the excluded middle would have to build a term of either
-- type `P` or `¬P`. This is clearly impossible without any knowledge
-- of what proposition `P` is.

-- The types for which `P` or `¬P` holds is called `Dec P` in the
-- standard library (short for `Decidable`).

open import Relation.Nullary.Decidable using (Dec)

-- The type of the proof of saying that excluded middle holds for
-- all types at universe level ℓ is therefore:
--
--   ExcludedMiddle ℓ = ∀ {P : Set ℓ} → Dec P
--
-- and this type is exactly the one found in `Axiom.ExcludedMiddle`:

open import Axiom.ExcludedMiddle

-- There are two different ways that the axiom can be introduced into
-- your Agda development. The first option is to postulate it:

postulate excludedMiddle : ExcludedMiddle ℓ

-- This has the advantage that it only needs to be postulated once
-- and it can then be imported into many different modules as with any
-- other proof. The downside is that the resulting Agda code will no
-- longer type check under the --safe flag.

-- The second approach is to pass it as a module parameter:

module Proof (excludedMiddle : ExcludedMiddle ℓ) where

-- The advantage of this approach is that the resulting Agda
-- development can still be type checked under the --safe flag.
-- Intuitively the reason for this is that when postulating it
-- you are telling Agda that excluded middle does hold (which is clearly
-- untrue as discussed above). In contrast when passing it as a module
-- parameter you are telling Agda that **if** excluded middle was true
-- then the following proofs would hold, which is logically valid.

-- The disadvantage of this approach is that it is now necessary to
-- include the excluded middle assumption as a parameter in every module
-- that you want to use it in. Additionally the modules can never
-- be fully instantiated (without postulating excluded middle).

------------------------------------------------------------------------
-- Other axioms

-- Double negation elimination
--   (∀ P → ¬ ¬ P → P)

import Axiom.DoubleNegationElimination

-- Function extensionality
--   (∀ f g → (∀ x → f x ≡ g x) → f ≡ g)

import Axiom.Extensionality.Propositional
import Axiom.Extensionality.Heterogeneous

-- Uniqueness of identity proofs (UIP)
--  (∀ x y (p q : x ≡ y) → p ≡ q)

import Axiom.UniquenessOfIdentityProofs