mstewartgallus

Still very confused and haven't figured it out but here are some notes.

I think that treating a syntax tree as dual to variations along the boundary of the tree sort of makes sense.

I still need to figure it out for real. This is still a mess rn.

Still can't figure out how to integrate distributions against Hasse-Schmidt algebra.

Given a step operator for small step semantics S ∈ 𝒟 ⊗ 𝒟, let S* ∈ 𝒥 × 𝒥 → k where S*(f, g) = ∫ S (f ⊗ g) . This ought to describe the "kinematics" of the operational semantics. In a certain sense, there's a relationship between a tree and the boundary of the tree.

mstewartgallus

k = SphericalCompletion(AlgClosure(𝔽₂((s, t))))

𝔻ⁿ = { x ∈ k⟨x₁, ..., xₙ⟩ | |x| ≤ 1 }

π₁ ∈ 𝔻ⁿ → 𝔻ⁿ
π₁(x) = ∑ₙ [n even] (x · tⁿ) t^(n/2)

π₂ ∈ 𝔻ⁿ → 𝔻ⁿ
π₂(x) = ∑ₙ [n odd] (x · tⁿ) t^((n - 1)/2)

mstewartgallus

The Borel algebra of a topological space is already a sigma-complete Boolean algebra so we can just do a Laurent series over it.

K = 𝔽₂((t))
R = 𝔅(X)((t))

Use a variation on Kahler differentials (hyperdifferential ring) for the Hasse-Schmidt derivative to cope with positive characteristic.

Ω¹ = R[Dₙr | r ∈ R, n ∈ ℕ]/~ where
   D₀	r ~ r
   D₁k ~ ∅

mstewartgallus

{-# OPTIONS --cubical --guarded #-}
module clocked where
open import Agda.Primitive
open import Agda.Builtin.Cubical.Path
open import Function.Base using (_∘_)
open import Relation.Nullary
open import Data.Unit
open import Data.Sum
open import Data.Product using (_×_; _,_)
open import Data.Bool using (Bool; true; false; if_then_else_)

mstewartgallus

I think you want something along the lines of the following for an internal logic of Rel.

One interesting thing is that I think you can extend things pretty simply with a kind of automatic differentation as Rel is pretty close to F₂-Vect/Ab₂.

So add h to the grammar and add rules.

Γ ⊢ h: B
h ∧ h ⟶ ∅

Then define

mstewartgallus

Trying to figure out an odd kind of anti-symmetric calculus. Just very awkward to work with substructural logic.

The trouble is that a double category sort of thing where the source object is the composition of several spans is really awkward to work with. Anti-symmetry is an attempt to approach things from the opposite perspective of apartness instead of equivalence and groupoids.

t ::= 𝔻 | 1 | t₀ ∧ t₁ | ⋆t

───    id
t ⊢ t

Γ, t₀, Δ, t₁, Σ, t₂, Π ⊢ t₃

mstewartgallus

Relational calculus with hopes to give semantics in a kind of "alternating multicategory".

I want to work with the exterior algebra ⋀ 𝔽₂[S] (or possibly formal power series ⋀ 𝔽₂[[S]] or algebraic power series ⋀ 𝔽₂(S)) as a nice way of working with set-set apartness relations and denotational semantics.

I want a kind of operad for my set of terms S that composes well with the exterior algebra ⋀ 𝔽₂[S]. I think I require some form of "super operads" but finite fields are already really confusing. Not really happy that enriching over super vector spaces seems to be required.

I suspect you basically want a kind of graded closed semi-additive category but maybe a little weaker.

Symmetry is a natural isomorphism.

mstewartgallus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.

Inductive U :=
| const (A: Type)

| id
(* | compose (τ0 τ1: U) *)

| empty

mstewartgallus

Set Primitive Projections.

Require Import Coq.Unicode.Utf8.

Reserved Infix "∈" (at level 90, right associativity).

Variant fiber {A B} (f: A → B): B → Type :=
  | fiber_intro x: fiber f (f x).
Arguments fiber_intro {A B f}.

mstewartgallus

Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Coq.Lists.List.

Import List.ListNotations.

Reserved Notation "Γ ⊢ Δ ⇒ τ" (at level 90).
Reserved Notation "x ∈ Γ" (at level 90).
Reserved Infix "$" (at level 20, left associativity).