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
1 vote
1 answer
67 views

`transp` In Agda

I'm still a bit confused about the transp operator in Agda: transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1 Is found ...
fweth's user avatar
  • 227
1 vote
0 answers
41 views

Minimal cubical type theory to do coercion

There are a lot of different versions of cubical type theory and a lot of constructs are introduced: intervals, paths, faces, lines, coe, hcom, v-types, glue-types, com, fcom, ghcom, gcom, box and cap....
Labbekak's user avatar
  • 565
2 votes
1 answer
332 views

Is cubical type theory still consistent with univalent excluded middle and univalent choice?

I want to formalize some undergraduate maths in cubical agda, and learning cubical type theory in the proccess. The problem is that I will need univalent excluded middle and univalent choice (and ...
Borja Sierra's user avatar
8 votes
1 answer
864 views

What does canonicity property mean in Type Theory?

The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property. Would you please explain ...
al pal's user avatar
  • 621
2 votes
2 answers
155 views

Propositional truncation of excluded middle

It is clear to me that it should be impossible to prove : exclMidl = isProp A → ((A) ⊎ (¬ A)) Because it would give deciding oracle for every Proposition. My ...
MJG's user avatar
  • 125
6 votes
1 answer
97 views

Reversing an application of `sym` to `ua` and `isoToEquiv` in cubical type theory

I am proving a kind of structure invariance principle for magmas in Cubical Type Theory with the Agda/Cubical library. This is done by constructing a path between two simple magmas and then ...
sryscad's user avatar
  • 191
5 votes
1 answer
275 views

What does "Kan" mean in "Kan operations"?

I'm studying Cubical Type Theory and I see the word "Kan operations" (ref1, ref2, ref3, and there are many more), which is related to "adding a cap to a tube" (can be also explained as "given a path ...
ice1000's user avatar
  • 940
7 votes
1 answer
470 views

Proof that type does not have decidable equality in Agda

Can one create such function in Agda ? ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g)) ℕ→ℕ-undecidable = ? I am particularly interested in proof using ...
MJG's user avatar
  • 125
7 votes
1 answer
489 views

What should we return when pattern matching on a Path constructor?

Context: Cubical Type Theory Consider a simple HIT, say, an HitInt: ...
ice1000's user avatar
  • 940