-- Agda development of Positive inductive-recursive definitions

-- The development is structured as follows:

-- 1. Basic definitions ----------------

-- Definition of Fam C
import Prelude
-- Isos in Fam C
import Prelude.Isos
-- Lemmas dealing with equality not in the standard library
import Prelude.Equality

-- 2. IR+ and basic properties ---------

-- Definition of IR codes and morphisms, and their decoding
import posIR

-- Proof that IR+ forms a category
import Category

-- Introduction rules for IR+ definitions (using Agda's support for
-- mutual definitions)
import Intro

-- 3. Constructions for IR+ codes ------

-- Simple basic constructions
import Constructions

-- A code that decodes to the binary coproduct of the decoding of given codes
import Constructions.Coproduct

-- A code that decodes to the binary product of the decoding of given codes
import Constructions.Product

-- 4. Examples -------------------------

-- Universes closed under Σ and Π in different categories respectively
import Examples.Universes

-- Normal form universes:

---- First for ×
import Examples.NF.Prod

---- Then for Σ
import Examples.NF.Sigma

-- Nested types are containers
import Examples.NestedTypes

-- In particular, lambda terms via nested types and positive IR
import Examples.Lam

-- 5. Uniform positive IR --------------

-- The last example requires uniform codes, which we define here

-- Definition of uniform codes, their decoding and translation to ordinary codes
import Uniform.posIR

-- Again, uniform codes form a category
import Uniform.Category

-- And we can define the introduction rules for uniform definitions
import Uniform.Intro

-- Constructions on uniform codes:

---- same as before
import Uniform.Constructions
import Uniform.Constructions.Product
import Uniform.Constructions.Coproduct

---- but we can also construct a kind of dependent product of codes (in Set^op)
import Uniform.Constructions.Pi

-- The coproduct requires us to develop some extra machinery
import Uniform.EnvBool
import Uniform.Shape