HoTT
From MaRDI portal
Software:27040
No author found.
Source code repository: https://github.com/HoTT/HoTT
Related Items (20)
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Synthetic topology in Homotopy Type Theory for probabilistic programming ⋮ The Marriage of Univalence and Parametricity ⋮ Quotienting the delay monad by weak bisimilarity ⋮ Foundations of dependent interoperability ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Homotopy type theory in Lean ⋮ Idempotents in intensional type theory ⋮ Unnamed Item ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Extensional constructive real analysis via locators ⋮ An introduction to univalent foundations for mathematicians ⋮ Semantics of higher inductive types ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY ⋮ Category Theory in Coq 8.5 ⋮ Formalizing abstract computability: Turing categories in Coq
This page was built for software: HoTT
