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.
11
questions
5
votes
1
answer
364
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 (<...
CommunityBot
- 1
6
votes
1
answer
285
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", ...
- 251
6
votes
1
answer
170
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 (...
- 466
3
votes
1
answer
87
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
95
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:
...
- 5,494
5
votes
2
answers
175
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:
...
- 5,494
9
votes
2
answers
225
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:
...
CommunityBot
- 1
9
votes
1
answer
304
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 (...
- 346
9
votes
1
answer
253
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 <...
- 5,494
8
votes
1
answer
128
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 ...
6
votes
2
answers
92
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:
...
- 5,494