Open JasonGross opened 10 years ago
Note that this is still open in trunk-polyproj (though you have to remove the Set Universe Polymorphism
as per #124 to get it to accept the annotated
Definition transport_prod' {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
(z : P a * Q a)
: transport (fun a => P a * Q a) p z = (transport _ p (fst z), transport _ p (snd z))
:= match p as p' return transport (fun a0 => P a0 * Q a0) p' z = (transport P p' (fst z), transport Q p' (snd z)) with
| idpath => idpath
end.
)
Adding an explicit return type (
match p as p' return transport (fun a0 => P a0 * Q a0) p' z = (transport P p' (fst z), transport Q p' (snd z)) with
) fixes the problem.