783 B
783 B
This folder contains a formalization of various properties about sequential colimits. Most importantly, we prove that sigma-types commute with colimits. It accompanies a submitted paper by Kristina Sojakova, Floris van Doorn and Egbert Rijke.
This repository contains some unproven results, marked by sorry. No unproven results are used for any theorems discussed in the paper. You can write print axioms theoremname in a file to verify that sorry is not used in the proofs.
You will need a working version of Lean 2 to compile this repository. Installation instructions for Lean 2 can be found here. After that, you can run linja (or path/to/lean2/bin/linja) from the command-line in the main directory to compile this repository.