package catt

  1. Overview
  2. Docs
An infinity-categorical coherence typechecker

Install

Dune Dependency

Authors

Maintainers

Sources

catt-1.0.tbz
sha256=20a0b4aae3655274cb7336cb158699ceb1ee29909e50405d0ccb9d54d985baeb
sha512=1919da8eea60817a0907be4aa6f399a9e66fc8746d190ea805de8721a44f5f8a68b9c67626b7767e42a7cd0f061e00c16cd6c63570cbdedf15bc31f8b598f72b

CHANGES.md.html

1.0 (2024-10)

Coq catt plugin

  • Working export of catt term into coq

Catt

  • Computation of 1-naturality

  • Computation of functorialisation

  • Computation of inverses and cancellation witnesses

  • Computation of opposites

  • Builtin identities and compositions

  • Computation of suspension and implicit suspension

  • Inference of implicit variables

  • Basic type checker

OCaml

Innovation. Community. Security.