Skip to main content
Process journal of learning by Attila Vajda

🐬 Smallproofs

βˆ€  f : A ⟢ B

     e    m   
βˆƒ A ⟢ I ⟢ B


f = m ∘ e

🐚

structure Factorization (A B : Type) :=
  (I : Type)
  (e : A β†’ I) -- epi
  (m : I β†’ B) -- mono
  (f : A β†’ B := m ∘ e)

Factor to basic building blocks (irreducibles), then simplify via a universal arrow.

I am learning about factorisation #

because I noticed I still don't really know what to do with simple calculus equations when I see something to factorise I might not yet know why or how to do it

so I found interesting stuff, for example these factorisation exercises can be designed, with tweakable components,

there is also seem to be abstract foundational meaning to them, for example maybe f = m ∘ e, where an expression is sent to it's prime factors by e, and maybe a universal arrow is found via m. Which stand for epi and monic arrows, so this perhaps has to do with injectivity and surjectivity.

I'm making my own ferment jars πŸ₯¬πŸ₯•πŸ§…πŸŒΏ #

and I am surprised how easy it is, and how beautiful and fun it is to ferment stuff

I blend/ground veggies and herbs with water, and add about a teaspoon of salt to each jarful. Then I pour the mix into jars and leave the jars indoors or outdoors with the lid left loosely on top.