martinescardo / HoTT-UF-Agda-Lecture-Notes Star 219 Code Issues Pull requests 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 16, 2024 Agda
HoTT-Intro / Agda Star 122 Code Issues Pull requests Discussions 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
ivanbakel / coq-antivalence Star 9 Code Issues Pull requests Coq plugin to generate type inequality axioms for inductive definitions coq calculus-of-inductive-constructions univalence-axiom Updated Aug 24, 2020 OCaml
lane-core / kitcat Star 3 Code Issues Pull requests Kitcat is an ergonomic and opinionated 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 Sep 24, 2024 Shell