Can I use if_then_else on indexed paths in HITs?

Question

I want to define a function out of an indexed higher inductive type, and am running into some problems.

Here is a somewhat contrived minimal example of what I'm doing:

{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
  using(_≡_ ; Type)
open import Data.Bool
  using(Bool ; true ; false ; if_then_else_)

data Test : Type₀ where
  point : Test
  loop : Bool → point ≡ point

foo : Test → Bool
foo point = true
foo (loop x i) = if x then true else true

Clearly foo is just a very roundabout way of writing const true, but Agda protests saying:

true != if x then true else true of type Bool
when checking the definition of foo

Is there a way to write a function like this, in which the result depends on x?

Alternatively, is there a reason it should not be possible?

Answer 1

When you do pattern matching on a higher inductive type, the cases for the higher constructors must be judgmentally equal to the cases for their faces. if x then true else true is not judgmentally equal to true, because it is stuck on x.

Answer 2

Is there a way to write a function like this, in which the result depends on x?

foo : Test → Bool
foo point = true
foo (loop false i) = true
foo (loop true i) = true

The logic is equivalent to your original code but is written in a different way.

Alternatively, is there a reason it should not be possible?

The term if x then true else true is a normal form, and it does not reduce to true. In your case in particular, you can simplify your logic in this way:

foo : Test → Bool
foo point = true
foo (loop x i) = true