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