Mechanizing the metaphysics of V

formalized googology in agda

A curated list of awesome skills, hooks, slash-commands, agent orchestrators, applications, and plugins for Claude Code by Anthropic

Open-source, local-first apps.

first-order logic and set theory

An experimental library for Cubical Agda

veblen function in agda

History of type theory (Chinese).

CSS files and a template for using Pandoc to generate standalone HTML files

Lecture notes on univalent foundations of mathematics with Agda

Agda is a dependently typed programming language / interactive theorem prover.

The Agda standard library

A new Categories library for Agda

agda-mode on VS Code

One has no future if one couldn't teach themself.

Choiceless grapher: a common-lisp diagram maker for consequences of the Axiom of Choice. This is a mirror of https://gitlab.common-lisp.net/idimitriou/jeffrey

A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

A Coq library for Homotopy Type Theory

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source

An axiom-free formalization of category theory in Coq for personal study and practical work

Googology in Coq

ChordNova is a powerful open-source chord progression analysis plus generation software with unprecedentedly detailed control over chord trait parameters, that is way above mainstream softwares. Ru…

An encoding of Zermelo-Fraenkel Set Theory in Coq

Tricks you wish the Coq manual told you [maintainer=@tchajed]

Formalization of the Axiom of Choice and its Equivalent Theorems in Coq

Formalization of Axiomatic Set Theory in Coq