Library Beroal.Equality
Equality in Intensional Type Theory
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.
sym_eq is an inverse to itself
sym_eq gives an opposite
Definition sym_eq_opp_right : refl_equal _ = trans_eq eq01 (sym_eq eq01).
Definition sym_eq_opp_left : refl_equal _ = trans_eq (sym_eq eq01) eq01.
refl_equal gives an identity
Check (refl_equal _) : eq01 = trans_eq eq01 (refl_equal _).
Definition refl_equal_identity_left : eq01 = trans_eq (refl_equal _) eq01.
trans_eq is associative
Definition trans_eq_assoc : trans_eq (trans_eq eq01 eq12) eq23
= trans_eq eq01 (trans_eq eq12 eq23).
End groupoid.
= trans_eq eq01 (trans_eq eq12 eq23).
End groupoid.
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].
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
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.
= 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.
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.