CCCaTT is a typechecker for unbiased cartesian closed categories.

Typechecker

Examples

If you don't feel inspired, here is a sample session (or try examples above):

coh K {a b : .} : a -> b -> a

coh ap {a b : .} (t : a -> b) (u : a) : b

coh ap-K {a b : .} (x : a) (y : b) : ap (ap K x) y = x

More details

• The source code.
• The documentation for the modules.
• The CaTT cousin.