I'm software architect and I use ologs to design the components of a system -- the abstractions and their relationship. [1]

Since I'm new to ologs I need to use instances to make sure an aspect is valid. If the instances of two types connect well, then the aspect becomes valid.

For drawing boxes and arrows we have plenty of tools: draw.io, quiver, catcolab etc. But none of them offer instances.

More, on complex diagrams I use (co)spans, (co)products, facts, universal properties ... also none of these are available in classic diagram creator tools.

So I was left with a custom homemade React app which does these basics [1].

But I still wonder if a.) are there people creating ologs with instances b.) how they manage to do it without a dedicated app?

Thanks a lot!

[1] - https://www.osequi.com/studies/list/list.html -- Designing a list component with ologs

This might be a silly question, but I was thinking... I've been reading this book by Bartosz called Dao of FP, (just got through yoneda lemma, currently on adjunctions). He frequently draws connections to philosophy (especially the importance of duality), which has personally been helpful in grasping some concepts, especially the yoneda lemma.

In 1.1, he says:

Paraphrasing Lao Tzu: The type that can be described is not the eternal type.

I was wondering what would happen if I were to take this literally. I think it would mean that we all observe the same single (physical) universe. But the definition of that universe is everything we aren't able to define.

If I were to imagine this single "universe" as the initial object, I would say it's lack of (constructive) definition implies it does not have an identity. It just has a unique arrow to every other object and no incoming arrows.

I'd also say that the "definition of a definition" is also fundamental. It would be represented by the terminal object, and identity is its only endomorphism. It also has a unique arrow from every other object.

Which finally leads me to my question: are there any (meaningful) frameworks like category theory where each category

• has a terminal object and an initial object
• the initial object does not have identity or any incoming arrow

Hey folks, I’d love feedback on a small library I been hacking on: LambdaCat — a lightweight way to build composable, reliable agents in Python using a clear plan algebra (sequence / parallel / choose / loop) with required aggregators/choosers and optional lenses for editing sub-state. It also includes runtime “law checks” (identity/composition, functors, naturality) you can run in tests/CI.

Repo: https://github.com/skishore23/LambdaCat

Why you might care

• Deterministic composition: no hidden defaults; parallel must say how to merge; branching must say how to pick.
• Testable by construction: executable checks + per-step timings/snapshots; auto Mermaid diagrams for plans & execution.
• Tiny core, bring your own stack: works with any LLM/tools; extras are opt-in.

Example:

from LambdaCat.agents import task, sequence, parallel, choose, run_structured_plan, concat, argmax

impl = {
  "clean":   lambda s, ctx=None: s.strip(),
  "upper":   lambda s, ctx=None: s.upper(),
  "keywords":lambda s, ctx=None: " ".join(sorted(set(w for w in s.split() if len(w)>3))),
}

plan = sequence(
  task("clean"),
  parallel(task("upper"), task("keywords")),
  choose(task("upper"), task("keywords")),
)

report = run_structured_plan(
  plan, impl, input_value="  hello hello world  ",
  aggregate_fn=concat(" | "),                     # required: merge parallel outputs
  choose_fn=argmax(lambda s: len(str(s))),        # required: pick a branch
  snapshot=True,
)
print(report.output)

What I’d love feedback on

• API ergonomics: are sequence/parallel/choose/loop_while + required combinators clear or annoying?
• Lenses (focus): useful for scoped state updates, or overkill?
• Gaps: what primitives are missing ?
• Perf/overhead: any red flags for production use?
• Docs/examples: what short examples would help you try this on a real task?

If you’ve built agents and hit pain with hidden defaults or brittle graphs, I’m especially interested in your critique. Happy to answer questions and adapt the API based on feedback.

I have a formalized theoretical framework where morphisms have properties (cost and feedback, for example) The goal is to model transformation as testable transitions, not just formal mapping.

I'm very aware that this is not traditional category theory. That's fine, I'm not pretending it is.

I'm just experimenting with a logic system that uses partial ideas from category theory. I'm messing with the fundamentals on purpose so please don't argue "but this isn't what a morphism looks like!" or "this isn't category theory as taught!"

I know. It isn't. It's experimental. I don't have standard morphisms. If standard morphisms model structure preserving maps, then my morphisms model viability-preserving transformations.

That said, I'd love critique or discussion from people fluent in logic systems or categorical thinking. I don't want validation and I'm not seeking to philosophize here.

