Differentiating Telescopes

First, a funny coincidence. Consider the act of Record Patching:

(X : Type, Y : Type, f : X → Y → X)[ X := Nat ]

This yields the following telescope:

(Y : Type, f : Nat → Y → Nat)

However, we can also view a patch as a sort of Partial Derivative that returns a dependent telescope (EG: a Bundle of telescopes):

∂ X (X : Type, Y : Type, f : X → Y → X) : Type → Telescope = λ X → (Y : Type, f : X → Y → X)

Our patch from before was simply applying arguments to this bundle.

Moreover, this seems to validate some of the expected properties of partial derivatives. This perplexed me for a bit, as the Coproduct of Telescopes is quite confusing! In particular, it is the "intersection" of telescopes, at which point the formula ∂ x ( Γ × Δ ) = Γ × ∂ x ( Δ ) + ∂ x ( Γ ) × Δ subscript 𝑥 Γ Δ Γ subscript 𝑥 Δ subscript 𝑥 Γ Δ \partial_{x}(\Gamma\times\Delta)=\Gamma\times\partial_{x}(\Delta)+\partial_{x}% (\Gamma)\times\Delta makes perfect sense (recall that the Product of Telescopes is given by telescope concatenation). If we unfold this formula explicitly, it says that to patch a telescope with a field X 𝑋 X , it suffices to patch both sides separately, and then intersect them together.

I suspect that this geometry may come from the underlying dependency graph of a telescope?

Subtracting telescopes

Note that we can meaningfully subtract two telescopes! Consider Monoid - Magma; this gives us (ε : A , idl : ∀ x → ε ⋆ x ≡ x, idr : ∀ x → x ⋆ ε ≡ x, assoc : ∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z), displayed over the signature of a magma.

This is a generalization of the partial derivative, as it lets us differentiate by a whole telescope all at once.

Holonomy

It feels like things like op on theories could be related to Holonomy.

Change structures

There are a couple of possible definitions of change structure:

The first comes directly from A Theory of Changes for Higher-Order Languages:

record Change-structure-on
  {ℓ ℓ'} (A : Type ℓ) (∂A : A → Type ℓ')
  : Type (ℓ ⊔ ℓ') where
  field
    _⊕_ : (a : A) → ∂A a → A
    _⊝_ : (a : A) → (b : A) → ∂A b
    ⊕-invr : ∀ a b → a ⊕ (b ⊝ a) ≡ a

This is sort of like a dependent Left Quasigroup with only one of the laws.

The second comes from Bob Atkey's blog, which replaces subtraction with a "local 0".

record Change-structure-on
  {ℓ ℓ'} (A : Type ℓ) (∂A : A → Type ℓ')
  : Type (ℓ ⊔ ℓ') where
  field
    _⊕_ : (a : A) → ∂A a → A
    𝟘 : (a : A) → ∂A a
    ⊕-zero : ∀ a → a ⊕ 𝟘 a ≡ a

This is vaguely remeniscent of a Category with fibrant objects: we have an operation to take total spaces, and a way to ensure that we can form the identity bundle.

Can we add an exterior algebra to this somehow?

[2025-02-03 Mon]

Some thoughts from the bus today: We need to track the multiplicities in the dependency graph of a telescope!

EG: the telescope (A : Type, pt : A) of a pointed magma has a dependency graph like:

∙∙{\bullet}∙∙{\bullet}(1)1\scriptstyle{(1)}

But the dependency graph of a magma (A : Type, _⋆_ : A → A → A) has a dependency graph like:

∙∙{\bullet}∙∙{\bullet}(12)12\scriptstyle{(12)}

This gives us a way of talking about orientation, as we can have Symmetry Groups act on the edges of the dependency graph.

After discussions with Jacques Carette, we came to the conclusion that you need to be able to compute a symmetry group for a telescope; EG, the symmetry groups of Magma are S 1 × ( S 2 × S 1 ) subscript 𝑆 1 subscript 𝑆 2 subscript 𝑆 1 S_{1}\times(S_{2}\times S_{1}) . A Differential Form for a telescope Γ Γ \Gamma consists of a displayed telescope A : Γ → Tele : 𝐴 → Γ Tele A:\Gamma\to\mathrm{Tele} , and an element of the symmetry group of Γ Γ \Gamma .

In general, symmetry groups can act on displayed telescopes: this is vaguely remeniscent of symmetries in Displayed Type Theory.

The rules for computing symmetry groups are a bit tricky though; Let d : 𝒰 → Group : 𝑑 → 𝒰 Group d:\mathcal{U}\to\mathrm{Group} denote the operation that computes a symmetry group for a type. Ideally, we'd want d ⁢ ( A → A → A ) = S 2 × S 1 𝑑 → 𝐴 𝐴 → 𝐴 subscript 𝑆 2 subscript 𝑆 1 d(A\to A\to A)=S_{2}\times S_{1} ; there is one non-trivial symmetry for the arguments of the function type, and only a trivial symmetry for the output. This becomes clear if we uncurry, but it's not immediatelly apparent how to make this work for curried functions.

It's probably worth looking at Π Π \Pi types generally, though I don't know if it makes more sense to try and compute symmetries, or to index by symmetries instead.

[2025-02-04 Tue]

After deeper thought, it's not really differential geometry that we are doing, its Galois Theory! EG: instead of looking at permutations of Field Extensions, we are looking at permutations of Theory Extensions.

References