5
$\begingroup$

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:

liftFam' : {A : Type} {x y : A} {B : A → Type} (u : B x) (p : x ≡ y) → (x , u) ≡ (y , (transp (λ i → B (p i)) i0) u)
liftFam' u p = {!!}

But, I get the following error upon trying to load the document:

Cannot instantiate the metavariable _219 to solution B (p i1)
since it contains the variable p
which is not in scope of the metavariable
when checking that the expression transp (λ i → B (p i)) i0 u has
type _B_219 y

Can anybody give some advice on what the problem is?

$\endgroup$

2 Answers 2

2
$\begingroup$

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 Agda is confused about the type of the dependent pair (which should be Σ A B, but you didn't in any way indicate that). In usual cases Agda should infer that by looking at the types on both sides of the equality. The further complication of transp completely threw Agda off, so it is reporting something seemingly unrelated to the core error.

$\endgroup$
2
  • $\begingroup$ _≡_ {A = Σ _ B} is more neatly written Path (Σ _ B). $\endgroup$
    – HTNW
    Jun 5, 2022 at 21:09
  • $\begingroup$ @HTNW Right, I forgot we are in cubical Agda. $\endgroup$
    – Trebor
    Jun 6, 2022 at 4:36
1
$\begingroup$

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 parentheses on the right hand side:

(x , u) ≡ _,_ {B = B} y (transp (λ i → B (p i)) i0 u)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.