{-
Agda code accompanying the paper

   A. M. Pitts and S. C. Steenkamp,
   "Constructing Initial Algebras Using Inflationary Iteration"
   (https://arxiv.org/abs/2105.03252)

Checked with Agda Version 2.6.2

The development makes use of Axiom K, Aga's universes of
proof-irrelevant propositions, and its facility to declare rewrites.

Global flags set in agda.agda-lib:
  --prop --rewriting --confluence-check --show-irrelevant --with-K

-}
module index where

-- The development does not depend on Agda's Standard Library.
-- Instead, following file contains some common definitions.
import Prelude

-- Section 1. Introduction
import InitialAlgebra

-- Section 2. Constructive meta-theory
{- Axioms used:
  Propositional Extensionailty
  Quotient Types with definitional computation rule
  Function Extensionality (derived from quotient types)
  Axiom of Unique Choice
  (The WISC axiom is introduced later.)
-}
import Axioms

-- Section 3. Size indexed inflationary iteration
import ThinSemiCategory -- Definition 3.1
import WellFoundedRelations
import Size -- Definition 3.2
import Colimit
import InflationaryIteration -- Lemma 3.6
import InitialAlgebraViaInflationaryIteration -- Theorem 3.8

-- Section 4. Initial algebras for sized endofunctors
import AlgebraicSignature
import SizedFunctor -- Theorem 4.4
import WISC -- the WISC Axiom
import Sets -- colimits in the category of Sets
import ProductsofSizedFunctors -- Theorem 4.13