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.