{-# OPTIONS --prop --rewriting #-}

-- This development has been tested to typecheck with Agda version 2.8.0-08923ce
-- The typechecking gets a bit slow, expect a few minutes on a high end laptop

module readme where

-- Tools and postulates (funext, etc)
import lib

-- Definition of a CwF with dependent products and booleans (incl. large elimination)
import model

-- Definition of CwF morphisms
import morphism

-- Definition of dependent CwFs, and pulling them back along morphisms
import depModel

-- Initial CwF ("syntax") with its elimination principles
import initialObs

-- Strictification of the substitution associativity and unit laws of a CwF
-- + definition of a morphism from the strictified CwF to the original CwF
import strictifyCat
import strictifyCatMorphism

-- Strictification of most administrative equations using Pédrot's strict preshaves
-- + definition of a morphism from the strictified CwF to the contextual core of the original CwF
import strictifyPMP
import strictifyPMPMorphism

-- Proving that the strictification morphisms are in fact isomorphisms
import strictifyIso

-- strictification of the initial model using strict presheaves. it
-- includes dependent model over the strict initial model and its
-- induction principle
import initialStrict

-- some tests for definitional equalities in the strict syntax
import test

-- a canonicity proof
import canon