#

univalent-foundations

Here are 12 public repositories matching this topic...

HoTT / HoTT

Homotopy type theory

type-theory homotopy-type-theory univalent-foundations

Updated May 15, 2022
Coq

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory

type-theory cubical-type-theory homotopy-type-theory univalent-foundations

Updated Aug 20, 2021
Haskell

martinescardo / HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda

dependent-types type-theory agda lecture-notes mltt homotopy-type-theory univalent-foundations univalent-mathematics hott-uf martin-lof-type-theory univalence-axiom function-extensionality propositional-truncation univalent-type-theory

Updated Apr 12, 2022
Agda

HoTT-Intro / Agda

Agda formalisation of the Introduction to Homotopy Type Theory

mathematics agda textbook univalence homotopy-type-theory univalent-foundations mathematics-library univalent-mathematics hott-uf univalence-axiom

Updated Nov 27, 2021
Agda

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

type-theory agda ordinal homotopy-type-theory univalent-foundations constructive-mathematics compact-type totally-separated-type injective-type searchable-set univalent-mathematics

Updated May 15, 2022
Agda

UniMath / agda-unimath

Univalent mathematics in Agda

type-theory agda homotopy-type-theory univalent-foundations

Updated May 12, 2022
Makefile

ayberkt / formal-topology-in-UF

Formal Topology in Univalent Foundations (WIP).

topology homotopy-type-theory univalent-foundations univalent-mathematics formal-topologies locale-theory pointless-topology constructive-topology

Updated Dec 24, 2021
CSS

langston-barrett / reed-thesis

My undergradate thesis on coinductive types in univalent type theory

thesis mathematics type-theory category-theory univalence unimath univalent-foundations

Updated May 10, 2018
TeX

forked-from-1kasper / bravo

Castle Bravo: Experimental HoTT Implementation

dependent-types proof-assistant hott theorem-prover type-checker mltt homotopy-type-theory univalent-foundations hott-uf

Updated May 15, 2022
OCaml

AnthonyBordg / UniLab

Formalized Mathematics

dependent-types coq-formalization unimath univalent-foundations

Updated Nov 9, 2017
Coq

raghnysh / ufcoq

This project is an effort to formalise small parts of mathematics over the univalent foundations in the framework of the Coq proof assistant. It is mainly for my personal education.

coq homotopy-type-theory univalent-foundations formalisation

Updated May 11, 2022
Coq

CelestialCry / Univalent-Foundations

Univalent Foundations in Agda

agda univalent-foundations

Updated Oct 14, 2020
Agda

Improve this page

Add a description, image, and links to the univalent-foundations topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the univalent-foundations topic, visit your repo's landing page and select "manage topics."