Supplementary artefacts for TYPES 2023. Typechecked using Agda 2.6.3 and Cubical v0.5. Written by Stefania Damato & Thorsten Altenkirch.
-
Containers.agda: Definition of generalised containers, the category
$\underline{\mathbf{Cont}}$ of generalised containers, and the container extension functor ⟦_⟧ mapping generalised containers to functors. -
ContainersProofs.agda: 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
$\underline{\mathbf{C}}$ and give rise to functors of type$\underline{\mathbf{C}} \to \underline{\mathbf{Set}}$ . - InductiveContainers.agda: (WIP) Formalisation of the proofs that ordinary container functors are closed under fixed points, i.e. container functors are closed under initial algebras and terminal coalgebras. Proofs taken from Containers: Constructing strictly positive types.
- IndexedGeneralised.agda: Proof that indexed containers are a special case of generalised containers.
An HTML rendering of this code can be found here.