# BI Algebras and Monoidal Topoi
In separation logic, the set of propositions forms a BI algebra.
A Heyting algebra provides all the familiar logical connectives.
A BI algebra adds the separating conjunction and implication,
which are useful for reasoning about mutable state.
In topos theory, we have the concept of a monoidal closed topos.
A topos is effectively a mathematical universe; it has an "internal logic" which mostly feels like set/type theory.
A monoidal closed topos adds an additional "product type" and "function type", in addition to the regular ones.
These structures look very similar to each other.
This suggests a number of interesting avenues of exploration.
## Generalization of separation logic
This one is obvious. We use separation logic to reason about programs.
Are monoidal topoi likewise useful for reasoning about programs?
## Noncommutative geometry
*Synthetic differential geometry* is an alternative approach to calculus that uses a rigorous formulation of infinitesimals,
rather than limits and ε-δ definitions. For example, there is a space of nilsquare infinitesimals
\\(D = \\{d\\in\\mathbb{R} | d^2=0\\}\\), and an axiom that the functions \\(D\\to\\mathbb{R}\\)
extend uniquely to *linear* functions \\(\\mathbb{R}\\to\\mathbb{R}\\).
Synthetic differential geometry can be modeled as the internal language of a topos.
That topos is the functor category \\(\[\\mathcal{C}, \\mathit{Set}\]\\),
where \\(\\mathcal{C}\\) is some category of commutative algebras, possibly with extra structure.
*Noncommutative geometry* is a "quantum" generalization of geometry that I don't understand very well.
But the basic idea is this:
- All of the information about a geometric space is contained in the algebra of functions on that space.
- That algebra is always commutative.
- So let's instead take a *noncommutative* algebra, and treat it as if it were the algebra of functions on some mysterious "noncommutative space"!
Putting these together, it seems to me that there should be some sort of "Noncommutative synthetic differential geometry",
modeled on the topos of functors from a category of *non-commutative* algebras.
These topoi turn out to be monoidal closed topoi. Furthermore, the axioms about infinitesimals still apply,
but only if you use the *monoidal* version of function types.
All of this suggests to me that there should be some beautiful connection
between quantum mechanics and separation logic, mediated by noncommutative synthetic differential geometry.

- [BI Algebras and Monoidal Topoi](./bi_topos.md)