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
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
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?