Skip to main content

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
2 votes
0 answers
119 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 ...
Cheery's user avatar
  • 721
1 vote
0 answers
137 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 ...
blueberry's user avatar
  • 111
6 votes
1 answer
354 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", ...
Naïm Favier's user avatar
2 votes
1 answer
119 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 ...
Trebor's user avatar
  • 3,867
9 votes
1 answer
272 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 "...
Russoul's user avatar
  • 345
1 vote
0 answers
127 views

Cartesian cubical interval with reversal?

Background: cartesian cubical type theory (supports i = j as restriction, where i and j are ...
ice1000's user avatar
  • 6,144
8 votes
1 answer
222 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 (...
ice1000's user avatar
  • 6,144
3 votes
1 answer
97 views

Core language representation of path application with extension types

Suppose I have a concat function with a signature using extension types: ...
ice1000's user avatar
  • 6,144
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 ...
ice1000's user avatar
  • 6,144
3 votes
1 answer
212 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 ...
ice1000's user avatar
  • 6,144
3 votes
1 answer
77 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 ...
ice1000's user avatar
  • 6,144
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 ...
ice1000's user avatar
  • 6,144
4 votes
1 answer
192 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 \...
ice1000's user avatar
  • 6,144
9 votes
1 answer
361 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 (...
Trebor's user avatar
  • 3,867
10 votes
1 answer
291 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:\...
ice1000's user avatar
  • 6,144
9 votes
1 answer
330 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 <...
Joey Eremondi's user avatar
18 votes
2 answers
1k 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/...
Anqur's user avatar
  • 191
8 votes
1 answer
153 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 ...
Joey Eremondi's user avatar
9 votes
2 answers
579 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." ...
Trebor's user avatar
  • 3,867
4 votes
0 answers
173 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 ...
ice1000's user avatar
  • 6,144
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 ...
Guy Coder's user avatar
  • 2,836
26 votes
2 answers
755 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 ...
Trebor's user avatar
  • 3,867