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.

Filter by
Sorted by
Tagged with
3 votes
1 answer
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
5 votes
0 answers
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
3 votes
1 answer
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
3 votes
1 answer
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
2 votes
1 answer
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
4 votes
1 answer
162 views

In (CHM/CCHM) cubical type theory, how to conversion-check face formulae?

In my impression (also according to Amelia in her discord server), some non-syntactically equal face formulae should be definitionally-equal (denoted $\equiv$): $(a = 1 \land b = 1) \equiv (b = 1 \...
  • 5,037
9 votes
1 answer
278 views

Current status of cubical inductive families

I have the impression that cubical type theory hasn't dealt with inductive families yet. But the only source on this matter I can get is this Agda issue. What I've gathered is Agda supports defining (...
  • 3,063
10 votes
1 answer
253 views

How to implement the type checking of `transp` in de Morgan cubical type theory?

I am reading many referential materials and I want to find a proper way to implement it. Suppose the syntax is ${\sf transp}~A~\psi:A~0\to A~1$, where (let's call it "the condition") $A:\...
  • 5,037
9 votes
1 answer
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 <...
17 votes
2 answers
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
8 votes
1 answer
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 ...
9 votes
1 answer
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
4 votes
0 answers
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
29 votes
3 answers
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
23 votes
2 answers
512 views

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

I came across this notion in several places, especially in recent papers that establish important meta-theoretic properties of type theories like CuTT. The entry in nLab focuses on the geometric ...
  • 3,063