9
$\begingroup$

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try

Inductive seq : Set -> Set -> SProp :=
| srefl : forall (A : Set), seq A A.

Definition coe (A : Set) (B : Set) (hyp : seq A B) (x : A) : B :=
match hyp with
| srefl A => x
end.

which understandably doesn't work because Coq doesn't want me to eliminate SProp into Set. In Agda I try

coe : (A : Set) -> (B : Set) -> .(A ≡ B) -> A -> B
coe A A _ x = x

which I imagine fails for similar reasons.

Yet it seems like such a function should be definable, since A and B are definitionally equal by assumption.

Is there a theoretical reason why such a function cannot be defined (besides design choices in Coq or Agda)? If not, is there a system or theory in which I could safely define such a function?

$\endgroup$
1
  • $\begingroup$ In Agda you can use the @0 annotation instead. $\endgroup$
    – Trebor
    Apr 13 at 2:09

2 Answers 2

5
$\begingroup$

Agda has a runtime irrelevance modality which may be closer to what you want. In particular, since there's only one constructor, it is ok to eliminate the identity type even if it is marked irrelevant. So:

coe : (a b : Set) (@0 eq : a ≡ b) -> a -> b
coe _ _ refl x = x
$\endgroup$
1
  • $\begingroup$ Very cool, thanks! It seems like Idris 2 is based on this idea as well $\endgroup$
    – Couchy
    Apr 13 at 3:17
5
$\begingroup$

In the latest versions of Coq, you can use an irrelevant equality, and eliminate it into Set/Type, see the reference manual. You have however to explicitly allow it, because with the current reduction behaviour definitional proof irrelevance in an impredicative sort of (strict) propositions is non-terminating (see the example by Coquand and Abel).

As far as I know, there are two ways to patch this. You can have a predicative hierarchy of sorts (what Agda does, but not sure how definitional UIP fares there), from what I gathered it is open whether this is normalizing or not, but at least we don’t have any counter-examples. Alternatively, you can replace the inductive equality with observational equality, which behaves much better as a strict proposition. I guess one day Coq will go for this latter, but there’s still quite some way to go, so don’t expect it to land tomorrow.

$\endgroup$
1
  • 1
    $\begingroup$ This is the downside of asking two questions at once :( I think this should be accepted as well. $\endgroup$
    – Trebor
    Apr 13 at 10:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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