{-
Agda code accompanying the paper

   A. M. Pitts and S. C. Steenkamp,
   "Constructing Initial Algebras Using Inflationary Iteration"
   In K. Kishida (ed), Fourth International Conference on Applied
   Category Theory (ACT 2021), EPTCS Vol ?, 2021

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

Source code: https://dx.doi.org/10.17863/CAM.73911

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