Categorical Logic and Type Theory in Cubical

This library is an extension of the cubical library focused on formalization of categorical logic and applications to type theory, especially logical relations. Most of the library is intended to eventually be merged upstream after we have experience with the design here.

The source code has a glorious clickable rendered version.

Style and Build Tests

There are style constraints on whitespace that are used upstream, so we check those with the fix-whitespace whitespace utility. This checks things like trailing whitespace, tabs v. spaces, etc. There are makefile targets to check and fix any whitespace issues.

To check if all of the repository compiles, run make test. Note that make test is what is ran on each push, so it also does the above whitespace checks.