Skip to content
View peterlefanulumsdaine's full-sized avatar
95 followers · 3 following

Achievements

Achievement: Public SponsorAchievement: YOLOAchievement: StarstruckAchievement: Arctic Code Vault ContributorAchievement: Pull Sharkx2

Achievements

Achievement: Public SponsorAchievement: YOLOAchievement: StarstruckAchievement: Arctic Code Vault ContributorAchievement: Pull Sharkx2

Highlights

  • Pro
Block or Report

Block or report peterlefanulumsdaine

Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

Stars

Type: All
Language
Sort by: Recently starred
Showing results

PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.

Python 136 23 Updated Jul 19, 2024

ericries / tom-lehrer

Complete archive of Tom Lehrer's songs, sheet music, and web content following his 2022 public domain release

HTML 6 Updated Jan 17, 2023

michaelt / martin-lof

papers of Per Martin Löf

TeX 738 64 Updated Jan 30, 2024

tvdstaaij / telegram-history-dump

Backup Telegram chat logs using telegram-cli

Ruby 655 85 Updated Oct 1, 2020

peterlefanulumsdaine / higher-inductive-paper

Paper in progress

TeX 7 Updated Apr 21, 2019

fsieczkowski / System-T

Formalisation of Goedel's System T in Coq

Coq 15 2 Updated Jul 1, 2011

peterlefanulumsdaine / HoTT

Forked from HoTT/Coq-HoTT

Homotopy type theory

Coq 2 Updated Jun 9, 2021

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

Coq 1,231 186 Updated Jul 20, 2024

peterlefanulumsdaine / Homotopy

Forked from andrejbauer/Homotopy

Homotopy theory in Coq.

Verilog 3 1 Updated Dec 5, 2011

andrejbauer / Homotopy

Homotopy theory in Coq.

Verilog 90 8 Updated Mar 26, 2011

peterlefanulumsdaine / Oberwolfach-explorations

collaboration on work in progress

Verilog 15 1 Updated Mar 4, 2011

peterlefanulumsdaine / pllthesis

Fossil record of the growth of my thesis.

TeX 1 Updated Mar 16, 2024

txa / OmegaCats

8 1 Updated Oct 9, 2012