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.

si∣Ui∩Uj=sj∣Ui∩Uj    ⟹    ∃! s∈F(U)  with  s∣Ui=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.