Defining coercion for proof irrelevant equality

Question

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?

Answer 1

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

Answer 2

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.