Pinned Repositories
cartmell-thesis
HoTT group project to TeXify Cartmell's PhD thesis “Generalised Algebraic Theories and Contextual Categories”
general-type-theories
A (formalised) general definition of type theories
higher-inductive-paper
Paper in progress
Homotopy
Homotopy theory in Coq.
HoTT
Homotopy type theory
hott-limits
A formalization of (homotopy) limits in Homotopy Type Theory
Oberwolfach-explorations
collaboration on work in progress
palmgren-archive
Research material of Erik Palmgren (1963–2019)
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
TypeTheory
The mathematical study of type theories, in univalent foundations
peterlefanulumsdaine's Repositories
peterlefanulumsdaine/general-type-theories
A (formalised) general definition of type theories
peterlefanulumsdaine/palmgren-archive
Research material of Erik Palmgren (1963–2019)
peterlefanulumsdaine/Oberwolfach-explorations
collaboration on work in progress
peterlefanulumsdaine/cartmell-thesis
HoTT group project to TeXify Cartmell's PhD thesis “Generalised Algebraic Theories and Contextual Categories”
peterlefanulumsdaine/hott-limits
A formalization of (homotopy) limits in Homotopy Type Theory
peterlefanulumsdaine/higher-inductive-paper
Paper in progress
peterlefanulumsdaine/Homotopy
Homotopy theory in Coq.
peterlefanulumsdaine/HoTT
Homotopy type theory
peterlefanulumsdaine/pllthesis
Fossil record of the growth of my thesis.
peterlefanulumsdaine/UniMath2017-CategoryTheory
Category theory group projects at UniMath workshop, Birmingham, Dec 2017
peterlefanulumsdaine/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
peterlefanulumsdaine/book
A textbook on informal homotopy type theory
peterlefanulumsdaine/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
peterlefanulumsdaine/cubical
Implementation of Univalence in Cubical Sets
peterlefanulumsdaine/dedekind-reals
A formalization of the Dedekind reals in Coq
peterlefanulumsdaine/europroofnet.github.io
Sources of the EuroProofNet web site.
peterlefanulumsdaine/formalabstracts
peterlefanulumsdaine/haskell-challenges
Code challenges to solve with Haskell
peterlefanulumsdaine/homebrew-xfig
peterlefanulumsdaine/initiality
A formalized proof of a version of the initiality conjecture
peterlefanulumsdaine/lambda
Notes on lambda calculus and type theory.
peterlefanulumsdaine/largecatmodules
Large category of modules over monads on top of UniMaths and Display category
peterlefanulumsdaine/social-distancing-simulator
An artificial simulation of social distancing in the time of an epidemic.
peterlefanulumsdaine/System-T
Formalisation of Goedel's System T in Coq
peterlefanulumsdaine/TypeTheory
The mathematical study of type theories, in univalent foundations