Skip to main content

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.

Filter by
Sorted by
Tagged with
2 votes
0 answers

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 ...
6 votes
1 answer

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 (<...
1 vote
0 answers

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 ...
6 votes
1 answer

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", ...
8 votes
1 answer

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 (...
3 votes
1 answer

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 ...
4 votes
1 answer

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 votes
2 answers

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: ...
9 votes
2 answers

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: ...
9 votes
1 answer

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 (...
9 votes
1 answer

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 <...
8 votes
1 answer

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

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: ...