Daniel Rosiak

Mathematician  ·  Developer

Formal reasoning,
from theory to building to play.

I’m a mathematician and a builder. I take ideas from category theory and logic and turn them into things people can use: software, games, books, and research that make formal reasoning usable.

siUiUj=sjUiUj        !sF(U)  with  sUi=sis_i\big|_{U_i \cap U_j} = s_j\big|_{U_i \cap U_j} \;\;\Longrightarrow\;\; \exists!\, s \in \mathcal{F}(U) \ \text{ with }\ s\big|_{U_i} = s_i
Local sections that agree on their overlaps glue into one whole.