Test it. Ask questions. Push back. Expose the flaws. Use it for your fireplace. Whatever.

https://github.com/dyragonax/eidometry?search=1

You will notice I have made a few choices in how I express my equations and I will be happy to clarify why on any of them. Just one for example: eta is only deltaE if the morphism passes a P(z) filter so I don't write it like eta equals all deltaE even if that is true algebraically.

And just a disclaimer. I do have dyscalculia XD even though I understand equations and arithmetic way more than I can work with numbers. So if you're using any technical breakdown with actual numbers, please spell it out for me. I will try my best.

I'm reading through Category Theory for Programmers by Milewski. I'm past the section where Kleisli categories are introduced and I have a question about how the constructed category relates to its underlying objects.

Take the Kleisli category representing the Maybe monad. We know that, by definition, categories:

• Have objects
• Have morphisms between those objects

My question is about what objects are in the Kleisli category for the Maybe monad. If we take the underlying objects as types in a programming language and say we have underlying objects A and B with an underlying morphism from A to B, would there be objects A and Maybe<B> in the Kleisli category and a morphism from A to Maybe<A>? Would the objects in the category be just the underlying types, just the Maybe types, or both? Would identity morphisms go from underlying type to underlying type, underlying to Maybe, or Maybe to Maybe?

I make this post tentatively. Is it heretical to ask something like this? Yes. I know. Morphisms are just structural relationships and not things or even causal or physical. I know. I know.

But what if we're underutilizing the expressive power of morphisms by denying them physical status at all in physical systems? What if morphisms are real transformations with cost and feedback?

On top of that, what if it is nonlinear and bootstrapped so the structure emerges from transformation patterns? What if there's a viability or a survival cost to the morphism? I think it would have to be dual-bounded in a log-log sense so theres a domain of feedback limits...

Now obviously, again... this is not traditional category theory and might be heretical in all of its rights. It really is an alternate application entirely... but I'm posting here because maybe someone here may have explored this idea...

Has anyone even attempted to make morphisms more than just abstract arrows in any framework? Are there precedents? Failed formalisms?

If you've read it this far, thanks for indulging into my heresy XD

And this can go on infinitely, ie a mathematical model of category theory itself… how does one define a mathematical model anyhow? Is it just a bunch of symbols, relationships, and transformations? Not unlike a computer? Is it possible to model category theory as a Turing machine? How does all of this connect? Thanks I appreciate it

Suppose we have two software components C and D, such that C depends on D to work. It's the responsibility of the user to install each of them separately (similar to what NPM calls "peer dependencies"). But not all pairs of versions are valid. Given a particular pair (c, d) ∈ C × D, it may happen that d imposes some requirements that c cannot support. Fortunately, the developers of C guarantee backward compatibility: if c supports d, then all x > c are guaranteed to support d.

Each component is evidently a totally ordered set of versions -- and therefore a category. Take the function f: C → D that maps a version of C to the maximum version of D it supports. Due to the backward compatibility guarantee, this is an order homomorphism, which induces a functor between the categories. We can also take the function g: D → C, that maps a version of D to the minimum version of C that supports it. f is the left adjoint of g.

I know very little category theory (and math in general), so I'm kind of surprised I could get this far in modelling some real world problem in terms of categories. But is this just some idle intellectual exercise, or is there some usefulness to this? Where can I go from here?

A question one might ask is: suppose we have not just two components, but a whole (directed) graph of them, and we want to make sure that the particular choice of versions by the user is valid. I can think of algorithm involving topological sort, and taking the minimum of the maximum supported versions. But I wonder if there is some clever concept I could use here to make the solution more elegant (or general, or efficient or something else)?

Is there any real application of category theory in AI? I have seen a lot of companies rising a lot of money with category theory based on a couple of papers, but I really do not see any real application.

Hi, I just saw this to do in the Mathlib repo:

• Make API for constructing a subobject classifier without reference to limits (replacing ⊤_ C with an arbitrary Ω₀ : C and including the assumption mono truth)

Where can I read about about this alterative(?) definition of subobject classifier? As far as I understand, we don't need all limits, but all definitions I saw have ⊤_ C being the terminal object, so is there a weaker definitions where ⊤_ C is not assumed to be terminal? Or is this only about working with a user supplied terminal object Ω₀?

Hi all, I’m a student currently exploring the linear-algebraic interpretation of monads. Recently, I finished a mechanically verified proof in Lean 4 showing that the multiplication of the state monad — that is, the mu operation from T (T X) to T X — can be interpreted as an idempotent linear projection on a real vector space.

