-- Martin Escardo, 7th August 2015.

{-
   This is a predicative version of
   http://www.cs.bham.ac.uk/~mhe/impredicativity/
   that doesn't use type-in-type.

   http://www.cs.bham.ac.uk/~mhe/predicativity/predicativity.zip
-}

module index where

open import prop
open import propisset
open import proptrunc
open import logic
open import description
open import quotient