Section Id.

(* Some results of the paper 

Proof-relevance of families of setoids 
and identity in type theory 
Erik Palmgren 
October 13, 2010 

http://www2.math.uu.se/~palmgren/pfsitt.pdf

*)


Inductive Id (A: Set) (x: A) : A -> Set :=
Id_refl : Id A x x.

(* Paulin-Mohring's elimination rule *)

Fixpoint Id_PM_elim (A:Set)(x:A)
(D: (forall y:A, (forall z: (Id A x y), Set)))
(d: (D x (Id_refl A x)))
(b: A)(c: (Id A x b)) : (D b c)
:= 
match c  return (D _ c) with
| Id_refl  => d
end.

(* The standard Martin-L\u00f6f elimination rule is definable 

Definition  Id_ML_elim:  (forall A:Set, 
(forall C: (forall x y: A, (forall z: (Id A x y), Set)),
(forall d :(forall x:A, (C x x (Id_refl A x))),
(forall a b :A, (forall c: (Id A a b), (C a b c)))))):=
(fun A C d a b c =>
(Id_PM_elim A a (C a) (d a) b c)).  *)
 
(* Alternatively *)

Theorem Id_ML_elim:  (forall A:Set, 
(forall C: (forall x y: A, (forall z: (Id A x y), Set)),
(forall d :(forall x:A, (C x x (Id_refl A x))),
(forall a b :A, (forall c: (Id A a b), (C a b c)))))).
intros.
apply Id_PM_elim.
apply d.
Defined.

(*
Print Id_ML_elim.

Variable A':Set.
Variable C': (forall x y:A', (forall z: (Id A' x y), Set)).
Variable a:A'.
Variable d: (forall x:A', C' x x (Id_refl A' x)).
Eval compute in (Id_ML_elim A' C' d a a (Id_refl A' a)).
*)


Definition Id_symm {A:Set}{a b :A}(c: (Id A a b)): (Id A b a) :=
Id_ML_elim A (fun x y z => (Id A y x)) (fun x=> Id_refl A x) a b c.

Definition Id_trans {A:Set}{a b u:A}(w: (Id A b u))(z:(Id A a b)): (Id A a u)
:= (Id_ML_elim A (fun x y v => ((Id A y u) -> (Id A x u))) 
(fun x=> (fun t => t)) a b z) w.
     
Definition comp  {A:Set}{a b c:A}(w : (Id A b c))(z: (Id A a b)): (Id A a c) 
:= Id_trans w z.

Infix "o":= comp (at level 10). 

Definition id {A:Set}(z:A) := Id_refl A z.

Theorem G1 : 
(forall A:Set, (forall x y: A, (forall z: (Id A x y),
(Id (Id A x y) ((id y) o z) z)))).
intros.
induction z.
apply Id_refl.
Qed.

Theorem G2: 
(forall A:Set, (forall x y: A, (forall z:(Id A x y),
(Id (Id A x y) (z o (id x)) z)))).
intros.
induction z.
unfold comp.
apply Id_refl.
Qed.

Theorem G3:
(forall A:Set, (forall x y: A, (forall z:(Id A x y),
(Id (Id A y y) (z o (Id_symm z)) (id y))))).
intros.
induction z.
apply Id_refl.
Qed.

Theorem G4:
(forall A:Set, (forall x y: A, (forall z:(Id A x y),
(Id (Id A x x) ((Id_symm z) o z) (id x))))).
intros.
induction z.
apply Id_refl.
Qed.


Theorem G5:
(forall A:Set, (forall x y u v:A, 
(forall p: (Id A x y), (forall w: (Id A y u), 
(forall z: (Id A u v),
(Id (Id A x v) ((z o w) o p) (z o (w o p)))))))).
intros.
induction p.
induction w.
induction z.
apply Id_refl.
Qed.

Definition R {A:Set}(B:A -> Set)
{a b: A}(c : (Id A a b))(q: B a) : (B b)
:= (Id_ML_elim A (fun x y z => (B x -> B y)) 
(fun x => (fun t => t)) a b c) q .


Theorem R1: 
(forall A:Set, (forall B: A -> Set,(forall a:A,(forall w: B a,
(Id (B a) (R B (id a) w) w))))).
intros.
apply Id_refl.
Qed.

Theorem R2:
(forall A:Set, (forall B: A -> Set, 
(forall a b c:A,
(forall z: (Id A a b), (forall t: (Id A b c), 
(forall w: (B a),
(Id (B c) (R B t (R B z w)) 
          (R B (t o z) w)))))))).
intros.
induction z.
induction t.
apply Id_refl.
Qed.

Theorem Lemma4_2: (forall A:Set, (forall u:A,
let B: (A-> Set) := (fun x => (Id A u x)) in
(forall a b:A,
(forall z: (Id A a b), (forall v: (Id A u a),
(Id (Id A u b) (R B z v) (z o v))))))). 
intros.
induction z.
induction v.
apply Id_refl.
Qed.


Inductive Sigma (A:Set) (B: A -> Set) :=
pair { prj1:  A ; prj2: B prj1}.


Definition split (A:Set) (B:A-> Set)
 (C: (Sigma A B) ->Set) (z: (Sigma A B))
 (d: (forall x:A,  (forall y: B x, (C (pair A B x y))))) :
 (C z)
:= match z with 
    | (pair a b) => d a b
    end.


(* Hypothesis A: Set.
Hypothesis B: A -> Set.
Definition S:Set := (Sigma A B). *)

Definition D (A:Set)(B: A-> Set)(z z' : (Sigma A B))(q : 
(Id (Sigma A B) z z')) : Set :=
(Sigma (Id A (prj1 A B z) (prj1 A B z')) 
 (fun p => 
        (Id (B (prj1 A B z')) 
            (R B p (prj2 A B z))) 
            (prj2 A B z'))).


Theorem Lemma5_1a : (forall A : Set,(forall B:A -> Set,(forall a a':A, 
(forall b : B a, (forall b': B a', 
(Id (Sigma A B) (pair A B a b) (pair A B a' b')) ->
(Sigma (Id A a a') (fun p => 
        (Id (B a') (R B p b) b')))))))).
intros.
assert (D A B (pair A B a b) (pair A B a' b') H).
apply Id_ML_elim.
intros.
apply split with (C:=(fun x=> (D A B x x (Id_refl (Sigma A B) x)))).
intros.
unfold D.
unfold prj1.
unfold prj2.
apply pair with (prj1:= (Id_refl A x0)).
unfold R.
unfold Id_ML_elim.
unfold Id_PM_elim.
apply Id_refl.
unfold D in H0.
unfold prj1 in H0.
unfold prj2 in H0.
assumption.
Qed.




Theorem Lemma5_1b :(forall A:Set, (forall B: A-> Set, 
(forall a a':A, 
(forall b : B a, (forall b': B a', 
(Sigma (Id A a a') (fun p => 
        (Id (B a') (R B p b) b')))
->
(Id (Sigma A B) (pair A B a b) (pair A B a' b'))))))).
intros.
induction H.
induction prj3.
unfold R in prj4.
unfold Id_ML_elim in prj4.
unfold Id_PM_elim in prj4.
induction prj4.
apply Id_refl.
Qed.