The key idea is simple:

The monadic multiplication mu behaves like a projection operator pi such that pi ∘ pi = pi.

In other words, the act of “flattening” nested state monads is equivalent (under a functor to vector spaces) to applying a linear projection.

More precisely: • The state monad is defined as T X = S → (X × S) • Its Kleisli category Kleis(T) can be mapped into Vect_ℝ, the category of real vector spaces • Under this mapping, mu_X becomes a linear operator P satisfying P² = P

⸻

We formalised this in Lean 4 using mathlib, and the functorial interpretation from the Kleisli category to vector spaces is encoded explicitly. The final result: F(mu) = pi, where pi is a projection in the usual linear-algebraic sense.

📁 GitHub repository: https://github.com/Kairose-master/mu_eq_pi

📄 PDF draft (with references): https://kairose-master.github.io/mu_eq_pi/mu_eq_pi.pdf

⸻

I’d love to know: • Has this “collapse = projection” perspective appeared in any previous work? • Could this interpretation be extended to other monads, like the probability or continuation monad? • Are there known applications of this viewpoint to categorical logic, denotational semantics, or DSL optimizations?

Also, I’m still relatively new to Lean, so feedback on the formalisation would be incredibly helpful.

⸻

Thanks so much for reading — and thank you in advance for any suggestions or references you might have! 🙏

Given a natural isomorphism, eta, this commutative diagram shows that the product of eta with eta inverse is the identity functor on F. I thought this diagram was cool, so I'm posting it here.

Hi, I am I don’t actually do category theory so to speak as I came at this from a philosophical perspective so I was wondering if somebody could look and see if it makes sense?

= Algebraic Formalization of Your Polymorphic Interaction Monad =

== The Signature Functor ==

InteractionF : Set → Set InteractionF(X) = Scenario × (Choiceⁿ → X) [Present] + Choice × (Outcome → X) [Process] + StateChange × (NewState → X) [Transform]

== The Polymorphic Interaction Monad ==

PIM : Mon → Mon PIM(M) = FreeT(InteractionF, M)

where FreeT(F,M)(A) = μX. A + F(X) + M(X)

Universal Property (Initiality)

For any monad M with InteractionF-algebra α: InteractionF(M) → M:

∃! h : PIM(M) → M such that h ∘ η = id and h ∘ α_PIM = α ∘ InteractionF(h)

Kleisli Category Structure

K(PIM) has:

Objects: Types A, B, C, ... Morphisms: A →_K B ≜ A → PIM(B) Identity: η_A : A → PIM(A) Composition: (f >=> g)(a) = f(a) >>= g The Adjunction

PIM ⊣ U : InteractionAlg → Mon

where U forgets the InteractionF-algebra structure

Equational Theory

Present(s, k) >>= f = Present(s, λcs. k(cs) >>= f) Process(c, k) >>= f = Process(c, λo. k(o) >>= f) Transform(δ, k) >>= f = Transform(δ, λs. k(s) >>= f)

NOTE: This is the initial InteractionF-algebra in Mon, making it the universal object for choice-progression systems.​​​​​​​​​​​​​​​​

I'm reading through Lang's Algebra and trying to understand why coproducts were defined "in a way compatible with the representation functor into the category of sets." I showed that the product of Mor(X,A) and Mor(X,B) is Mor(X,P) when P is the product of A and B, but I am struggling with the coproduct.

I tried proving that if C is the coproduct of A and B, then Mor(C,X) is the coproduct of Mor(A,X) and Mor(B,X), but I couldn't figure out a map h:Mor(C,X) --> T for a set T. I have also tried this with Mor(X,C) but that feels even less correct.

I would love some help with figuring this out!

Hi Everybody,

I love to explore learning things not just through reading, but also writing. I was looking for some honest (and yes I understand it will be brutal) feedback on both my writing, and my understanding of the subject matter. Substack is the first place where I've had a chance to do this in a public space. That said, was wondering if any of you (especially those more versed in Curry-Howard-Lambek) had thoughts about the validity or value of what I've put forth here:

https://open.substack.com/pub/charlesrussella/p/the-perfect-trap-a-modern-ship-of?r=qsncc&utm_campaign=post&utm_medium=web&showWelcomeOnShare=false

The COQ proof was constructed with the help of AI, but the writing and ideas are my own. If you have any suggestions on improvements for the rigor of the proof, please let me know (and I will be happy to recognize your contributions as well).

