UniMath/agda-unimath

The agda-unimath library

Language: Agda - Size: 28.8 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 261 - Forks: 82

martinescardo/TypeTopology

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

Language: Agda - Size: 17.8 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 261 - Forks: 49

martinescardo/HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

Language: Agda - Size: 5.8 MB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 227 - Forks: 20

ayberkt/formal-topology-in-UF

Formal Topology in Univalent Foundations (WIP).

Language: CSS - Size: 10.5 MB - Last synced at: 4 months ago - Pushed at: almost 3 years ago - Stars: 36 - Forks: 2

amato-gianluca/MyHOTT

My implementation of the HOTT/UF book

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

rahulc29/realizability

Experiments with Realizability in Univalent Type Theory

Language: HTML - Size: 8.21 MB - Last synced at: 4 months ago - Pushed at: 9 months ago - Stars: 18 - 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: 5 days ago - Pushed at: 4 months ago - Stars: 3 - Forks: 1

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: 9 months ago - Pushed at: 9 months ago - Stars: 5 - Forks: 0

fredrik-bakke/forest

Language: Shell - Size: 1.14 MB - Last synced at: 4 months ago - Pushed at: 9 months ago - Stars: 3 - Forks: 0

HoTT-Intro/Agda

Agda formalisation of the Introduction to Homotopy Type Theory

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