A partially formalised proof of the canonical-form theorem for the dependent type theory of the regular categories. The formalisation is built on top of the General Type Theories framework.
It is recommended to use the opam package manager to install the environment. Details about installing Opam can be found here.
- Install Coq
$ opam install coq
- Add the released coq-archive packages:
$ opam repo add coq-released https://coq.inria.fr/opam/released
- Install Coq-HoTT
$ opam install coq-hott
- Generate a makefile from _CoqProject with
$ coq_makefile -f _CoqProject -o CoqMakefile
- Compile the project with
$ make -f CoqMakefile
- Use CoqIDE (shipped with Coq), VSCoq or ProofGeneral
DependentTypeTheory.v contains the definition of the type theory of regular categories: signature, types and logical rules.
Computability.v contains the computation rules, the definition of computable judgement and proofs of preservation of computability for (some) logical rules in case of empty context.