Groupoid is doing formalization of mathematics in a cubical type systems.




Mathematical theories, models and systems:

TOC















Languages

Non-dependent languages are targets or runtimes, and dependently typed language are provers.

Runtimes

Runtimes and effect type systems.

31 DEC 2016 — Certified CPS Interpreter
31 DEC 2016 — Intercore SMP Protocol
10 OCT 2016 — Array Processing
10 OCT 2016 — Effect Type System
24 MAY 2018 — Process Type System

Provers

Theorem provers for logic, lambda encodings exploration and homotopy calculus.

10 OCT 2016 — Pure Type System
6 JUL 2018 — Homotopy Type System
19 JAN 2020 — Principia System

Models

Great language should come with a great library.

3 AUG 2018 — Formal Mathematics

Foundation

The examples of HTS base library man pages.

16 JUL 2017 — Pi, Sigma, Path, Proto, Prop, Stream, List, Nat, Maybe, IO, IOI, Bool

Mathematics

The series of notes on Homotopy Theory, Category Theory, Topos Theory, Sheaf Theory and Differential Geometry, formalized in HTS.

10 OCT 2017 — Isomorphism
19 OCT 2017 — Inductive Data Types
20 JUN 2017 — Hopf Fibrations
5 NOV 2017 — Category
20 MAY 2018 — Bundle
25 JUL 2018 — CW Complex
9 AUG 2018 — Formal Set Topos
30 DEC 2018 — Equivalence
13 JAN 2019 — Presheaf Type Theories
15 JAN 2019 — Homotopy Limits
15 JAN 2019 — Differential Geometry
17 JAN 2019 — de Rham Cohesion
22 JAN 2019 — Homology

Notes

The series of articles on foundation and mathematics of Homotopy Type Theory.

Issue I: Internalizing MLTT
Issue III: Homotopy Type Theory
Issue VIII: Formal Set Topos
Addendum I: Pure Type System
Addendum II: Many Faces of Equality