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