Tag Info

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 ...
• 506
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...
• 6,276
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 ...
Accepted

How to access local definitions in Agda

You can refer to local definitions if the where block is declared as a module: ...
• 2,077
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 ...
• 301
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 ...

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? ...
• 6,276
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. ...
• 982

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 ...
• 4,015

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 ...
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 ...
• 4,015

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. ...
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 ...
• 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 ...
• 6,276

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