Peter, as far as I remember, you were interested in the “Field with one element”, so I suppose, you've read 2015 paper “Absolute algebra and Segal’s Γ-rings” by A. Connes and C. Consani. I want to discuss the connection between Linear Type Theories and generalization of semirings Connes et al. developed in that paper to accomodate the 𝔽₁-like objects.
In ordinary algebraic theories, you have the formation rules like these:
a : G
———————unit —————————inv
e : G a⁻¹ : G
a : G b : G
————————————————compose
ab : G
Multiple inputs, single outcome. An algebraic theory is an explicit presentation of a finitely-presentable category-with-finite-products in terms of generators (finite number of basic types and typed formation rules) and relations (equational axioms). In algebraic theories equational axioms may duplicate or discard inputs, for instance:
a : G
——————————
a⁻¹a = e
(here we use a twice on the left side and omit it completely on the right side)
It's not possible to model an algebraic theory in generic monoidal categories since one needs canonical projections and diagonals to make sense of such equational axioms: the tensor product has to be the categorical product.
One possible generalization of algebraic theories is to restrict duplication and/or omission of inputs. In such formalism one cannot write down a definition of a group, but one can introduce discarding and duplication explicitly as defined operations, leading to definition of a formal Hopf algebra instead.
It also seems possible to develop a hybrid formalism, where duplication and omission are not restricted, but controlled. There, we choose a semiring (e.g. the {0, 1, ω} semiring or {0, 1, 2, ..., ω}) to annotate constituents with its elements telling how many instances of an input are required to obtain the outcome, see http://bentnib.org/quantitative-type-theory.pdf. Inputs annotated by 1 as linear or affine ones, variables annotated by ω behave as in ordinary algebraic theories, in general the rules look as follows
s :¹ Server r :ʷ Request
—————————————————————————————
s!r : Result
Four years ago I've met an interesting computational case, where under specific circumstances you can run computation of two decimal expansions of a real number, r⁺ and r⁻. One of the computations may stall at some point, but one of them always remains productive and yields digit after digit indefinetely. If both remain productive, they yield the same number (possibly two different expansions of the same number, like 1.0000... and 0.9999). This led me to the idea to consider non-deterministic generalizations of algebraic theories, where you could obtain multiple outcomes when applying an operation:
c : Coin
——————————————————————————————toss
c↘tt : Bool c↘ff : Bool
or even
e :¹ Spin½ d :ʷ Direction
——————————————————————————————————measure
e⁺ : Spin½[d] e⁻ : Spin½[-d]
Here we have annotated the stuff above the line by elements of a chosen semiring, but what about elements below the line?
Consider the generalization of semirings developed in the “Absolute algebra and Segal’s Γ-rings” by Connes and Consani. There, one introduces 𝕊-modules as generalization for commutative monoids (M, 0, +) and 𝕊-algebras as generalization for semirings, where one additionally has an associative unital multiplication that distributes over the addition.
In a nutshell, an 𝕊-module is a sequence of types (in sense of Homotopy Type Theory) M(0), M(1), M(2),.. representing “summable lists of elements of M” of given length. More precisely, M is a type-valued functor from the category of finite sets and maps between them. Morally, the values of the functor on finite sets Fin(0), Fin(1), Fin(2), etc, are the types of “summable lists of elements of M” of given length and values M(f) of the functor on maps f : Fin(n) -> Fin(m) provide all available operations to transform a summable list of the length n into the list of the length m while keeping the sum unchanged: think of f in terms of arrows between finite sets of numbered points, k-th element of the "new" list will be zero if no arrows from the "old" list point into it, and sum of all elements pointing into it otherwise, the property of f being a map guarantees that each element of the "old" list appeared exactly once in the "new" one, thus the sum remains unchanged. Operations on "summable lists" arising from functions between finite sets provide us with permutations, inserting of zero between any summands and partial (in case we're mapping into M(n) with n > 1) or complete summation (in case we're mapping into M(1)) of summable lists. Functoriality guarantees that summation is commutative and associative. The unique maps from M(0) into M(n) make M(n) into pointed spaces with selected point being the list of all zeroes.
An 𝕊-algebra is defined as a monoidal object in the category of 𝕊-modules, i.e. it is an 𝕊-modules equipped by associative multiplication distributive over summation of summable lists. 𝕊-algebras play the role of generalized semirings. Matrices with coefficients in such “semirings” are allowed to contain not arbitrary, but only summable lists of elements of a "semiring" as their rows. This way one recovers permutation groups as groups of invertible matrices over 𝔽₁ etc.
I suspect that 𝕊-algebras are precisely the gadgets we need to do accounting for quantitative non-deterministic algebraic theories: the non-deterministic outcome with n possibilities has to be annotated by a summable list of length n. I'm looking for a somebody discuss this suspicion and sort out why it does not really make any sense, or develop such a framework and its categorical semantics if it does.