Reedy

A formalisation of some results on the Reedy fibrant diagrams in two-level type theory. WIP port of the Lean implementaion: https://github.com/annenkov/two-level

Usage

Clone the repo with git submodules:

git clone --recurse-submodules git@github.com:CoqHott/reedy.git

Run make to compile the project (also compiles the coq-2ltt submodule).

Dependencies

Amin Timany's Category library: https://github.com/amintimany/Categories

Requirements

Coq 8.7