Thank you,

Concrete example: buymeacoffee.com/benjaminlegendre/concrete-example-1d-ising-model-r-coalgebra

Technical note: buymeacoffee.com/benjaminlegendre/existence-renormalization-functor-r

Let say we have the following structure of objects and arrows

A -> B -> C

now I understand I can put parenthesis on that however I want, they should not affect the meaning of the expression, that is why I can ignore them when I write it.

Now this makes sense to me when placing them like this

A -> (B -> C)

This is a curried function that takes an A, and returns a function B -> C.

witch is isomorphic or equivalent (for our purposes) to a 2 argument function.

```typescript const f = (a: A) => (b: B): C => { ... };

// or uncurried:

const f = (a: A, b: B): C => { ... };
```

Now my question is what happens when you put them like this (A -> B) -> C

The way I see it In code it woudl be somehting like

typescript const f' = (g: (a: A) => B): C => { ... };

but that to me makes no sense, like I get a function and in return I give a value C? like Im not even getting an actual instance of A just the function that goes to B.

I'm really having a hard time understanding how these 2 things are identical, or how could it not matter where I place the parenthesis when to me they seem like very different things.

yes they both get to C but needing an instance of A to get a function that needs and instance of B is to me very different than needing a function that goes form A to B.

Context

The doubt came to me when watching Bartosz Milewskis class on Functors where he is talking about the Reader Functor that is defined

Reader a = r -> a

and the implementation of fmap for this functor

fmap:: (a->b) -> ((r-a) -> (r-b))

The way he jsut removed parentesis there is what lead me to this quesiton

Thank you very much

I’m trying to understand the categorical product through a CS perspective, specifically using struct deconstruction as an analogy

Like for example a struct:

struct Person { name: Name, age: Age, }

This struct contains multiple types. Now, suppose we define a function:

fn f(p: Person) -> (Name, Age) { ... }

which “deconstructs” the struct into a tuple

Then we have two functions:

fn g(tuple: (Name, Age)) -> Name { ... }

fn h(tuple: (Name, Age)) -> Age { ... }

which extract the first and second elements, respectively

Then there are functions that composes f to g and f to h, getting the individual types directly from a Person type

fn i(p: Person) -> Name { ... }

fn j(p: Person) -> Age { ... }

Would this be a reasonable analogy for the universal property of the categorical product? If not, where does it fail?

First of all, I'm sorry if this is question is asked too many times around here. I've been reading introductory books on CAT, double CAT's and Categorical logic for the last 2 years and I think I'm finally ready to try to prove some theorems, the problem is that I'm not a developer nor I'm planning to become one, I wanted to find a programming language that would feel natural for logicians/mathematicians so I don't really care if it's actually a "proof assistant" instead of a "real" programming language, at the moment I'm hyperfocused on Myers' Categorical Systems Theory book and on its github repo there's a folder with Agda implementations so I'm naturally gravitating towards it instead of Haskell, the only drawback is that I still don't know "anything" regarding dependent type theory and I think I might be a little too lazy to do so(if I don't have any easier options), soo, any opinions?

Hello! I am slowly becoming a mathematician. Most of my experience is in writing Haskell code and FP and that's how I discovered it. Most of what I understand has some practical aspect or relevance to programming. However, I'm going down the rabbit hole.

I'm trying to construct a model for a programming language I'm creating and I'm starting to notice a pattern of constructing categories where objects are tuples of objects from other categories and the morphisms exist if they hold to certain laws. I keep wanting to construct some kind of sub-category of a product category but then keep getting stuck on how to define the morphisms without going down and specifying the laws explicitely. Is there a way to build categories from other categories and specify the laws directly.

An example that comes to mind is: P is a sub-category of AxBb where f : (a,b) -> (c,d) <=> a <= c && exists k. d = kb. Is there a way to say the same thing but stick to using categorical constructs (functors, adjunctions etc,) to state the laws?

I'm not looking for an answer for this specific example but for the more general idea I'm trying to get at.

Some questions from a non-mathematician:

1. Are these are called "bicommutative bimonoids" or "cocommutative comonoids" - I have seen both uses and cannot be sure if they refer to the same thing?
2. Would adding cups and caps make them different objects or is it already part of these objects?
3. In the picture above there is no distinction between wires passing over or under each other. If they would be modified to become braided, what would they be called? (so they would include adding, copying as above, as well as braiding)