# Questions tagged [cubical-type-theory]

Cubical type theory is a version of homotopy type theory in which univalence is not just an axiom but a theorem, hence, since this is constructive, has “computational content”. Cubical type theory models the infinity-groupoid-structure implied by Martin-Löf identity types on constructive cubical sets, whence the name.

15 questions
Filter by
Sorted by
Tagged with
88 views

### Core language representation of path application with extension types

Suppose I have a concat function with a signature using extension types: ...
• 5,037
100 views

### Can we bring unification results under cofibrations outside?

Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do ...
• 5,037
178 views

### Does cubical canonicity imply closed version of regularity?

Clarification of my terminologies: Cubical canonicity: a generalized version of canonicity that the "generated by introduction rules" property holds in, not just closed context, but also ...
• 5,037
65 views

### How does conversion check on partial elements/systems (in terms of cubical) work?

In cubical, hcomp is sometimes normal form, and to conversion check two normal hcomp terms, we need to compare the partial ...
• 5,037
61 views

### How does substitution on partial elements/systems (in terms of cubical) work?

Let h = hcomp (λ j → λ { (i = i1) → x }) u, using Cubical Agda syntax. The equivalent cubicaltt syntax is ...
• 5,037
162 views

• 5,037
216 views

### Case splitting with quotient types in Cubical Agda

I'm getting started with Cubcal Agda and I'm quite confused. I've got a HIT A defined, with a path constructor eq returning <...
710 views

### What are "fibration/cofibration" in type theory and what are their intuitions?

I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/...
• 181
117 views

### Are P x and ▸ ((next P) ⊛ (next x)) equivalent in Guarded Cubical Agda?

In Guarded Cubical Agda there's ▹_ : Set i → Set i and ▸_ : ▹ Set i → Set i. If I've got ...
356 views

### What is the state of the art in proof automation in HoTT/CuTT?

One of the frequent criticisms of HoTT is that it requires a lot of lemmata keeping track of which types are sets/propositions etc. And a frequent counterpoint is "It can be automated." ...
• 3,063
122 views

### Is it possible to have a cubical type theory with pattern matching on the identity path?

We have the lovely dependent pattern matching on refl constructor of identity type in systems like Agda, but the same feature is missing for Cubical Agda. People ...
• 5,037
967 views

### What are the bases for different Proof Assistants?

From the Wikipedia article on Proof Assistant it shows some Proof Assistants are based on Higher Order Logic, (HOL Light) and some are based on Dependent Types, (Coq). Are there any other means upon ...
• 2,786