Finite Inverse Categories as Signatures

We define a simple dependent type theory and prove that its well-formed types correspond exactly to finite inverse categories.