: Mathematician & AI engineer : category theory : universal algebra : topology & sheaf theory : formal verification : foundation-model infrastructure :
now
now: may 2025 — Lean4 formalization (part-time), march 2025 — AMC/AIME Lean4 labeling, august 2024 — Weekly category seminars, march 2024 — Research grant 2024
:: may 2025 — Lean4 formalization (part-time) :: march 2025 — AMC/AIME Lean4 labeling :: august 2024 — Weekly category seminars :: march 2024 — Research grant 2024 ::
affiliations
affiliations: Harmonic, Project Numina, University of Cape Town, University of the Witwatersrand, Kili Technology, Lean Prover community, SAMS
::: Harmonic ::: Project Numina ::: University of Cape Town ::: University of the Witwatersrand ::: Kili Technology ::: Lean Prover community ::: SAMS :::
Notes on topological, lax-topological (semi-topological/solid), and topologically algebraic functors via structured sources/sinks, classical characterizations, and the quantaloid-enriched “topological = total” theorem.
Short primer explaining presheaves, the locality and gluing axioms, and the equalizer diagram that packages the sheaf condition for a topological space.
Hom-sets worked out in any category: hom-functors preserve identities and composition, and detect monos/epis by injectivity - notes for Lean 4 formalisation.
Honours project on free semimodules and their examples. Covers definitions, universal properties, and connections to category theory and universal algebra. Supervised by Prof. G. Janelidze (UCT).
Yoneda lemma for monoids via M-sets: explicit Nat(M(-), X) <-> X bijection, Cayley as a corollary, plus Yoneda embedding and an enriched remark for self-study.
Free algebras as initial objects in C[X]. Example: free vector spaces; the universal-property definition also yields free magmas, free groups, and more.
Exercises in category theory: how modules over a ring and vector spaces over a field can be framed as algebraic categories by extending the operator signatures to handle scalar multiplication.
Monoids and preorders as categories: characterize when they are groupoids (groups/equivalence relations) and when they are skeletons (orders). With examples.