module README where
{-
  Agda code to accompany the paper:

  Marcelo P. Fiore, Andrew M. Pitts and S. C. Steenkamp,
  "Quotients, Inductive Types and Quotient Inductive Types",
  LMCS 18(2:15)2022,
  https://doi.org/10.46298/lmcs-18(2:15)2022

  Agda code at https://doi.org/10.17863/CAM.77483

  The code has been checked with Agda version 2.6.2.1

  The files use a common set of options given in the file flags.agda-lib:

  --with-K
    (we make use of Streicher's Axiom K, or equivalently the
    Uniqueness of Identity Proofs (UIP), via the more liberal, dafault
    version of Agda's dependent patern matching)

  --prop
    (we make use of Agda’s built-in predicative universes of
    definitionally proof-irrelevant propositions)

  --rewriting
    (we use Agda's facility for user-defined extensions of its
    evaluation relation with new computation rules, in order to make
    the computation rules for postulated quotient types be
    definitional equalities)

  We begin with a small library of common definitions:
-}
open import Prelude
{-
  Next we give some postulates for propositional extensionaliy,
  Hofmann-style quotient types and the axiom of unique choice, as
  described in section 2 (Type Theory) of the paper:
-}
open import TypeTheory
{-
  We also rely on some standard facts about well-founded induction and
  recursion (deriving the latter from the former via a use of Unique
  Choice -- see Proposition 5.3 in the paper):
-}
open import WellFoundedRelations
{-
  We make use of (an indexed version of) the Weakly Initial Set of
  Covers (WISC) Axiom, as discussed in section 4 of the paper:
-}
open import WeaklyInitialSetsOfCovers
{-
  Now there are two branches: QW and QWI

    The QW branch treats the construction of QW-types, as described in
    the paper.
-}
open import QW
{-
    The QWI branch generalises the construction to the case of the
    indexed version of QW-types, the QWI-types described in section 3.3
    of the paper.
-}
open import QWI