open import Data.Bool
open import Data.Unit
open import Data.Empty
open import Cubical.Core.Everything
ty : Bool → Set
ty false = ⊥
ty true = ⊤
ex : (b₁ b₂ : Bool)(p : b₁ ≡ b₂)(e₁ : ty b₁)(e₂ : ty b₂) → PathP (λ i → ty (p i)) e₁ e₂
ex true true p tt tt i = {! tt !}
I would expect this proof to go though.. but instead I get this error
⊤ !=< ty (p i)
when checking that the expression tt has type ty (p i)
Why doesn't ty (p i) reduce to ⊤ in this case?
p : true ≡ true in this hole and p i0 normalizes to true..
Answer by Dan Doel:
This isn't an available principle. Matching on the endpoints of this path doesn't tell you that the whole path is constant, even though it is in this case.
There's work on an extension of this sort of type theory that would probably allow this. Essentially what you'd do is introduce a generic point along p to match on, which must be either true or false. Then the fact that that generic point is one or the other tells you the whole path is, and this sort of proof works.
And by work I mean papers. I'm not sure anyone's thought about how to get it into Agda. I think it'd make a lot of situations nicer.
This only works because every value of ⊤ is automatically equal. Otherwise you'd have to prove that what you get by transporting is equal to your specified value by a composition or something.