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