GAT for exterior calculus in arbitrary dimension

I am working on a GAT for exterior calculus that will provide a symbolic frontend to the DEC machinery in this package. It would be neat have a theory that works in arbitrary integer dimension, something like:

```julia
@theory ExtCalc{Ob,Hom,Space} <: AdditiveCategory{Ob,Hom} begin
Space::TYPE
ndims(X::Space)::Int

Chain(X::Space, n::Int)::Ob
∂(X::Space, n::Int)::Hom(Chain(X, n), Chain(X, n-1))
∂(X, n+1) ⋅ ∂(X, n) == zero(Chain(X, n+1), Chain(X, n-1)) ⊣ (X::Space, n::Int)

Form(X::Space, n::Int)::Ob # == Cochain(X, n)
d(X::Space, n::Int)::Hom(Form(X, n), Form(X, n+1))
d(X, n-1) ⋅ d(X, n) == zero(Form(X, n-1), Form(X, n+1)) ⊣ (X::Space, n::Int)

dual(X::Space)::Space
hodge(X::Space, n::Int)::Hom(Form(X,n), Form(dual(X), ndims(X)-n))
end
```

However, using Julia integers in GATs is currently not fully supported by Catlab, so the above code does not work.

Alternatively, one could axiomatize the integers within the GAT itself, such as in [this paper](https://arxiv.org/abs/2007.00167). As a GAT, this might look like:

```julia
@theory Integers begin
ℤ::TYPE
zero()::ℤ
succ(n::ℤ)::ℤ
pred(n::ℤ)::ℤ
pred(succ(n)) == n ⊣ (n::ℤ)
succ(pred(n)) == n ⊣ (n::ℤ)
end
```

Frankly that seems more trouble than its worth. Instead, we should improve upstream support for mixing certain basic Julia types with GATs and then revisit this issue.