------------------------------------------------------------------------ -- 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 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