Namdak Tonpa

I am an independent researcher and the BDFL author of Groupoid Space, a comprehensive framework exploring higher groupoids, homotopy type theory, and foundational structures in mathematics and programming languages for the BEAM ecosystem. My work bridges logic, category theory, and computational mathematics, with a focus on dependent types, groupoid semantics, and infinity structures.

Primary research interests include: higher groupoids, homotopy type theory, dependent type systems, and the design of novel programming languages inspired by foundational mathematicians.

Languages

I design and develop programming languages targeting the Erlang BEAM virtual machine, deeply inspired by the following foundational figures in logic, type theory, concurrency, and mathematics:

Alonzo Church — Lambda calculus and computation
Yves Lafont — Interaction nets and linear logic
Henk Barendregt — Lambda calculus and type theory
Per Martin-Löf — Intuitionistic type theory and dependent types
Christine Paulin-Mohring — Tactical Theorem Prover
Frank Pfenning — Logical frameworks and dependent types
Laurent Schwartz — Distribution theory and functional analysis
Anders Mörtberg — Cubical type theory and constructive mathematics
Urs Schreiber — Higher category theory, cohesion, and differential geometry in type theory

Articles

The following articles form the content of Volume IV of the Groupoid Space book series.

Foundations

Type Theory — [PDF]
Inductive Types — [PDF]
Homotopy Type Theory — [PDF]
Higher Inductive Types — [PDF]
Modalities — [PDF]

Languages

Alonzo Church — [PDF]
Yves Lafont — [PDF]
Felix Bloch — [PDF]
Joe Armstrong — [PDF]
Robin Milner — [PDF]
Henk Barendregt — [PDF]
Per Martin-Löf — [PDF]
Frank Pfenning — [PDF]
Laurent Schwartz — [PDF]
Anders Mörtberg — [PDF]
Urs Schreiber — [PDF]

Mathematics

Algebra vs Geometry — [PDF]
Category Theory — [PDF]
Topos Theory — [PDF]
Categories with Families — [PDF]
Categories with Representable Maps — [PDF]
Abelian Categories — [PDF]
Comprehension Categories — [PDF]
Cosmic Cube — [PDF]
Homotopical Dynamics — [PDF]
Fibered Categories — [PDF]
Chevalley Descent — [PDF]
Local Cartesian Closed Categories — [PDF]
Symmetric Monoidal Categories — [PDF]
Cohesive Topoi — [PDF]
Quillen Model Structure — [PDF]
Grothendieck Schemes — [PDF]
Simplicial Homotopy Theory — [PDF]
Cohomology and Spectra — [PDF]
Grothendieck Yoga — [PDF]

Books

I am the sole author of the Groupoid Space book series, consisting of 8 volumes covering foundational to advanced topics in groupoids, homotopy theory, type theory, and their applications to programming languages.

Volume I — Foundations
Volume II — Theoretical Interpreters
Volume III — Fibrational Provers
Volume IV — Advanced Studies
Volume V — Verification
Volume VI — Formal Philosophy
Volume VII — Introduction to Mind
Volume VIII — Philosophy of Mathematics

All volumes are available at groupoid.space.

Governmental Employments

Director Assistant
State Enterprise "Information Court Systems", Judiciary of Ukraine
Kyiv, Ukraine
April 2026 – present
https://ics.gov.ua

Director of System Analysis Department
State Enterprise "Electronic Health", Ministry of Healthcare of Ukraine
Kyiv, Ukraine
June 2024 – March 2026
https://ehealth.gov.ua

Enterprise Architect
State Enterprise "Infotech", Ministry of Internal Affairs of Ukraine
Kyiv, Ukraine
September 2019 – April 2023
https://infotech.gov.ua

Senior Researcher
National Technical University of Ukraine “Igor Sikorsky Kyiv Polytechnic Institute”
Kyiv, Ukraine
September 2018 – January 2022
https://kpi.edu.ua/

Systems Architect
State Owned Joint-Stock Company Commercial Bank "PrivatBank"
Dnipro, Ukraine
September 2013 – May 2015
https://privatbank.ua

Data sourced from ORCID (0000-0001-7127-8796) and official records. All employments listed under Maksym Sokhatskyi (Namdak Tonpa).

Courses

The following are the most completed and advanced courses from the Groupoid Institute curriculum:

Groupoid Theory and Higher Categories — Completed
Homotopy Type Theory — Advanced module finished
Dependent Type Systems for the BEAM — Full implementation track
Cubical and Cohesive Structures — Completed

Full list and materials: Institute → Courses

Sites

Groupoid Space
groupoid.space — Main research site and book repository.

GitHub
github.com/groupoid • github.com/5HT

Mathstodon
mathstodon.xyz/@5ht

ORCID
0000-0001-7127-8796