GAT for exterior calculus in arbitrary dimension

[epatters]

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:

@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. As a GAT, this might look like:

@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.

[epatters]

See #32 for the current approach to the exterior calculus GAT.