This PR adds some definitions and proofs on containers. As a prerequisite, it also required adding (non-indexed) W-types and M-types written as a record type.
More specifically,
we define the category of generalised containers,
we define the container extension functor,
we give two different presentations of the proof that the container extension functor is full and faithful,
and we give proofs that set-containers are closed under least and greatest fixed points.
Most of the proofs are an adaptation of those in 'Containers: Constructing strictly positive types' by Abbott, Altenkirch, and Ghani.
I am aware of the -W[no]NoGuardednessFlag warning being raised. This warning is raised because MRecord.agda is not tagged with a --guardedness flag. I avoided this tag as I import MRecord.agda from Algebras.agda, which exists in the Data directory, and which therefore causes an error if it is also tagged with --guardedness. I'd be happy to refactor if reviewers have suggestions on how else I can organise things.
This PR adds some definitions and proofs on containers. As a prerequisite, it also required adding (non-indexed) W-types and M-types written as a record type.
More specifically,
Most of the proofs are an adaptation of those in 'Containers: Constructing strictly positive types' by Abbott, Altenkirch, and Ghani.
I am aware of the
-W[no]NoGuardednessFlagwarning being raised. This warning is raised because MRecord.agda is not tagged with a--guardednessflag. I avoided this tag as I import MRecord.agda from Algebras.agda, which exists in the Data directory, and which therefore causes an error if it is also tagged with--guardedness. I'd be happy to refactor if reviewers have suggestions on how else I can organise things.