Pinned Repositories
bibtex2html
book
A textbook on informal homotopy type theory
checker
an attempt at making a prototype proof checker for experimental purposes
coq-builder
A system of makefiles for building coq and the programs it requires.
coq-tex
Process coq code in a tex file, adding coq's output to the tex file so it appears in the final document.
epkg
Here I present a simple bug fix to epkg, the encap-based generic package manager. The problem was that it was setting the umask before creating files and directories.
Ktheory
formalization of theorems of higher algebraic K-theory
M2
The primary source code repository for Macaulay2
UniMath
A unified approach to formalization of mathematical knowledge based on Univalent Foundations.
VV-C-system-from-a-monad
This repository contains various versions of Voevodsky's paper "C-system of a module over a Jf-relative monad"
DanGrayson's Repositories
DanGrayson/coq-tex
Process coq code in a tex file, adding coq's output to the tex file so it appears in the final document.
DanGrayson/epkg
Here I present a simple bug fix to epkg, the encap-based generic package manager. The problem was that it was setting the umask before creating files and directories.
DanGrayson/ProofGeneral
ProofGeneral, adapted for use with "checker", my prototype proof assistant
DanGrayson/Foundations2
Development of the univalent foundations of mathematics in Coq
DanGrayson/HoTT
Homotopy type theory
DanGrayson/rezk_completion
Rezk completion