Process journal of learning by Attila Vajda

fragments 2025-juli-5

💡

this is fascinating in my experience:

          Light
         /     \
      on       off

Light ≅ 1+1

1 + 1 is 2 is 1 is 0

and it's also a "jewel of abstraction"

Unit ≅ 1 (terminal object) -- has exactly one value () -- wow this sort of stuff is awesome for me! I wondered what is Unit, and it's 🌈 isomorphic to 𝟙 the terminal object !! 😌 🎉

Bool ≅ 1 + 1 (coproduct of two units)

🧂⏳ #intersting #mvp

1 × 1 (product of units)

#🎮 Bag n := Unit × Unit × ... × Unit -- n times

coalgebraic types, coinductive types

Game logic = algebraic types! #🐙🎮

maybe dual? games ≅ algebra

products & sums × +

Π ∑

sum type (1 + 1 + ...) ~ choosing product type (1 × 1 × ...) ~ store simultaneously

#🤯 ~ combinatorics!

Leaf ≅ Beauty + Science
Beauty : Type   -- aesthetic, observable form
Science : Structure × Patterns × Relations  -- multiple layers bundled together

Tao Te Ching ~ Lean4 #mvp #cool

gondolkozás, beszéd, változatosság

structure Változatos (T : Type) :=
(beszéd : T)
(írás : T)
(gondolkozás : T)

inductive Idea
| base (desc : String) : Idea
| connect (i j : Idea) : Idea

⨁🎨

      ●
      │
      ⨁  (coproduct / sum)
    /   \
  ● base"B" ● base"C"

× and + seem like sort of switches as well, like a binary knob you can turn and water flows one way or th other!!! to me these signs look somewhat like switches: i

      ●
      │
      🎨  (coproduct / sum)
     /   \
    ●     ●

+ (sum)
   ──┬──► left flow
     │
     └──► right flow

× (product)
   ──┬──► flow A
     │
   ──┴──► flow B

+ = either/or (like a toggle switch: 🎛️←→→) × = and/with (both channels open)

+ = solo instrument playing one melody line 🎷 or 🎸 × = duet combining harmonies 🎹🎺

def switch {A B : Type} (choice : Bool) (a : A) (b : B) : A ⊕ B :=
if choice then Sum.inl a else Sum.i

def splitter (a : A) (b : B) : A × B := (a, b)

+, disjoint union, local choices, ×, local patches combined

Wait, lim is always a global, a sheaf? That's fascinating! I have an exam question / theme on limits, are you telling me the limits of calculus are also little modular / special ideas of these concepts? And in fact, + and ×?

sums are colimits! #maybe gluing via coproducts (disjoint union)

⨅ ~ ∀ ~ Π ~ ×

⨆ ~ ∃ ~ ∑ ~ +

"small is beautiful"