I've been thinking a lot about functorial semantics lately - it's probably one of the best ideas in category theory. The idea is relatively simple just that a functor

C -> D represents the structure of C being imposed in D. 1/n^{}

C -> D represents the structure of C being imposed in D. 1/n

Lawvere used this idea in his thesis to revolutionize universal algebra. Universal algebra aims to provide a common framework for all the sorts of gadgets that algebraists study e.g. groups, rings, fields, modules, etc. Lawvere identified a class of categories 2/n
^{}

called Lawvere theories representing algebraic gadgets. For a Lawvere theory Q, a finite product preserving functor Q -> C is the same as an instance of the gadget Q represents in C. For example if Q is the Lawvere theory of groups, a finite product preserving functor 3/n
^{}

Q -> Set is the same as an ordinary group. You can get a lot of mileage from this perspective including:

* For every model of Q there is a free Q-model adjunction

* for every morphism of Lawvere theories f : Q -> R there is an adjunction between models of Q and 4/n^{}

* For every model of Q there is a free Q-model adjunction

* for every morphism of Lawvere theories f : Q -> R there is an adjunction between models of Q and 4/n

models of R.

* The categories of models of a Lawvere theory enjoy many nice properties...including at least finite completeness and cocompleteness.

* Lawvere theories can be smashed together using the tensor product to build more complicated types of Gadgets.

And lots more! 5/n^{}

* The categories of models of a Lawvere theory enjoy many nice properties...including at least finite completeness and cocompleteness.

* Lawvere theories can be smashed together using the tensor product to build more complicated types of Gadgets.

And lots more! 5/n

Lawvere theories are wonderful but functorial semantics has a lot more applications. More generally in categorical logic, a category T is used to represent a logical theory so that it's morphisms correspond to proofs. Then a structure preserving functor T -> C is 6/n
^{}

Is a model of T in C, in the usual sense that logicians mean. Categorical logic is a huge field and there is a lot more you can get from the functorial semantics idea...but I don't feel confident summarizing it all without leaving out something big.

7/n^{}

7/n

Functorial semantics also has use in applied category theory.

* David Spivaks work models databases as functors from a Schema representing the type of data and it's relationships to the category of Sets

* Colored Petri nets can be understood as symmetric monoidal functors..8/n^{}

* David Spivaks work models databases as functors from a Schema representing the type of data and it's relationships to the category of Sets

* Colored Petri nets can be understood as symmetric monoidal functors..8/n

from the category of executions of a net to Span.

* Other extensions of Petri nets can be understood as functors out of the category of executions. My favorite example is nets whose tokens are themselves Petri nets. You can read about them on my blog: jadeedenstarmaster.wordpress.com/2021/01/29/net… 9/n^{}

* Other extensions of Petri nets can be understood as functors out of the category of executions. My favorite example is nets whose tokens are themselves Petri nets. You can read about them on my blog: jadeedenstarmaster.wordpress.com/2021/01/29/net… 9/n

There are many more examples of functorial semantics in all fields which categories touch. Does anyone have an example that they've encountered in their own work?

10/n, n=10.^{}

10/n, n=10.

I forgot the biggest example of functorial semantics in my own work. Myself and my collaborators work on these double categories (or bicategories, or categories or whatever) whose morphisms represent systems equipped with input and output boundaries. The next step is to 11/10
^{}

functorial semantics i.e. think about double funxtors out of these open categories which represent computations or measurements of these open systems. The functoriality of this syntax and semantics gives compositional formula for building computations on networks from 12/10
^{}

their components 13/10.
^{}

• • •

Missing some Tweet in this thread? You can try to
force a refresh

**
Keep Current with
jade eden
**

Stay in touch and get notified when new unrolls are available from this author!

**
This Thread may be Removed Anytime!**

Twitter may remove this content at anytime! Save it as PDF for later use!

- Follow @ThreadReaderApp to mention us!
- From a Twitter thread mention us with a keyword "unroll"

`@threadreaderapp unroll`

Practice here first or read more on our help page!

Support us! We are indie developers!

This site is made by just two indie developers on a laptop doing marketing, support and development! Read more about the story.

**Become a Premium Member** ($3/month or $30/year) and get exclusive features!

Too expensive? **Make a small donation** by buying us coffee ($5) or help with server cost ($10)

Thank you for your support!

Check out other threads from @JadeMasterMath!

Read all threads by @JadeMasterMath