A type theory for unbiased cartesian closed categories. We provide a small proof assistant which you can also try online. In order to get used to the syntax, you can have a look at the test file.
The theory should come up soon.
The Emacs mode can be loaded by adding
(require 'cccatt-mode "~/path/to/cccatt-mode.el")
to you .emacs file.