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.
21
questions
1
vote
0
answers
111
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
320
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", ...
- 171
2
votes
1
answer
105
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 ...
- 3,688
9
votes
1
answer
228
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
124
views
Cartesian cubical interval with reversal?
Background: cartesian cubical type theory (supports i = j as restriction, where i and j are ...
- 5,857
8
votes
1
answer
198
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 (...
- 5,857
3
votes
1
answer
96
views
Core language representation of path application with extension types
Suppose I have a concat function with a signature using extension types:
...
- 5,857
5
votes
0
answers
109
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,857
3
votes
1
answer
206
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,857
3
votes
1
answer
74
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,857
2
votes
1
answer
72
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,857
4
votes
1
answer
186
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,857
9
votes
1
answer
338
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,688
10
votes
1
answer
277
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,857
9
votes
1
answer
290
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 <...
- 773
17
votes
2
answers
906
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
148
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 ...
- 773
9
votes
1
answer
437
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,688
4
votes
0
answers
163
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,857
32
votes
3
answers
1k
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,826
23
votes
2
answers
647
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,688