Trebor-Huang

I'm an undergrad at Tsinghua University. / I like mathematics and dependent type theory.

Internal cat of a doughnut

Pinned Repositories

ASKL
A simple HTML player for 4K Malody charts.
Language:Python2 2 01
combinator-nbe
Normalization by evaluation of simply typed combinators.
Language:Agda26 3 12
Down-The-Path
Spartan implementation of H.O.T.T.
Language:Python25 5 00
history
History of type theory (Chinese).
Language:TeX320 10 610
HomotopyHistory
Language:Typst22 2 00
ice1000
🧊 A Elbereth Gilthoniel / silivren penna míriel! 🌟
Language:Haskell20 4 12
pure-type-system
A python implementation of Barendregt's pure type system.
Language:Python3 2 00
vscode-btex
VSCode extension for bTeX.
Language:TypeScript20 2 243
vscode-forester
VSCode support for Forester
Language:TypeScript18 4 71
ZFC
An embedding of ZFC into Agda
Language:Agda14 2 11

Trebor-Huang's Repositories

Trebor-Huang/history
History of type theory (Chinese).
Language:TeX320 10 610
Trebor-Huang/combinator-nbe
Normalization by evaluation of simply typed combinators.
Language:Agda26 3 12
Trebor-Huang/Down-The-Path
Spartan implementation of H.O.T.T.
Language:Python25 5 00
Trebor-Huang/HomotopyHistory
Language:Typst22 2 00
Trebor-Huang/ice1000
🧊 A Elbereth Gilthoniel / silivren penna míriel! 🌟
Language:Haskell20 4 12
Trebor-Huang/vscode-btex
VSCode extension for bTeX.
Language:TypeScript20 2 243
Trebor-Huang/vscode-forester
VSCode support for Forester
Language:TypeScript18 4 71
Trebor-Huang/forester-theme
Language:XSLT91
Trebor-Huang/forest
My forest.
Language:Shell8 4 00
Trebor-Huang/clock
The clock from Rain World as an OS X desktop widget
Language:Python7 1 02
Trebor-Huang/elementary
Elementary functions in Lean
Language:Lean4 2 01
Trebor-Huang/at
Effective Algebraic Topology in Haskell
Language:Haskell3 1 0
Trebor-Huang/hexo-banana-forest
A hexo plugin for foresting.
Language:TypeScript3 3 0
Trebor-Huang/CFG-Challenge
A challenge for proof assistants about a particular context-free language.
Language:Agda2 2 0
Trebor-Huang/Numerical-Analysis-Homework
Homework repository for Numerical Analysis course.
Language:TeX2 2 0
Trebor-Huang/stiff-second-order-bvp
A robust adaptive algorithm for stiff second order boundary value problems
Language:Python1 2 0
Trebor-Huang/agda-categories
A new Categories library for Agda
Language:Agda1 0
Trebor-Huang/agda-mode-vscode
agda-mode on VS Code
Language:ReScript1 0
Trebor-Huang/btex
Language:TypeScript1 0
Trebor-Huang/cold_clear_ai_love2d_wrapper
Language:C1 0
Trebor-Huang/cubical
An experimental library for Cubical Agda
Language:Agda1 0
Trebor-Huang/cubical-classics
An attempt towards univalent classical mathematics in Cubical Agda.
Language:Agda1 0
Trebor-Huang/KaTeX
Fast math typesetting for the web.
Language:JavaScript
Trebor-Huang/LieSphereGeometry
An HTML demo for Lie Sphere Geometry
Language:TypeScript2 0
Trebor-Huang/musescore-microtonal-edo-plugin
Microtonal MuseScore plugin to retune notes in any EDO
Language:QML1 0
Trebor-Huang/nbe-for-mltt
Normalization by Evaluation for Martin-Löf Type Theory
Language:OCaml1 0
Trebor-Huang/STLC
Language:Agda2 0
Trebor-Huang/tactics
Language:Agda1 0
Trebor-Huang/Techmino
Techmino is fun! Techmino方块研究所唯一官方仓库
Language:Lua1 0
Trebor-Huang/Trebor-Huang.github.io
Personal Website
Language:JavaScript2 0