-
Stockholm University
- Stockholm, Sweden
- www.peterlefanulumsdaine.com
Highlights
- Pro
Block or Report
Block or report peterlefanulumsdaine
Contact GitHub support about this user’s behavior. Learn more about reporting abuse.
Report abuse-
dedekind-reals Public
Forked from coq-community/dedekind-realsA formalization of the Dedekind reals in Coq
Coq MIT License UpdatedJun 22, 2024 -
TypeTheory Public
Forked from UniMath/TypeTheoryThe mathematical study of type theories, in univalent foundations
Coq UpdatedMay 22, 2024 -
UniMath Public
Forked from UniMath/UniMathThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Coq Other UpdatedMay 9, 2024 -
-
cartmell-thesis Public
HoTT group project to TeXify Cartmell's PhD thesis “Generalised Algebraic Theories and Contextual Categories”
-
lambda Public
Forked from blynn/lambdaNotes on lambda calculus and type theory.
Haskell UpdatedFeb 28, 2023 -
palmgren-archive Public
Research material of Erik Palmgren (1963–2019)
-
largecatmodules Public
Forked from UniMath/largecatmodulesLarge category of modules over monads on top of UniMaths and Display category
Coq UpdatedOct 26, 2022 -
System-T Public
Forked from fsieczkowski/System-TFormalisation of Goedel's System T in Coq
Coq UpdatedAug 28, 2022 -
europroofnet.github.io Public
Forked from EuroProofNet/europroofnet.github.ioSources of the EuroProofNet web site.
Ruby UpdatedMar 24, 2022 -
haskell-challenges Public
Forked from effectfully-ou/haskell-challengesCode challenges to solve with Haskell
Haskell MIT License UpdatedJul 28, 2021 -
general-type-theories Public
A (formalised) general definition of type theories
-
-
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 develo…
OCaml GNU Lesser General Public License v2.1 UpdatedJun 8, 2021 -
A textbook on informal homotopy type theory
TeX UpdatedApr 4, 2020 -
social-distancing-simulator Public
Forked from andrejbauer/social-distancing-simulatorAn artificial simulation of social distancing in the time of an epidemic.
HTML MIT License UpdatedMar 18, 2020 -
-
initiality Public
Forked from guillaumebrunerie/initialityA formalized proof of a version of the initiality conjecture
Agda UpdatedMar 14, 2019 -
UniMath2017-CategoryTheory Public
Category theory group projects at UniMath workshop, Birmingham, Dec 2017
-
-
hott-limits Public
A formalization of (homotopy) limits in Homotopy Type Theory
-
homebrew-xfig Public
Forked from mistydemeo/homebrew-xfigRuby BSD 2-Clause "Simplified" License UpdatedOct 21, 2014 -
cubical Public
Forked from simhu/cubicalImplementation of Univalence in Cubical Sets
Haskell MIT License UpdatedJan 17, 2014 -
Homotopy Public
Forked from andrejbauer/HomotopyHomotopy theory in Coq.
-