{-# OPTIONS  --cubical --guardedness --allow-unsolved-metas #-}

module README where

-- Definition of generalised containers, the category Cont of generalised containers,
-- and the container extension functor ⟦_⟧ mapping generalised containers to functors.
import Containers

-- Two proofs of the central result that the container extension functor ⟦_⟧ is full
-- and faithful. One follows the proof given in Containers: Constructing strictly
-- positive types, and the other is a new presentation of the previous proof that
-- makes explicit the use of the Yoneda lemma. We have proved this result for the
-- case of generalised containers, which are parameterised by an arbitrary category
-- and give rise to functors of type C → Set.
import ContainersProofs

-- (Work in progress) Formalisation of the proofs that ordinary container functors
-- are closed under fixed points, i.e. fixed points of container functors are
-- themselves container functors. Proofs taken from Containers: Constructing strictly
-- positive types.
import InductiveContainers

-- Proof that indexed containers are a special case of generalised containers.
import IndexedGeneralised