Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Rezk completion
branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
limits
ssp
topos
.dir-locals.el
.gitignore
HLevel_n_is_of_hlevel_Sn.v
Make
Make.makefile
Makefile
README.md
auxiliary_lemmas_HoTT.v
category_hset.v
equivalences.v
equivalences_lemmas.v
functors_transformations.v
pathnotations.v
precategories.v
precomp_ess_surj.v
precomp_fully_faithful.v
rezk_completion.v
sub_precategories.v
whiskering.v
yoneda.v

README.md

Rezk Completion

This Coq library mechanizes the Rezk completion as described in http://arxiv.org/abs/1303.0584

It builds upon V. Voevodsky's Foundations library, available on http://arxiv.org/abs/1401.0053

Installation

This library is part of the UniMath repository, available at https://github.com/UniMath/UniMath . The recommended way to obtain this library is to install UniMath. Instructions for installing UniMath can be found on the UniMath web page. The below installation instructions should be considered as obsolete.

Requirements

Coq

The library compiles under Coq8.3pl5, patched according to the instructions given in http://arxiv.org/abs/1401.0053. Lower patch levels of Coq8.3, e.g., Coq8.3pl2, are likely to work as well.

Libraries

Files used from V. Voevodsky's Foundations:

  • uuu.v
  • uu0.v
  • hProp.v
  • hSet.v
  • funextfun.v

They should be installed in the user-contrib/Foundations directory of Coq, so Coq can find them.

Licensing and copyright

Authors: Benedikt Ahrens, Chris Kapulkin, Mike Shulman

The code in this repository is made available under the terms of "CC0 1.0 Universal", see http://creativecommons.org/publicdomain/zero/1.0/legalcode. That means, basically, that we disclaim all rights, including copyright, and put it into the public domain.

The code in this repository is (also) put into the public domain, which means we disclaim any and all copyright protection.

Something went wrong with that request. Please try again.