  We present a domain-specific type theory for constructions and proofs in
category theory. The type theory axiomatizes notions of category, functor,
profunctor and a generalized form of natural transformations. The type theory
imposes an ordered linear restriction on standard predicate logic, which
guarantees that all functions between categories are functorial, all relations
are profunctorial, and all transformations are natural by construction, with no
separate proofs necessary. Important category-theoretic proofs such as the
Yoneda lemma and Co-yoneda lemma become simple type-theoretic proofs about the
relationship between unit, tensor and (ordered) function types, and can be seen
to be ordered refinements of theorems in predicate logic. The type theory is
sound and complete for a categorical model in virtual equipments, which model
both internal and enriched category theory. While the proofs in our type theory
look like standard set-based arguments, the syntactic discipline ensure that
all proofs and constructions carry over to enriched and internal settings as
well.
