I'm writing Agda code as I read the HoTT book. I'm stuck on Lemma 2.3.9:
data _≡_ {X : Set} : X -> X -> Set where
refl : {x : X} -> x ≡ x
infix 4 _≡_
-- Lemma 2.1.2
_·_ : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
refl · refl = refl
-- Lemma 2.3.1
transp : {A : Set} {P : A -> Set} {x y : A} -> x ≡ y -> P x -> P y
transp refl f = f
lemma2'3'9 : {A : Set}{P : A -> Set}{x y z : A}{p : x ≡ y}{q : y ≡ z}{u : P x} ->
(transp q (transp p u)) ≡ (transp (p · q) u)
lemma2'3'9 {p = refl} {q = refl} = ?
Type-checking with Adga Emacs Mode gives me the following error:
?0 : transp refl (transp refl u) ≡ transp (refl · refl) u
_X_53 : Set [ at /home/user/prog/agda/sample.agda:12,38-39 ]
———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
P x =< _X_53 (blocked on _X_53)
Questions
Note I wrote a working example of Lemma 2.3.9 in Coq, so I'm assuming it's possible in Agda.
Inductive eq {X:Type} (x: X) : X -> Type :=
| refl : eq x x.
Notation "x = y" := (eq x y)
(at level 70, no associativity)
: type_scope.
Definition eqInd{A} (C: forall x y: A, x = y -> Type) (c: forall x: A, C x x (refl x)) (x y: A): forall p: x = y, C x y p :=
fun xy: x = y => match xy with
| refl _ => c x
end.
Definition dot'{A}{x y: A}: x = y -> forall z: A, y = z -> x = z :=
let D := fun x y: A => fun p: x = y => forall z: A, forall q: y = z, x = z in
let d: forall x, D x x (refl x) := let E: forall x z: A, forall q: x = z, Type := fun x z: A => fun q: x = z => x = z in
let e := fun x => refl x
in fun x z => fun q => eqInd E e x z q
in fun p: x = y => eqInd D d x y p.
(* Lemma 2.1.2 *)
Definition dot{A}{x y z: A}: x = y -> y = z -> x = z :=
fun p: x = y => dot' p z.
Definition id {A} := fun a: A => a.
(* Lemma 2.3.1 *)
Definition transp{A} {P: A -> Type} {x y: A}: x = y -> P x -> P y :=
fun p =>
let D := fun x y: A => fun p: x = y => P x -> P y in
let d: forall x, D x x (refl x) := fun x => id
in eqInd D d x y p.
Lemma L_2_3_9{A}{P: A -> Type}{x y z: A}{p: x = y}{q: y = z}{u: P x}:
transp q (transp p u) = transp (dot p q) u.
Proof.
unfold transp, dot, dot'.
rewrite <- q.
rewrite <- p.
reflexivity.
Qed.
_X_53 is a meta variable, i.e., an unknown part of a term. In order to figure out this unknown part of the term, Agda tries to resolve the meta variable. She does so by looking at the context the meta variable appears in, deriving constraints from this context, and determining possible candidate solutions for the meta variable that meet the constraints.
Among other things, Agda uses meta variables to implement implicit arguments. Each implicit argument is replaced with a meta variable, which Agda then tries to resolve within a context that includes the remaining arguments. This is how values for implicit arguments can be derived from the remaining arguments, for example.
Sometimes Agda is unable to figure out an implicit argument, even though one would think that she should be able to. I.e., Agda is unable to resolve the implicit argument's meta variable. This is when she needs a little assistance, i.e., we have to explicitly specify one or more of the implicit arguments. Which is what @gallais suggests in the comment.
=< compares two types. A =< B means that something of type A can be put where something of type B is required. So, if you have a function that takes a B, you can give it an A and it'll type check. I think that this is mostly used for Agda's sized types. In your case, I think, this can be read as type equality instead.
But back to the error message. Agda fails to find a solution for _X_53. The constraint that needs to be met is P x =< _X_53. If, in your case, =< is type equality, then why doesn't Agda simply set _X_53 to P x?
According to my very limited understanding, the reason is higher-order unification, which is a bit of a - to use a very technical term - capricious and finicky beast. _X_53 isn't the complete truth here. Meta variables can be functions and thus have arguments. According to the Agda debug log, the actual unification problem at hand is to unify _X_53 A P x x and P x. If I remember things correctly, then the two xs in the former are a problem. Take this with a grain of salt, though. I'm not a type theorist.
Long story short, sometimes Agda fails to figure out an implicit argument because unification fails and it's a bit hard to understand why exactly.
Finally, something related: The following article talks a bit about best practices for using implicit arguments: Inference in Agda
Update
I guess the two xs are a problem, because they keep Agda from finding a unique solution to the unification problem. Note that both, λ a b c d. P c and λ a b c d. P d would work for _X_53 in that both would make _X_53 A P x x reduce to P x.