All Questions
Tagged with agda cubical-agda
9
questions
3
votes
0
answers
110
views
Lower bounds in type theory proof assistant with ordinals and universes without axioms
I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024?
My ...
- 279
8
votes
1
answer
240
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 (...
- 6,306
3
votes
1
answer
98
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 ...
- 317
4
votes
1
answer
110
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:
...
- 317
5
votes
2
answers
246
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:
...
- 317
9
votes
2
answers
252
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:
...
- 317
9
votes
1
answer
348
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 <...
- 921
8
votes
1
answer
158
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 ...
- 921
6
votes
2
answers
105
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:
...
- 170