{- A small type of propositions à la Voevodsky in Agda --------------------------------------------------- Martin Escardo 3rd August 2015, last updated 5th August 2015, 9 May 2016. Based on Vladimir Voevodsky's Plenary Talk "Resizing rules" at the Types meeting in 11th September 2011 in Bergen. https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf Abstract -------- We apply Jesper Cockx and Andreas Abel's rewriting feature for Agda, "Sprinkles of extensionality for your vanilla type theory" Types 2016, Novi Sad, Serbia, 23-26 May 2016. http://www.types2016.uns.ac.rs/index.php/programme-2/conf-prog (A previous version uses the option --type-in-type confined to one module only instead: http://www.cs.bham.ac.uk/~mhe/impredicativity/) Here only the module prop.agda needs to define rewriting rules for resizing. However, in the current version of Agda, 2.5.2, modules that use that module have to use the option --rewriting. A difference of this kind of impredicativity with CoC's impredicativity is that unique choice and description hold. Our truth values are types with at most one element, and yet they are proof relevant in some sense. zip file with agda source available at http://www.cs.bham.ac.uk/~mhe/impredicativity-via-rewriting/impredicativity.zip This type checks in Agda 2.5.2. Click at a module name to navigate to it. -} module index where -- The following module defines the type Prop:U₀ of propositions -- in the first universe U₀, which amounts to impredicativity. -- It is the only rogue module that uses --rewriting to define -- -- Prop = Σ(P:U₀).isProp P -- -- so that Prop:U₀ rather than U₁. open import prop -- The type of propositions is a set, assuming functional and -- propositional extensionality: open import propisset -- Using impredicativity, we can define propositional truncation by -- universal quantification over truth values (as Voevodsky does): open import proptrunc -- We then develop some amount of logic in the type Prop of -- propositions, where we define the logical connectives and their -- introduction and elimination rules following the ideas of the HoTT -- book. We then prove that -- -- false = ∀ r. r -- p ∧ q = ∀ r. (p ⇒ q ⇒ r) ⇒ r -- p ∨ q = ∀ r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r -- ∃ p = ∀ r. (∀ x. p(x) ⇒ r) ⇒ r open import logic -- We then prove the axiom of description: for any set X and any -- p:X→Prop, -- -- (∃!(x:X).p(x))=true → Σ(x:X).p(x)=true. open import description -- We then get quotients (incomplete for the moment): open import quotient