Pinned Repositories
agda-lvo
large veblen ordinal in agda
Baby-Set-Theory
Coq集合论中文教程
CategoryTheory
A Coq formalization of the textbook Categories and Toposes: Visualized and Explained
Coq-Metaphysics
计算形而上学
Googology
Coq巨大数論
MetaLogic
first-order logic and set theory
MetaZF
Coq集合模型论
ReverseMaths
Coq反推数学
Set-Theory
A formalization of the textbook Elements of Set Theory
USST
A formalization of the proof that GCH implies AC in Cubical Agda.
choukh's Repositories
choukh/Set-Theory
A formalization of the textbook Elements of Set Theory
choukh/Baby-Set-Theory
Coq集合论中文教程
choukh/CategoryTheory
A Coq formalization of the textbook Categories and Toposes: Visualized and Explained
choukh/MetaZF
Coq集合模型论
choukh/agda-lvo
large veblen ordinal in agda
choukh/Coq-Metaphysics
计算形而上学
choukh/Googology
Coq巨大数論
choukh/MetaLogic
first-order logic and set theory
choukh/ReverseMaths
Coq反推数学
choukh/DEST
Double Extension Set Theory in Agda
choukh/HilbertSystem
Formal development of Hilbert style propositional logic in Agda
choukh/StructuralSetTheory
结构化集合论
choukh/USST
A formalization of the proof that GCH implies AC in Cubical Agda.
choukh/agda-mode-vscode
agda-mode on VS Code
choukh/choukh.github.io
choukh/cubical
An experimental library for Cubical Agda
choukh/literate-agda-to-modern-html