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.
9
questions
8
votes
1
answer
907
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 ...
- 621
7
votes
1
answer
481
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 ...
- 125
7
votes
1
answer
491
views
What should we return when pattern matching on a Path constructor?
Context: Cubical Type Theory
Consider a simple HIT, say, an HitInt:
...
- 940
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 ...
- 191
5
votes
1
answer
283
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 ...
- 940
2
votes
2
answers
156
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 ...
- 125
2
votes
1
answer
357
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 ...
- 23
1
vote
1
answer
75
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 ...
- 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....
- 565