Question

stuck.md

    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:

    ex : (b₁ b₂ : Bool)(p : b₁ ≡ b₂)(e₁ : ty b₁)(e₂ : ty b₂) → PathP (λ i → ty (p i)) e₁ e₂ 
    ex true true p e₁ e₂ i = transp (λ j → ty (p (i ∧ j))) (~ i) e₁

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.

ex : (b₁ b₂ : Bool)(p : b₁ ≡ b₂)(e₁ : ty b₁)(e₂ : ty b₂) → PathP (λ i → ty (p i)) e₁ e₂ 
ex true true p e₁ e₂ i = transp (λ j → ty (p (i ∧ j))) (~ i) e₁

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.

https://agda.zulipchat.com/#narrow/stream/260790-cubical/topic/.E2.9C.94.20Stuck.20Proof/near/283197935