6
$\begingroup$

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?

$\endgroup$
0

2 Answers 2

4
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ 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) $\endgroup$ Mar 2, 2022 at 9:50
  • $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Mar 2, 2022 at 16:25
  • $\begingroup$ 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 :) $\endgroup$ Mar 2, 2022 at 17:01
4
$\begingroup$

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
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.