GitHub topics: mltt
groupoid/groupoid.space
🧊 Інститут формальної математики
Language: TeX - Size: 76.8 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 34 - Forks: 13
groupoid/anders
🧊 Модальний гомотопічний верифікатор математики
Language: OCaml - Size: 14.8 MB - Last synced at: 7 days ago - Pushed at: 12 days ago - Stars: 22 - Forks: 2
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
Language: Agda - Size: 5.8 MB - Last synced at: 13 days ago - Pushed at: about 1 year ago - Stars: 227 - Forks: 20
forked-from-1kasper/anders
Anders: Cubical Type Checker
Language: OCaml - Size: 4.02 MB - Last synced at: 20 days ago - Pushed at: over 1 year ago - Stars: 24 - Forks: 1
forked-from-1kasper/bravo
Castle Bravo: Experimental HoTT Implementation
Language: OCaml - Size: 381 KB - Last synced at: 20 days ago - Pushed at: almost 2 years ago - Stars: 7 - Forks: 1
forked-from-1kasper/hurricane
Hurricane: HoTT-I Type System
Language: OCaml - Size: 44.9 KB - Last synced at: 3 months ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0
keilambda/ttfpi-agda
Formalization of the book "Type Theory and Formal Proof: An Introduction" in Agda
Language: Agda - Size: 60.5 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 3 - Forks: 0
lepton-lang/mltt-type-checker
An MLTT type checker implemented using Saki-Lang
Size: 7.81 KB - Last synced at: 3 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0
kotoromo/IntroAgda
Material para una exposición dada el Miércoles 2 de Marzo del 2023 sobre una introducción a Agda como asistente de pruebas y a la Teoría Homotópica de Tipos.
Language: HTML - Size: 1.14 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
esmolanka/simple-pi
Simplistic implementation of dependently typed lambda calculus
Language: Haskell - Size: 69.3 KB - Last synced at: about 2 years ago - Pushed at: over 8 years ago - Stars: 4 - Forks: 0
