dcclogin/cubical-sqrt

experimental

cubical-sqrt

Resources

Basic

• (Paper) Cubical agda: a dependently typed programming language with univalence and higher inductive types
• (Paper) Cubical Type Theory: a constructive interpretation of the univalence axiom

More

• (Paper) Naive cubical type theory
• (Tutorial) A tutorial on implementing De Morgan cubical type theory by Yinsen (Tesla) Zhang
• (Tutorial) Cubical Agda: a cold Introduction by Yinsen (Tesla) Zhang
• (Course) CSCI 8980 Higher-Dimensional Type Theory @ UMN
• (Project) 1lab by Amélia Liao et al.
• (People) Dan Licata's Research
• (Catalog) Maths - Cubical Type Theory (CTT) @ EuclideanSpace
• (Thesis) Higher Inductive Types and Internal Parametricity for Cubical Type Theory by Evan Cavallo

Cartesian Cubical Type Theory

• (Paper) Syntax and Models of Cartesian Cubical Type Theory
• (Project) The red* family of proof assistants
• (Thesis) Computational Semantics of Cartesian Cubical Type Theory by Carlo Angiuli

History of Cubical Type Theory (Evan Cavallo)

Higher-dimensional models

1. [HS98] The groupoid interpretation of type theory Retrospective
2. [AW09] Homotopy theoretic models of identity types
3. [BG12] Topological and Simplicial Models of Identity Types

Formalisms

1. [GG08] The identity type weak factorisation system
2. [BG11] Types are weak ω-groupoids
3. [Voe14] The equivalence axiom and univalent models of type theory
4. [KL12a] The Simplicial Model of Univalent Foundations (after Voevodsky)
5. [VAG+20] UniMath - a computer-checked library of univalent mathematics
6. [Uni13] Homotopy Type Theory: Univalent Foundations of Mathematics
7. [BCP15] Non-Constructivity in Kan Simplicial Sets

Constructivity and computation

1. [LH11] 2-Dimensional Directed Type Theory
2. [LH12] Canonicity for 2-Dimensional Type Theory
3. [BCH13] A model of type theory in cubical sets
4. [CCHM15] Cubical Type Theory: a constructive interpretation of the univalence axiom
5. [AFH18] Paper Cartesian Cubical Computational Type Theory [Slides]
6. [Hub19] Canonicity for Cubical Type Theory
7. [OP18] Axioms for Modelling Cubical Type Theory in a Topos
8. [LOPS18] Internal Universes in Models of Homotopy Type Theory
9. [ABCFHL19] Syntax and Models of Cartesian Cubical Type Theory
10. [CMS20] Unifying Cubical Models of Univalent Type Theory [Slides1] [Slides2]