module Index where

-- The source code can also be downloaded as a zip file
-- https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/variantsIR/variantsIR.zip

-- 0. Basic background definitions

import Prelude.Basic        -- Standard type formers
import Prelude.Equality     -- The identity type, and lemmas about it
import Prelude.Container    -- Containers
import Prelude.Fam          -- The type (category) of families of things
import Prelude.Equivalences -- Isomorphisms in Fam D

{----- 1. Dybjer-Setzer codes --------------------------------------------}

import DS.IR                    -- Basic definition of Dybjer-Setzer
                                -- codes and their decoding

import DS.Initial               -- Formation, introduction and
                                -- elimination rules
import DS.InitialPleasingAgda   -- Same as above, but without
                                -- bypassing Agda's checks

import DS.Bind                  -- Proof that DS-bind decodes to Fam-bind
import DS.compositionFromPower  -- Composition in terms of bind and an
                                -- assumed power operation

import DS.powerFromComposition  -- Conversely powers in terms of an
                                -- assumed composition

-- Alternative versions of Dybjer-Setzer codes:

import DS.Arg                   -- Dybjer and Setzer's original 1999 system
import DS.SigmaDelta            -- A system with σ and δ merged into on code σδ
import DS.DSPi                  -- DS.Arg with a π-code added

{----- 2. Uniform IR -----------------------------------------------------}

import Uniform.IR                  -- Basic definition of uniform IR
                                   -- codes and their decoding

import Uniform.Initial             -- Formation, introduction and
                                   -- elimination rules
import Uniform.InitialPleasingAgda -- same, not bypassing Agda's
                                   -- checks

import Uniform.Examples            -- Examples of uniform codes

import Uniform.AppLift             -- The combined bind and power
                                   -- operation _++[_⟶_] and its
                                   -- properties

import Uniform.Composition         -- Composition of uniform codes

import Uniform.EmbeddingIntoDS     -- Embedding uniform codes into DS


import Uniform.Coproduct           -- Coproducts of uniform codes
import Uniform.Coproduct.Maps      -- Proof that coproducts are coproducts



{----- 3. Polynomial IR --------------------------------------------------}

import Polynomial.IR                   -- Basic definition of Polynomial codes,
                                       -- and their decoding

import Polynomial.Initial              -- Formation, introduction and
                                       -- elimination rules
import Polynomial.InitialPleasingAgda  -- same, not bypassing Agda's checks

import Polynomial.Composition          -- Composition of Polynomial codes

import Polynomial.EmbeddingFromDS      -- Embedding DS codes into Polynomial codes

-- A container variation of Polynomial codes

import Polynomial.Container.IR          -- Basic definition and decoding
import Polynomial.Container.Equivalence -- Maps back and forth to ordinary
                                        -- Polynomial codes
import Polynomial.Container.Composition -- Composition directly for
                                        -- container polynomial codes

{-------------------------------------------------------------------------}

-- (the directory Misc contains experiments and work in  progress)