The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

By the way, it is sometimes the case that "equality over", as
inherited from cubical type theory, is a more appropriate way to deal
with heterogeneous equality than John Major equality since most of the
time, we want to heterogeneously compare objects in syntactically
different but nevertheless provably equal types, thus not expecting
Uniqueness of Identity of Proofs to come in.

Best,

Hugo Herbelin

----------------------------------------------------------------------
Reserved Notation "x =_{ H } y" (at level 70).
Inductive eq_over {A} (x:A) : forall {B} (y:B), A = B -> Prop :=
  eq_over_refl : x =_{eq_refl} x 
where "x =_{ H } y" := (eq_over x y H).

Import EqNotations.

Lemma eq_over_eq {A A'} {a:A} {a':A'} {H} : a =_{H} a' <-> rew H in a = a'.
Proof.
split; intro H0; now destruct H, H0.
Defined.

Lemma eq_over_homogeneous {A} {a:A} {a':A} : a =_{eq_refl} a' <-> a = a'.
Proof.
exact eq_over_eq.
Defined.

Lemma f_equal_over {A} {B:A->Type} (C:forall {a}, B a -> Type)
  {a a'} {b:B a} {b':B a'} {H:a=a'}
 (H0 : b =_{f_equal B H} b') : C b = C b'.
Proof.
destruct H. simpl in H0.
now apply eq_over_homogeneous in H0 as [].
Defined.

(* and so on *)

On Wed, Nov 03, 2021 at 08:23:22PM +0100, Hugo Herbelin wrote:
> Hi,
> 
> > For what its worth, the reason I first considered this property above is
> > because it appeared necessary in order to prove the following fact 
> > concerning
> > heterogeneous equalities:
> > 
> > Theorem JMeq_f :
> >   forall A (B: A -> Type) (C: A -> Type) (f: forall a, B a) (g: forall a, 
> > C a),
> >     JMeq f g ->
> >     forall x, JMeq (f x) (g x).
> 
> This reminds me of Nicolas Oury's embedding of the extensional
> Calculus of Inductive Constructions into the intensional one [1,2]. As
> far as I can recollect, he convinced himself at some point that your
> theorem was not provable and took it as an axiom.
> 
> Best,
> 
> Hugo Herbelin
> 
> [1] N. Oury, Extensionality in the Calculus of Constructions, TPHOLs'05
> [2] N. Oury, Égalité et filtrage avec types dépendants dans le Calcul
>     des Constructions Inductives, PhD thesis, 2006.