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.
24
questions
6
votes
0
answers
98
views
What are "empty compositions", and why are they bad?
Empty hcomps and empty systems are often mentioned in the context of cubical type theory, in particular related to the efficiency of evaluation, for example here and here. What exactly are they, and ...
- 4,025
4
votes
2
answers
140
views
Parametricity and data kinds
I am wondering about the MonoMaybe type family from the monad-validation Haskell library written by Alexis King. Its definition ...
- 296
2
votes
0
answers
125
views
Implementation of cubical type theory as described in this paper?
Syntax and Models of Cartesian Cubical Type Theory
I'd like to understand this paper enough to know how to implement cubical type theory. However I'm confused about how cofibrations should be ...
- 731
1
vote
0
answers
144
views
Designing a proof assistant around Cubical
As far as I know, Agda is currently the only "widely popular" theorem prover to have somewhat good HoTT support via it's CubicalTT mode. Now, I understand what has slowed down the addition ...
- 111
6
votes
1
answer
372
views
Is the de Morgan interval Kan?
I often read that the interval in cubical type theory does not have the structure of a Kan cubical set (i.e. is not fibrant), which justifies calling it a "pre-type" or "exo-type", ...
- 296
2
votes
1
answer
126
views
Naive computation of propositional resizing
As far as I know, it is not known whether cubical type theories with propositional resizing admit computational interpretations. But here is an obvious attempt: Turn off universe checking locally, and ...
- 4,025
9
votes
1
answer
290
views
What is the intuition behind the `Glue` type in Cubical Type Theories
I have some clues regarding Glue based on a paper here and the accepted answer here.
The first resource says that Glue "...
- 345
1
vote
0
answers
128
views
Cartesian cubical interval with reversal?
Background: cartesian cubical type theory (supports i = j as restriction, where i and j are ...
- 6,306
8
votes
1
answer
240
views
Termination and confluence -- which goes first?
I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by:
the well-typedness of the clauses (type check)
the coverage of the patterns (...
- 6,306
3
votes
1
answer
98
views
Core language representation of path application with extension types
Suppose I have a concat function with a signature using extension types:
...
- 6,306
5
votes
0
answers
111
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 ...
- 6,306
3
votes
1
answer
216
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 ...
- 6,306
3
votes
1
answer
79
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 ...
- 6,306
2
votes
1
answer
78
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 ...
- 6,306
4
votes
1
answer
193
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 \...
- 6,306