ncat.v

Set Universe Polymorphism.

Notation "( a ; b )" := (existT _ a b) (at level 0).
Notation "'dfst' a" := (projT1 a) (at level 10).
Notation "'dsnd' a" := (projT2 a) (at level 10).

Record NCat :=
mkNCat {
  Arity : Type;
  Sign : Arity -> Type
}.

Fixpoint CatOp n : NCat :=
  match n with
  | O => {| Arity := unit ; Sign := (fun _ => unit) |}
  | S n' => {| Arity := { A: (CatOp n').(Arity) &
                            (CatOp n').(Sign) A -> Type };
              Sign := (fun '(A ; M) =>
                         { s: (CatOp n').(Sign) A & (M s * M s)%type }) |}
  end.

Reserved Notation "f ∘ g" (at level 55).