Library DiSeL.EqTypeX

From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Module EqualityX.

Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).

Structure mixin_of T := Mixin {op : rel T; _ : axiom op}.
Notation class_of := mixin_of (only parsing).

Section ClassDef.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Definition pack c := @Pack T c T.
Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.

End ClassDef.

Module Exports.
Coercion sort : type >-> Sortclass.
Notation eqTypeX := type.
Notation EqMixinX := Mixin.
Notation EqTypeX T m := (@pack T m).
End Exports.

End EqualityX.
Export EqualityX.Exports.

Section EqualityConversion.

Variable U: eqTypeX.
Definition eq_opX T := EqualityX.op (EqualityX.class T).

Lemma eqxP : Equality.axiom (@eq_opX U).
Proof. by case: U=>s[op a ?]; apply: a. Qed.

Canonical eqMixinX := EqMixin eqxP.
Canonical eqTypeX' := EqType U eqMixinX.

End EqualityConversion.