bond15/stuck.md

Created May 21, 2022 23:24

Star (0) You must be signed in to star a gist
Fork (0) You must be signed in to fork a gist

Learn more about clone URLs
Clone this repository at <script src="https://gist.github.com/bond15/073ba0715e74938af50f11c22b0d5455.js"></script>
Save bond15/073ba0715e74938af50f11c22b0d5455 to your computer and use it in GitHub Desktop.

Question

Raw

    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..

Author

bond15 commented May 22, 2022

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