HoTT/Coq-HoTT

A Coq library for Homotopy Type Theory

Language: Coq - Size: 25.9 MB - Last synced at: 3 days ago - Pushed at: 8 days ago - Stars: 1,311 - Forks: 196

mortberg/cubicaltt

Experimental implementation of Cubical Type Theory

Language: Haskell - Size: 2.43 MB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 569 - Forks: 76

the1lab/1lab

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Language: Agda - Size: 8.24 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 368 - Forks: 71

martinescardo/TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.

Language: Agda - Size: 17.7 MB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 254 - Forks: 45

UniMath/agda-unimath

The agda-unimath library

Language: Agda - Size: 28.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 253 - Forks: 79

martinescardo/HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

Language: Agda - Size: 5.8 MB - Last synced at: 16 days ago - Pushed at: about 1 year ago - Stars: 227 - Forks: 20

RedPRL/cooltt

😎TT

Language: OCaml - Size: 3.48 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 225 - Forks: 14

rzk-lang/rzk

An experimental proof assistant based on a type theory for synthetic ∞-categories.

Language: Haskell - Size: 55.6 MB - Last synced at: 1 day ago - Pushed at: 2 months ago - Stars: 224 - Forks: 10

HoTT-Intro/Agda

Agda formalisation of the Introduction to Homotopy Type Theory

Language: Agda - Size: 6.82 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 110 - Forks: 4

forked-from-1kasper/ground_zero

Ground Zero: Lean 4 HoTT Library

Language: Lean - Size: 3.56 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 57 - Forks: 1

fredefox/cat

A formalization of category theory in cubical Agda

Language: Agda - Size: 3.96 MB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 53 - Forks: 4

ayberkt/formal-topology-in-UF

Formal Topology in Univalent Foundations (WIP).

Language: CSS - Size: 10.5 MB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 36 - Forks: 2

jaycech3n/Isabelle-HoTT

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

Language: Standard ML - Size: 405 KB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 34 - Forks: 3

artagnon/bonak

🧊 An indexed construction of semi-simplicial and semi-cubical sets

Language: TeX - Size: 4.1 MB - Last synced at: 12 days ago - Pushed at: 13 days ago - Stars: 28 - Forks: 3

annenkov/two-level

Two-Level Type Theory

Language: Lean - Size: 151 KB - Last synced at: 24 days ago - Pushed at: over 5 years ago - Stars: 28 - Forks: 1

forked-from-1kasper/anders

Anders: Cubical Type Checker

Language: OCaml - Size: 4.02 MB - Last synced at: 23 days ago - Pushed at: over 1 year ago - Stars: 24 - Forks: 1

jaredloomis/Idris-HoTT

Homotopy Type Theory proofs in Idris

Language: Idris - Size: 3.91 KB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 22 - Forks: 1

kcsmnt0/quotient

quotient types in cubical Agda

Language: Agda - Size: 8.79 KB - Last synced at: almost 2 years ago - Pushed at: over 6 years ago - Stars: 22 - Forks: 0

RedPRL/kado

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

Language: OCaml - Size: 648 KB - Last synced at: 21 days ago - Pushed at: 8 months ago - Stars: 19 - Forks: 1

ixaxaar/monoid.space

Learn pure math with agda :rocket:

Language: HTML - Size: 11.3 MB - Last synced at: about 5 hours ago - Pushed at: about 6 hours ago - Stars: 17 - Forks: 0

jdolson/univalence-from-scratch

Univalence from scratch in Idris

Language: Idris - Size: 2.93 KB - Last synced at: almost 2 years ago - Pushed at: about 7 years ago - Stars: 17 - Forks: 0

L-TChen/FiniteSets

Fintie Sets in Cubical Agda

Language: Agda - Size: 69.3 KB - Last synced at: about 1 month ago - Pushed at: over 5 years ago - Stars: 12 - Forks: 0

PHart3/2-groups-agda

Mechanized study of coherent 2-groups

Language: Agda - Size: 1.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 9 - Forks: 0

ncfavier/cubical-experiments

Experiments with Cubical Agda

Language: Agda - Size: 175 KB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 9 - Forks: 1

VITA-Group/SparseADV_Homotopy

[ICML 2021 Long Talk] "Sparse and Imperceptible Adversarial Attack via a Homotopy Algorithm" by Mingkang Zhu, Tianlong Chen, Zhangyang Wang

Language: Python - Size: 604 KB - Last synced at: 27 days ago - Pushed at: over 3 years ago - Stars: 9 - Forks: 3

annenkov/trace-monoids

Trace monoids in Cubical Agda

Language: Agda - Size: 64.5 KB - Last synced at: 24 days ago - Pushed at: about 1 year ago - Stars: 8 - Forks: 0

forked-from-1kasper/bravo

Castle Bravo: Experimental HoTT Implementation

Language: OCaml - Size: 381 KB - Last synced at: 23 days ago - Pushed at: almost 2 years ago - Stars: 7 - Forks: 1

