(** 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 *)

Definition sym_eq_inv_self : eq01 = sym_eq (sym_eq eq01).
Proof.
refine (subst_as_in (fun _ as0 => as0 = sym_eq (sym_eq as0)) eq01 _).
simpl.
refine (refl_equal _).
Defined.

(** [sym_eq] gives an opposite *)

Definition sym_eq_opp_right : refl_equal _ = trans_eq eq01 (sym_eq eq01).
Proof.
refine (subst_as_in
	(fun _ as0 => _ = trans_eq as0 (sym_eq as0)) eq01 _).
simpl.
refine (refl_equal _).
Defined.

Definition sym_eq_opp_left : refl_equal _ = trans_eq (sym_eq eq01) eq01.
Proof.
refine (subst_as_in
	(fun _ as0 => refl_equal _ = trans_eq (sym_eq as0) as0) eq01 _).
simpl.
refine (refl_equal _).
Defined.

(** [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.
Proof.
refine (subst_as_in
	(fun _ as0 => as0 = trans_eq (refl_equal _) as0) eq01 _).
simpl.
refine (refl_equal _).
Defined.

(** [trans_eq] is associative *)
Definition trans_eq_assoc : trans_eq (trans_eq eq01 eq12) eq23
	= trans_eq eq01 (trans_eq eq12 eq23).
Proof.
refine (subst_as_in
	(fun _ as0 => trans_eq (trans_eq eq01 eq12) as0
		= trans_eq eq01 (trans_eq eq12 as0)) eq23 _).
simpl.
refine (refl_equal _).
Defined.

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.
Proof.
simpl.
refine (refl_equal _).
Qed.

(** subst preserves composition *)
Definition subst_pres_comp : subst0 (trans_eq eq01 eq12) v0
	= subst0 eq12 (subst0 eq01 v0).
Proof.
refine (subst_as_in
	(fun _ as0 => subst0 (trans_eq eq01 as0) _
		= subst0 as0 (subst0 eq01 _)) eq12 _).
simpl.
refine (refl_equal _).
Qed.

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.
Proof.
refine (subst_as_in
	(fun vv as0 => refl_equal vv
		= eq_rect _ (fun v => v=vv) as0 _ as0)
	eq01 _).
simpl.
refine (refl_equal _).
Qed.

Definition subst_mix1
	: refl_equal v0 = eq_rect _ (fun v => v0=v) eq01 _ (sym_eq eq01).
Proof.
refine (subst_as_in
	(fun _ as0 => refl_equal v0
		= eq_rect _ (fun v => v0=v) as0 _ (sym_eq as0))
	eq01 _).
simpl.
refine (refl_equal _).
Qed.
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.
Proof.
refine (subst_as_in
	(fun _ as0 => subst_in pair_fr_ob as0 v0
		= pair_fr_mor _ _ (subst as0) v0)
	eq01 _).
unfold pair_fr_ob, pair_fr_mor.
simpl.
destruct v0.
refine (refl_equal _).
Qed.
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].
(* subst commutes with f *)
Definition subst_comm_f : f (subst eqt v0) = subst_prod eqt (f v0).
Proof.
refine (subst_as_in
	(fun _ as0 => f (subst as0 _) = subst_prod as0 _) eqt _).
simpl.
refine (refl_equal _).
Defined.

End subst_comm_f.



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

(* compare 'JMeq_constr_diff_types s (Q:S=T)'
	to '{s || Q:S = T} : (s : S) = (s [Q:S = T⟩ : T)'
		in "Altenkirch, McBride, Swierstra. Observational Equality, Now!"
	and to 'JMSubst2'
		in "Oury. Extensionality in the Calculus of Constructions" *)
Definition JMeq_constr_diff_types : forall (a:t0) (eqt:t0=t1),
	@JMeq t0 a t1 (subst eqt a).
Proof.
refine (fun a eqt => _).
refine (subst_as_in (fun t2 eqt0 => @JMeq t0 a t2 (subst eqt0 a)) eqt _).
simpl.
refine (JMeq_refl _).
Qed.

End JMeq.