← Back to Portfolio

Interactive Category Theory Commutative Diagrams

Direct manipulation of categorical structures, functorial diagrams, and natural transformations formalized in Georgy Dunaev's mathematical foundations and Lean 4 audit files. Drag any node to observe topological preservation, or click a path button to verify commutativity.

1. The Yoneda Lemma: Naturality Square

For any morphism $f: A \to B$, the natural transformation $\alpha: \mathcal{C}(A, -) \Rightarrow F$ commutes with post-composition:

Theorem (Yoneda Commutativity): F(f)(α_A(id_A)) = α_B(f ∘ id_A) = α_B(f)
Status: Both paths commute in Set. Every natural transformation is uniquely determined by α_A(id_A).

2. Functor Composition & Associativity

Covariant functor $F: \mathcal{C} \to \mathcal{D}$ preserves composition: $F(g \circ f) = F(g) \circ F(f)$.

Functor Axiom: F(g ∘ f) = F(g) ∘ F(f) with F(id_A) = id_{F(A)}
Verification: Preserves identity and composition laws under the Curry-Howard morphism mapping.