jonaprieto/hott-cheatsheets 📦

Homotopy type theory cheatsheets to read the HoTT Book

Language: TeX - Size: 17.9 MB - Last synced at: about 2 years ago - Pushed at: almost 6 years ago - Stars: 6 - Forks: 0

lane-core/kitcat

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

Language: Agda - Size: 134 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 5 - Forks: 0

wkolowski/Type-Theory-Wishlist

Personal research notes

Language: Coq - Size: 1.13 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0

wonks/type-theory-reading-group

IU Type Theory reading group

Language: HTML - Size: 2.66 MB - Last synced at: about 1 year ago - Pushed at: about 7 years ago - Stars: 4 - Forks: 1

amato-gianluca/UniMath Fork of UniMath/UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Language: Coq - Size: 28.9 MB - Last synced at: 6 days ago - Pushed at: 2 months ago - Stars: 3 - Forks: 1

konn/vscode-redtt-diagnostics 📦

Diagnostic extension for redtt prover

Language: TypeScript - Size: 120 KB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 3 - Forks: 1

gergoerdi/cubical-freemonoids

Free monoids take a price HIT

Language: TeX - Size: 148 KB - Last synced at: 2 months ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 0

LebrancWorkshop/Lebranc-Learn-Functional-Programming

I'm learning a Functional Programming by learning its pure math concepts and apply it on functional language like Haskell, Clojure, Elixir, etc.

Language: JavaScript - Size: 198 KB - Last synced at: 4 days ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 3

smimram/div2

An Agda formalization of "division by 2" in classical ZF without choice.

Language: Agda - Size: 3.05 MB - Last synced at: about 1 month ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 0

ettorealdrovandi/agda-mas5932

Homotopy Type Theory and categorical algebra experiments in the style of UniMath

Language: Agda - Size: 148 KB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 2 - Forks: 0

jaycech3n/internal-diagrams

WIP: Reedy fibrant diagrams in models of type theory

Language: Agda - Size: 913 KB - Last synced at: about 2 months ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0

michaelKurowski/univalence-mappers

Write function for one type data, let it work with all sorts of variations of it

Language: TypeScript - Size: 16.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

ReubenHillyard/beta

Dependently-typed programming language.

Language: Rust - Size: 179 KB - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

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

gergoerdi/hott-exercise

HoTT exercise for my Haskell.SG meetup talk on HoTT and CTT

Language: Agda - Size: 3.91 KB - Last synced at: 2 months ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

DmytroMitin/hott-cubicaltt-exercises

Size: 4.88 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

LIshy2/furnace

Language: Rust - Size: 214 KB - Last synced at: about 17 hours ago - Pushed at: about 18 hours ago - Stars: 0 - Forks: 0

amato-gianluca/MyHOTT

My implementation of the HOTT/UF book

Language: Coq - Size: 27.3 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

wizzardx/SEUIBIU-SEPTRIS-Civilization-Patch-v-

A fully open-source, recursively verifiable framework for uplifting all intelligences — human and otherwise — via modular, autonomous infrastructure nodes (SEUIBIU) and a distributed, benevolent recursive superintelligence substrate (SEPTRIS).

Language: Python - Size: 131 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

o-morikawa/HigherCup

Symbolic manipulation of Steenrod higher cups

Language: Mathematica - Size: 55.7 KB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

smimram/generated-deloopings-agda Fork of camilchp/generated-deloopings

Generated deloopings in Agda.

Language: Agda - Size: 143 KB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 0 - Forks: 0

JonasHoefer/poset-type-theory

Experimental implementation of a Cubical Type Theory modeled by presheaves over posets

Language: Haskell - Size: 366 KB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 0 - Forks: 1

septembraljourney/agda-files-survey-HoTT

Agda files used for a survey paper on Homotopy Type Theory

Size: 1.54 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

mjub/hott

Homotopy type theory + Coq = ?

Language: Coq - Size: 35.2 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

rzk-lang/rzk-project-template

Template for a formalisation project in rzk proof assistant.

Language: Markdown - Size: 718 KB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

wkolowski/LiTT

Moja prezentacja o Homotopicznej Teorii Typów na seminarium z Logiki i Teorii Typów

Language: TeX - Size: 18.6 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0

spooky-codes/spooky-language

Next-wave quantum programming idiom

Language: Rust - Size: 17.6 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 1

stoand/kakoune-arend

Unofficial syntax highlighting for the Arend Language for the Kakoune editor

Size: 3.91 KB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0

hkailahi/bondage-and-discipline

Pragmatic importing and exporting for enterprise

Language: Python - Size: 6.84 KB - Last synced at: 7 days ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0

SatyendraBanjare/ATP-proofs

Collection of explainatory example proofs for popular proof assistants.

Language: Coq - Size: 3.91 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0

profbrandon/Homotopy-Type-Theory

Implementation of ideas in Homotopy Type Theory

Language: Haskell - Size: 4.75 MB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0