A development of the theory of postulated colimits in Coq. Includes a proof that the pushout of a monomorphism is a monomorphism in a 'sheaf topos'.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
talk-2018-03-05
.gitignore
LICENSE.txt
README.md
category.v
coequaliser.v
disjoint_union.v
objoid_mapoid.v
outline.md
pushout.v
pushout_of_monomorphism.v
scratch.v

README.md

Postulated Colimits in Coq

A development of the theory of postulated colimits in Coq. Includes a proof that the pushout of a monomorphism is a monomorphism in a 'sheaf topos'.

Prerequisites

Install Coq here.

If developing in emacs place the following lines:

(setq coq-load-path-include-current t)
(setq coq-compile-before-require t)

in your init file. If not then you may have to run coqc on the various dependencies to run the proofs.

Acknowledgements

  • Coq - Proof Assistant
  • Postulated colimits and left exactness of Kan-extensions, Anders Kock, available here