The following pages link to HoTT (Q27040):
Displaying 20 items.
- Homotopy type theory in Lean (Q1687770) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Categoricity results and large model constructions for second-order ZF in dependent type theory (Q2319994) (← links)
- Formalizing abstract computability: Turing categories in Coq (Q2333325) (← links)
- Internal languages of finitely complete \((\infty , 1)\)-categories (Q2414596) (← links)
- Idempotents in intensional type theory (Q2974780) (← links)
- Quotienting the delay monad by weak bisimilarity (Q4559601) (← links)
- Foundations of dependent interoperability (Q4577812) (← links)
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory (Q4640312) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- Semantics of higher inductive types (Q4958656) (← links)
- (Q5031679) (← links)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
- Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
- Synthetic topology in Homotopy Type Theory for probabilistic programming (Q5055499) (← links)
- The Marriage of Univalence and Parametricity (Q5056401) (← links)
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (Q5079726) (← links)
- Extensional constructive real analysis via locators (Q5156769) (← links)
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY (Q5241229) (← links)
- Category Theory in Coq 8.5 (Q5369495) (← links)
