A formalisation of the pigeon theorem in UTT.
-
Updated
Dec 15, 2020 - TeX
#
hott
Here are 26 public repositories matching this topic...
-
Updated
Oct 2, 2018
Write function for one data type, let it work with all sorts of variations of it
-
Updated
Feb 9, 2024 - TypeScript
-
Updated
Dec 17, 2018
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
type-theory
category-theory
agda
uni
hott
univalence
agda-library
homotopy-type-theory
univalent-foundations
univalent-mathematics
martin-lof-type-theory
univalence-axiom
-
Updated
Oct 25, 2024 - Agda
Hurricane: HoTT-I Type System
dependent-types
proof-assistant
hott
theorem-prover
type-checker
mltt
homotopy-type-theory
hott-uf
dependent-type-theory
-
Updated
Mar 21, 2022 - OCaml
Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
-
Updated
Mar 23, 2020 - HTML
Some Notes on Types and Categories.
-
Updated
Aug 23, 2024 - Coq
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.
-
Updated
May 26, 2023 - HTML
Castle Bravo: Experimental HoTT Implementation
dependent-types
proof-assistant
hott
theorem-prover
type-checker
mltt
homotopy-type-theory
univalent-foundations
hott-uf
-
Updated
Jun 16, 2023 - OCaml
Anders: Cubical Type Checker
dependent-types
proof-assistant
cubical-type-theory
type-system
hott
theorem-prover
type-checker
mltt
ctt
homotopy-type-theory
dependent-type-theory
-
Updated
Oct 23, 2023 - OCaml
Proving Ground: Tools for Automated Mathematics
-
Updated
Aug 21, 2018 - Jupyter Notebook
Improve this page
Add a description, image, and links to the hott topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the hott topic, visit your repo's landing page and select "manage topics."