Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.

Administered by:

Server stats:

8.1K
active users

mastodon.world: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.3

#categorytheory

1 post1 participant0 posts today
Jencel Panic

"The notion of natural transformation is surprisingly easy to follow."

Really interesting #categorytheory blog, but this first sentence cracked me up.
blog.juliosong.com/linguistics

I-Yuwen · Category theory notes 10: Composite naturality (Part 1)The notion of natural transformation is surprisingly easy to follow. If you know what an arrow is and what a functor is, then you automatically know what a natural transformation is—it’s just an arrow between functors. I actually wondered why in many textbooks the introduction of such a “natural” notion should wait till all the intervening complex stuff (e.g., universal properties) had been taught. If I were to write an introductory tutorial, I’d introduce functors and natural transformations immediately after categories (as Mac Lane does in CWM), since these are the “backbone” of category theory and to understand them we really don’t need to know too much else.
Ryan

🚩 New preprint

We model open strings with internal defects as stratified manifolds, using bimodules and factorization algebras to generalize Chan–Paton factors. The result: suppressed entanglement, braided statistics, and epistemic obstructions in nonperturbative anyon regimes.

authorea.com/users/854182/arti

Keywords: #CategoryTheory #Mathematics #Math #Physics #StringTheory #Epistemology #Logic

HoldMyType

Example: is is{{{5^5 } ^5 }^5 }^5 a natural number? It is not of the form 0 or Suc(0), or Suc(Suc(0)), ... We need to use induction to show that this is a natural number.

Sjoerd Visscher

I believe proarrow equipments are a great setting to study optics in. You can see the expression for optics and the equivalent string diagram below.

The string diagram even looks like it's just a schematic drawing of an optic, but it really contains all the required information! The arrow heads indicate that s, t, a and b are all tight arrows, but in the loose direction.

If you specialize to the proarrow equipment of functors and profunctors and simplify, you get the final expression. And if you then make S and T constant functors, and A and B monoidal actions, you get back mixed optics.

#categorytheory#optics
Programming Languages Delft

"2-Functoriality of Initial Semantics, and Applications" by Benedikt Ahrens, Ambroise Lafont, and Thomas Lamiaux was accepted at #icfp

"We provide tools to compare and relate the models obtained from a signature for different choices of monoidal category [..] we use our results to relate the models of the different implementation [..] and to provide a generalized recursion principle for simply-typed syntax."

Read it on #arXiv: arxiv.org/abs/2503.10863

arXiv logo
arXiv.org2-Functoriality of Initial Semantics, and ApplicationsInitial semantics aims to model inductive structures and their properties, and to provide them with recursion principles respecting these properties. An ubiquitous example is the fold operator for lists. We are concerned with initial semantics that model languages with variable binding and their substitution structure, and that provide substitution-safe recursion principles. There are different approaches to implementing languages with variable binding depending on the choice of representation for contexts and free variables, such as unscoped syntax, or well-scoped syntax with finite or infinite contexts. Abstractly, each approach corresponds to choosing a different monoidal category to model contexts and binding, each choice yielding a different notion of "model" for the same abstract specification (or "signature"). In this work, we provide tools to compare and relate the models obtained from a signature for different choices of monoidal category. We do so by showing that initial semantics naturally has a 2-categorical structure when parametrized by the monoidal category modeling contexts. We thus can relate models obtained from different choices of monoidal categories provided the monoidal categories themselves are related. In particular, we use our results to relate the models of the different implementation -- de Bruijn vs locally nameless, finite vs infinite contexts -- , and to provide a generalized recursion principle for simply-typed syntax.
#TypeTheory#CategoryTheory
TrendingLive feeds
About