Questions tagged [cubical-agda]
The Cubical mode extends Agda with a variety of features from the CHM version of Cubical Type Theory. In particular, computational univalence and higher inductive types which hence gives computational meaning to Homotopy Type Theory and Univalent Foundations.
12
questions
1
vote
0
answers
113
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
324
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
6
votes
1
answer
431
views
Paths Between Quotient Types in Cubical Agda
I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types.
In particular, my quotient type is the integers, quotiented by the absolute value function (<...
- 61
8
votes
1
answer
199
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,877
3
votes
1
answer
93
views
Using induction to define Indexed family of HITs in agda
I am looking to define a family of HITs parametrized by $\mathbb{N}$. I want $(-)$-glob : $\mathbb{N} \to Type$, so that $n$-glob is the n-dimensional glob. I know how to construct the n-$glob$ by ...
- 305
3
votes
1
answer
98
views
Agda Error after reload when successfully filling a goal
So I'm not sure what this error is and I'm not even sure how I would find out. I'm trying to code up a proof that refl is a right identity. I've gotten to this stage:
...
- 305
5
votes
2
answers
198
views
Agda: Cannot Instantiate Metavariable
I'm running into a certain error while trying to code something up in cubical Agda, but I can't understand the error. Here is my code:
...
- 305
9
votes
2
answers
240
views
How to access local definitions in Agda
I'm working in cubical agda. I am wondering how to access local definitions once outside of the local environment. For example, suppose I have the following code:
...
- 305
9
votes
1
answer
340
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
9
votes
1
answer
292
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
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
6
votes
2
answers
99
views
Can I use if_then_else on indexed paths in HITs?
I want to define a function out of an indexed higher inductive type, and am running into some problems.
Here is a somewhat contrived minimal example of what I'm doing:
...
- 160