# Library Beroal.Equality

Equality in Intensional Type Theory

# Shorthands for eq elimination

Section subst.
Variable t:Type.
Definition subst_as_in := fun (v0:t)
(type_fun : forall right_eq:t, v0=right_eq -> Type)
(v1:t) (eq0:v0=v1) (value : type_fun v0 (refl_equal v0))
=> match eq0 as as0 in _=right_eq
return type_fun right_eq as0
with refl_equal => value end.
Definition subst_in := fun (type_fun:t -> Type) (v0 v1:t)
(eq0:v0=v1) (value:type_fun v0)
=> match eq0 in _=right_eq return type_fun right_eq
with refl_equal => value end.
Definition subst := fun (t0 t1:Type) (eq0:t0=t1) (value:t0)
=> match eq0 in _=right_eq return right_eq
with refl_equal => value end.
End subst.
Implicit Arguments subst_as_in [t v0 v1].
Implicit Arguments subst_in [t v0 v1].
Implicit Arguments subst [t0 t1].
Ltac subst_tac_in type_fun eq0 := refine (subst_in eq0 type_fun _).
Ltac subst_tac_as_in type_fun eq0:= refine (subst_as_in eq0 type_fun _).

# eq is a groupoid with:

• objects: formulas;
• morphisms: proofs of identity of formulas;
• identity morphism: refl_equal;
• composition of morphisms: trans_eq;
• inverse morphism: sym_eq.
Section groupoid.
Variable (t0:Type) (v0 v1 v2 v3:t0)
(eq01:v0=v1) (eq12:v1=v2) (eq23:v2=v3).

sym_eq is an inverse to itself
sym_eq gives an opposite
refl_equal gives an identity
trans_eq is associative
Definition trans_eq_assoc : trans_eq (trans_eq eq01 eq12) eq23
= trans_eq eq01 (trans_eq eq12 eq23).

End groupoid.

# Subst is a functor from groupoid eq to a category of types and functions between types

Section subst_functor.
Variable (sort0:Type) (type_fun:sort0->Type) (t0 t1 t2:sort0)
(v0:type_fun t0) (eq01:t0=t1) (eq12:t1=t2).
Definition subst0 := subst_in type_fun.
Implicit Arguments subst0 [v0 v1].

subst preserves identity
Definition subst_pres_id : v0 = subst0 (refl_equal _) v0.

subst preserves composition
Definition subst_pres_comp : subst0 (trans_eq eq01 eq12) v0
= subst0 eq12 (subst0 eq01 v0).

End subst_functor.

Section subst_mix.
Variable (t0:Type) (v0 v1:t0) (eq01:v0=v1).
Definition subst_mix0
: refl_equal v1 = eq_rect _ (fun v => v=v1) eq01 _ eq01.

Definition subst_mix1
: refl_equal v0 = eq_rect _ (fun v => v0=v) eq01 _ (sym_eq eq01).
End subst_mix.

# subst may be moved around a polymorphic function

Section subst_pair_fr.
Definition pair_fr_ob := fun t:Type => prod t t.
Definition pair_fr_mor := fun (t0 t1:Type) (f:t0->t1) p
=> match p with (a,b) => (f a, f b) end.
Variable (t0 t1:Type) (v0:prod t0 t0) (eq01:t0=t1).
Definition subst_pair_fr
: subst_in pair_fr_ob eq01 v0 = pair_fr_mor _ _ (subst eq01) v0.
End subst_pair_fr.

Section subst_comm_f.
Variable (t0 t1:Type) (eqt:t0=t1) (v0:t0).
Definition f := fun (t:Type) (a:t) => (a, a) : prod t t.
Implicit Arguments f [t].

Definition subst_prod := subst_in (fun t:Type => prod t t).
Implicit Arguments subst_prod [v0 v1].
Definition subst_comm_f : f (subst eqt v0) = subst_prod eqt (f v0).

End subst_comm_f.

Section JMeq.
Require Import Coq.Logic.JMeq.
Variable (t0 t1 t2:Type).

Definition JMeq_constr_diff_types : forall (a:t0) (eqt:t0=t1),
@JMeq t0 a t1 (subst eqt a).

End JMeq.