From 9075b67c497249c564a0848db3b2ea69b4612912 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 11 Jan 2019 16:11:43 -0500 Subject: [PATCH] update colim/README --- colimit/README.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/colimit/README.md b/colimit/README.md index 02e1d55..0dce244 100644 --- a/colimit/README.md +++ b/colimit/README.md @@ -1 +1,5 @@ -This folder contains various properties about colimits, from a paper to appear by Egbert Rijke, Floris van Doorn and Kristina Sojakova. \ No newline at end of file +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](https://github.com/leanprover/lean2). After that, you can run `linja` (or `path/to/lean2/bin/linja`) from the command-line in the main directory to compile this repository.