Skip to main content
10 votes
Accepted

Termination and confluence -- which goes first?

As you have noticed there is no "natural" way to prove confluence and termination: to prove confluence from local confluence you need termination, but proving termination often depends on ...
Jesper's user avatar
  • 506
7 votes
Accepted

Case splitting with quotient types in Cubical Agda

It means that your implementation of the squash case, let's call it u (where u may refer to i...
ice1000's user avatar
  • 6,276
6 votes
Accepted

Current status of cubical inductive families

I would take a look at Higher inductive types in cubical computational type theory by Evan Cavallo and Bob Harper. This paper provides: A complete set of rules for the formation and computation of ...
Matthew McQuaid's user avatar
6 votes
Accepted

How to access local definitions in Agda

You can refer to local definitions if the where block is declared as a module: ...
András Kovács's user avatar
5 votes
Accepted

Is the de Morgan interval Kan?

Short answer: The interval is not fibrant according to the CCHM definition of Kan fibration which is stronger than the one given in the question. Long answer: Regarding the (non) fibrancy of the ...
aws's user avatar
  • 301
5 votes
Accepted

Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?

These are not equivalent; ▸ ((next P) ⊛ (next x)) is equivalent to ▹ (P x). Hence if it were equivalent to ...
Jonathan Sterling's user avatar
4 votes

Can I use if_then_else on indexed paths in HITs?

Is there a way to write a function like this, in which the result depends on x? ...
ice1000's user avatar
  • 6,276
4 votes
Accepted

Can I use if_then_else on indexed paths in HITs?

When you do pattern matching on a higher inductive type, the cases for the higher constructors must be judgmentally equal to the cases for their faces. ...
Dan Doel's user avatar
  • 982
3 votes

Using induction to define Indexed family of HITs in agda

Use data _-glob : ℕ -> Type where Now you can just do something like H : blabla -> zero -glob. Warning: This is called an ...
Trebor's user avatar
  • 4,015
3 votes

How to access local definitions in Agda

To my knowledge this isn't possible, but you have a couple of options: Declare s and r outside of ...
Joey Eremondi's user avatar
2 votes
Accepted

Agda: Cannot Instantiate Metavariable

TL; DR: Explicitly stating the type of the equality solves the problem: _≡_ {A = Σ _ B} (x , u) (y , transp (λ i → B (p i)) i0 u) I think the main problem is that ...
Trebor's user avatar
  • 4,015
2 votes

Paths Between Quotient Types in Cubical Agda

I have comments inside the code. I am also interested if someone could further simplify the code. Also, keep in mind that your Int has two zeros, a positive one and a negative one. ...
Apostolis Xekoukoulotakis's user avatar
2 votes
Accepted

Agda Error after reload when successfully filling a goal

This is a problem of the implementation of Cubical Agda. The cubical equations are thrown to the constraint solver, and probably (I guess) the goal-filling mechanism only checks the type, not the ...
ice1000's user avatar
  • 6,276
1 vote

Agda: Cannot Instantiate Metavariable

Apart from @Trebor's answer, there is another way to specify the implicit argument: (x , u) ≡ (_,_ {B = B} y (transp (λ i → B (p i)) i0 u)) You may also remove the ...
ice1000's user avatar
  • 6,276

Only top scored, non community-wiki answers of a minimum length are eligible