# Can I use if_then_else on indexed paths in HITs?

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?

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.

• That makes sense, thanks! Is there a principled way to get around this if I have a proof that if x then true else true is always equal to true? (sadly rewriting does not work with cubical equality yet) Commented Mar 2, 2022 at 9:50
• It depends what exactly you mean. You can use the proof to build p : true ≡ true, and then use p i. But the p you build will probably be essentially q ∙ sym q where q is your proof, so that p is not really different from refl (they will be provably equal, but not judgmentally equal, I think). I get the feeling your example might be simplifying out some details that make your real goals less trivial, though. So maybe this sort of thing is what you want. Commented Mar 2, 2022 at 16:25
• I actually managed to unwind my real goal far enough to provide judgemental equality. I was doing a string comparison and needed to use with str1 ≟ str2 which made the types quite hairy, but it worked out. Looking for judgemental equality set me on the right path, so I will accept this answer :) Commented Mar 2, 2022 at 17:01

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