Library Corelib.Init.Equality
Require Import Notations.
Require Import Ltac.
Create HintDb typeclass_instances discriminated.
Create HintDb rewrite_instances discriminated.
Class Has_refl@{
sa se;
la le} (
eq :
forall A :
Type@{
sa;
la},
A -> A -> Type@{
se;
le})
:=
refl :
forall A x,
eq A x x.
Class Has_J@{
sa se sp;
la le lp} (
eq :
forall A :
Type@{
sa ;
la},
A -> A -> Type@{
se;
le})
(
Has_refl :
Has_refl eq) :=
J_eliminator :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
forall y :
A,
eq A x y -> Type@{
sp ;
lp}),
P x (
refl A x)
-> forall y e,
P y e.
Class Has_J_r@{
sa se sp;
la le lp} (
eq :
forall A :
Type@{
sa ;
la},
A -> A -> Type@{
se;
le})
(
Has_refl :
Has_refl eq) :=
J_r_eliminator:
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
forall y :
A,
eq A y x -> Type@{
sp ;
lp}),
P x (
refl A x)
-> forall y e,
P y e.
Class Has_J_forward@{
sa se sp;
la le lp} (
eq :
forall A :
Type@{
sa ;
la},
A -> A -> Type@{
se;
le})
(
Has_refl :
Has_refl eq) :=
J_forward :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
forall y :
A,
eq A x y -> Type@{
sp ;
lp})
y e,
P y e -> P x (
refl A x).
Class Has_J_r_forward@{
sa se sp;
la le lp} (
eq :
forall A :
Type@{
sa ;
la},
A -> A -> Type@{
se;
le})
(
Has_refl :
Has_refl eq) :=
J_r_forward :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
forall y :
A,
eq A y x -> Type@{
sp ;
lp})
y e,
P y e -> P x (
refl A x).
Class Has_Leibniz@{
sa se sp;
la le lp} (
eq :
forall A :
Type@{
sa ;
la},
A -> A -> Type@{
se;
le}) :=
leibniz :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
A -> Type@{
sp ;
lp}),
P x -> forall y,
eq A x y -> P y.
Class Has_Leibniz_r@{
sa se sp;
la le lp} (
eq :
forall A :
Type@{
sa ;
la},
A -> A -> Type@{
se;
le}) :=
leibniz_r :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
A -> Type@{
sp ;
lp}),
P x -> forall y,
eq A y x -> P y.
Register Has_refl as core.Has_refl.
Typeclasses Opaque Has_refl.
Register Has_J as core.Has_J.
Typeclasses Opaque Has_J.
Register Has_J_r as core.Has_J_r.
Typeclasses Opaque Has_J_r.
Register Has_J_forward as core.Has_J_forward.
Typeclasses Opaque Has_J_forward.
Register Has_J_r_forward as core.Has_J_r_forward.
Typeclasses Opaque Has_J_r_forward.
Register Has_Leibniz as core.Has_Leibniz.
Typeclasses Opaque Has_Leibniz.
Register Has_Leibniz_r as core.Has_Leibniz_r.
Typeclasses Opaque Has_Leibniz_r.
Definition J_no_dep@{
s s' sp;
l l' lp} {
eq} {
refl} (
eqr :
Has_J@{
s s' sp;
l l' lp}
eq refl) :
forall (
A :
Type@{
s ;
l}) (
x :
A) (
P :
A -> Type@{
sp ;
lp}),
P x -> forall y (
e :
eq A x y),
P y :=
fun A x P px y e =>
J_eliminator _ x (
fun y _ =>
P y)
px y e.
Definition Has_J_Has_Leibniz@{
s s' sp;
l l' lp} {
eq} {
refl} (
eqr :
Has_J@{
s s' sp;
l l' lp}
eq refl) :
Has_Leibniz@{
s s' sp;
l l' lp}
eq :=
fun A x P px y e =>
J_no_dep eqr A x P px y e.
Section ap.
Universe la le lb le'.
Context {
eq :
forall A :
Type@{
sa;
la},
A -> A -> Type@{
se;
le} }
{
eq' :
forall A :
Type@{
sb;
lb},
A -> A -> Type@{
se';
le'} }
{
_refl:
Has_refl@{
sb se';
lb le'}
eq'}
{
_leibniz:
Has_Leibniz@{
sa se se';
la le le'}
eq}.
Definition ap [
A :
Type@{
sa;
la}] [
B:
Type@{
sb;
lb}] (
f :
A -> B) [
x y :
A] (
e :
eq _ x y) :
eq' _ (
f x) (
f y) :=
leibniz A x (
fun y =>
eq' B (
f x) (
f y)) (
refl _ _)
y e.
End ap.
Register ap as core.ap.
Section sym.
Universe la le.
Context {
eq :
forall A :
Type@{
sa;
la},
A -> A -> Type@{
se;
le} }
{
A :
Type@{
sa;
la} }
{
_refl:
Has_refl@{
sa se;
la le}
eq}
{
_leibniz:
Has_Leibniz@{
sa se se;
la le le}
eq}.
Definition sym {
x y :
A} (
e :
eq _ x y) :
eq _ y x :=
leibniz _ _ (
fun y =>
eq A y _) (
refl _ _)
_ e.
End sym.
Definition Has_J_Has_J_forward@{
sa se sp;
la le lp}
eq Has_refl
{
has_J :
Has_J@{
sa se sp;
la le lp}
eq Has_refl} :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
forall y :
A,
eq A x y -> Type@{
sp ;
lp})
y e,
P y e -> P x (
refl A x) :=
fun A x P y e =>
J_eliminator _ _ (
fun y e =>
P y e -> P _ _) (
fun x =>
x)
_ _.
Definition _Has_J_Has_J_forward@{
sa se sp;
la le lp}
eq Has_refl
{
has_J :
Has_J@{
sa se sp;
la le lp}
eq Has_refl} :
Has_J_forward@{
sa se sp;
la le lp}
eq Has_refl
:=
Has_J_Has_J_forward _ _.
Hint Resolve _Has_J_Has_J_forward :
rewrite_instances.
Definition Has_J_r_Has_J_r_forward@{
sa se sp;
la le lp}
eq Has_refl
{
has_J :
Has_J_r@{
sa se sp;
la le lp}
eq Has_refl} :
forall (
A :
Type@{
sa ;
la}) (
x :
A) (
P :
forall y :
A,
eq A y x -> Type@{
sp ;
lp})
y e,
P y e -> P x (
refl A x) :=
fun A x P y e =>
J_r_eliminator _ _ (
fun y e =>
P y e -> P _ _) (
fun x =>
x)
_ _.
Definition _Has_J_r_Has_J_r_forward@{
sa se sp;
la le lp}
eq Has_refl
{
has_J :
Has_J_r@{
sa se sp;
la le lp}
eq Has_refl} :
Has_J_r_forward@{
sa se sp;
la le lp}
eq Has_refl
:=
Has_J_r_Has_J_r_forward _ _.
Hint Resolve _Has_J_r_Has_J_r_forward :
rewrite_instances.