-- Martin Escardo, 3rd August 2015, last updated 5th August 2015 {- A small type of propositions à la Voevodsky in Agda. (There is also a predicative version at http://www.cs.bham.ac.uk/~mhe/predicativity/) -} module index where {- We use type-in-type to get an experimental implementation of impredicativity à la Voevodsky (propositional resizing) in Agda. Only the tiny module prop.agda needs to use type-in-type. All the other modules work without it. Because of limitations of Agda, or perhaps of our ability to exploit Agda, we can only resize from the second universe U₁=Set₁ to the first universe U=Set₀. A difference of this kind of impredicativity with CoC's impredicativity is that the "axioms" of 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/impredicativity.zip This type checks in Agda 2.4.2.2 Click at a module name to navigate to it. -} {- A truth value is a type together with a witness that it is a proposition. The following module defines the type Prp:U of truth values in U, which amounts to impredicativity. It is the only rogue module that uses type-in-type to define Prp = Σ(P:U).isProp P so that Prp:U. -} open import prop {- NB. The option type-in-type is not inherited from prop.agda. For example, the following type checks with type-in-type, but fails to type check in this module, as it should: -} {- Fails to type check (good!): set : Set set = Set -} {- 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 Prp 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→Prp, (∃! p) = true → Σ(x:X).p(x)=true. -} open import description {- We then get quotients (incomplete for the moment): -} open import quotient