From 3999bbdd18346ced0519fbae1bb65541a73ee6fd Mon Sep 17 00:00:00 2001 From: nmvdw Date: Mon, 2 Jan 2017 13:08:36 +0100 Subject: [PATCH] Add files via upload --- FinSets.v | 327 +++++++++++++++++++++++++++++++++++++++ Integers.v | 443 +++++++++++++++++++++++++++++++++++++++++++++++++++++ Mod2.v | 396 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 1166 insertions(+) create mode 100644 FinSets.v create mode 100644 Integers.v create mode 100644 Mod2.v diff --git a/FinSets.v b/FinSets.v new file mode 100644 index 0000000..3b9d2c0 --- /dev/null +++ b/FinSets.v @@ -0,0 +1,327 @@ +Require Import HoTT. +Require Export HoTT. + +Module Export FinSet. + +Private Inductive FinSets (A : Type) : Type := + | empty : FinSets A + | L : A -> FinSets A + | U : FinSets A -> FinSets A -> FinSets A. + +Axiom assoc : forall (A : Type) (x y z : FinSets A), + U A x (U A y z) = U A (U A x y) z. + +Axiom comm : forall (A : Type) (x y : FinSets A), + U A x y = U A y x. + +Axiom nl : forall (A : Type) (x : FinSets A), + U A (empty A) x = x. + +Axiom nr : forall (A : Type) (x : FinSets A), + U A x (empty A) = x. + +Axiom idem : forall (A : Type) (x : A), + U A (L A x) (L A x) = L A x. + +Fixpoint FinSets_rec + (A : Type) + (P : Type) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x) + (x : FinSets A) + {struct x} + : P + := (match x return _ -> _ -> _ -> _ -> _ -> P with + | empty => fun _ => fun _ => fun _ => fun _ => fun _ => e + | L a => fun _ => fun _ => fun _ => fun _ => fun _ => l a + | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => u + (FinSets_rec A P e l u assocP commP nlP nrP idemP y) + (FinSets_rec A P e l u assocP commP nlP nrP idemP z) + end) assocP commP nlP nrP idemP. + +Axiom FinSets_beta_assoc : forall + (A : Type) + (P : Type) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x) + (x y z : FinSets A), + ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (assoc A x y z) + = + (assocP (FinSets_rec A P e l u assocP commP nlP nrP idemP x) + (FinSets_rec A P e l u assocP commP nlP nrP idemP y) + (FinSets_rec A P e l u assocP commP nlP nrP idemP z) + ). + +Axiom FinSets_beta_comm : forall + (A : Type) + (P : Type) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x) + (x y : FinSets A), + ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (comm A x y) + = + (commP (FinSets_rec A P e l u assocP commP nlP nrP idemP x) + (FinSets_rec A P e l u assocP commP nlP nrP idemP y) + ). + +Axiom FinSets_beta_nl : forall + (A : Type) + (P : Type) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x) + (x : FinSets A), + ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (nl A x) + = + (nlP (FinSets_rec A P e l u assocP commP nlP nrP idemP x) + ). + +Axiom FinSets_beta_nr : forall + (A : Type) + (P : Type) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x) + (x : FinSets A), + ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (nr A x) + = + (nrP (FinSets_rec A P e l u assocP commP nlP nrP idemP x) + ). + +Axiom FinSets_beta_idem : forall + (A : Type) + (P : Type) + (e : P) + (l : A -> P) + (u : P -> P -> P) + (assocP : forall (x y z : P), u x (u y z) = u (u x y) z) + (commP : forall (x y : P), u x y = u y x) + (nlP : forall (x : P), u e x = x) + (nrP : forall (x : P), u x e = x) + (idemP : forall (x : A), u (l x) (l x) = l x) + (x : A), + ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (idem A x) + = + idemP x. +End FinSet. + +Definition isIn : forall + (A : Type) + (eq : A -> A -> Bool), + A -> FinSets A -> Bool. +Proof. +intro A. +intro eq. +intro a. +refine (FinSets_rec A _ _ _ _ _ _ _ _ _). + Unshelve. + + Focus 6. + apply false. + + Focus 6. + intro a'. + apply (eq a a'). + + Focus 6. + intro b. + intro b'. + apply (orb b b'). + + Focus 3. + intros. + compute. + reflexivity. + + Focus 1. + intros. + compute. + destruct x. + reflexivity. + destruct y. + reflexivity. + reflexivity. + + Focus 1. + intros. + compute. + destruct x. + destruct y. + reflexivity. + reflexivity. + destruct y. + reflexivity. + reflexivity. + + Focus 1. + intros. + compute. + destruct x. + reflexivity. + reflexivity. + + intros. + compute. + destruct (eq a x). + reflexivity. + reflexivity. +Defined. + +Definition comprehension : forall + (A : Type) + (eq : A -> A -> Bool), + (A -> Bool) -> FinSets A -> FinSets A. +Proof. +intro A. +intro eq. +intro phi. +refine (FinSets_rec A _ _ _ _ _ _ _ _ _). + Unshelve. + + Focus 6. + apply empty. + + Focus 6. + intro a. + apply (if (phi a) then L A a else (empty A)). + + Focus 6. + intro x. + intro y. + apply (U A x y). + + Focus 3. + intros. + compute. + apply nl. + + Focus 1. + intros. + compute. + apply assoc. + + Focus 1. + intros. + compute. + apply comm. + + Focus 1. + intros. + compute. + apply nr. + + intros. + compute. + destruct (phi x). + apply idem. + apply nl. +Defined. + +Definition intersection : forall (A : Type) (eq : A -> A -> Bool), + FinSets A -> FinSets A -> FinSets A. +Proof. +intro A. +intro eq. +intro x. +intro y. +apply (comprehension A eq (fun (a : A) => isIn A eq a x) y). +Defined. + +Definition subset (A : Type) (eq : A -> A -> Bool) (x : FinSets A) (y : FinSets A) : Bool. +Proof. +refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _). + Unshelve. + + Focus 6. + apply x. + + Focus 6. + apply true. + + Focus 6. + intro a. + apply (isIn A eq a y). + + Focus 6. + intro b. + intro b'. + apply (andb b b'). + + Focus 1. + intros. + compute. + destruct x0. + destruct y0. + reflexivity. + reflexivity. + reflexivity. + + Focus 1. + intros. + compute. + destruct x0. + destruct y0. + reflexivity. + reflexivity. + destruct y0. + reflexivity. + reflexivity. + + Focus 1. + intros. + compute. + reflexivity. + + Focus 1. + intros. + compute. + destruct x0. + reflexivity. + reflexivity. + + intros. + destruct (isIn A eq x0 y). + compute. + reflexivity. + compute. + reflexivity. +Defined. + +Definition equal_set (A : Type) (eq : A -> A -> Bool) (x : FinSets A) (y : FinSets A) : Bool + := andb (subset A eq x y) (subset A eq y x). + +Fixpoint eq_nat n m : Bool := + match n, m with + | O, O => true + | O, S _ => false + | S _, O => false + | S n1, S m1 => eq_nat n1 m1 + end. \ No newline at end of file diff --git a/Integers.v b/Integers.v new file mode 100644 index 0000000..325cb9a --- /dev/null +++ b/Integers.v @@ -0,0 +1,443 @@ +Require Import HoTT. +Require Export HoTT. + +Theorem useful : + forall (A B : Type) + (f g : A -> B) + (a a' : A) + (p : a = a') + (q : f a = g a), + transport (fun x => f x = g x) p q = (ap f p)^ @ q @ (ap g p). +Proof. +intros. +induction p. +rewrite transport_1. +rewrite ap_1. +rewrite ap_1. +rewrite concat_p1. +simpl. +rewrite concat_1p. +reflexivity. +Qed. + +Module Export Ints. + +Private Inductive Z : Type0 := +| nul : Z +| succ : Z -> Z +| pred : Z -> Z. + +Axiom inv1 : forall n : Z, n = pred(succ n). +Axiom inv2 : forall n : Z, n = succ(pred n). + +Fixpoint Z_rec + (P : Type) + (a : P) + (s : P -> P) + (p : P -> P) + (i1 : forall (m : P), m = p(s m)) + (i2 : forall (m : P), m = s(p m)) + (x : Z) + {struct x} + : P + := + (match x return _ -> _ -> P with + | nul => fun _ => fun _ => a + | succ n => fun _ => fun _ => s ((Z_rec P a s p i1 i2) n) + | pred n => fun _ => fun _ => p ((Z_rec P a s p i1 i2) n) + end) i1 i2. + +Axiom Z_rec_beta_inv1 : forall + (P : Type) + (a : P) + (s : P -> P) + (p : P -> P) + (i1 : forall (m : P), m = p(s m)) + (i2 : forall (m : P), m = s(p m)) + (n : Z) + , ap (Z_rec P a s p i1 i2) (inv1 n) = i1 (Z_rec P a s p i1 i2 n). + +Axiom Z_rec_beta_inv2 : forall + (P : Type) + (a : P) + (s : P -> P) + (p : P -> P) + (i1 : forall (m : P), m = p(s m)) + (i2 : forall (m : P), m = s(p m)) + (n : Z) + , ap (Z_rec P a s p i1 i2) (inv2 n) = i2 (Z_rec P a s p i1 i2 n). + +Fixpoint Z_ind + (P : Z -> Type) + (a : P nul) + (s : forall (n : Z), P n -> P (succ n)) + (p : forall (n : Z), P n -> P (pred n)) + (i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m)) + (i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m)) + (x : Z) + {struct x} + : P x + := + (match x return _ -> _ -> P x with + | nul => fun _ => fun _ => a + | succ n => fun _ => fun _ => s n ((Z_ind P a s p i1 i2) n) + | pred n => fun _ => fun _ => p n ((Z_ind P a s p i1 i2) n) + end) i1 i2. + +Axiom Z_ind_beta_inv1 : forall + (P : Z -> Type) + (a : P nul) + (s : forall (n : Z), P n -> P (succ n)) + (p : forall (n : Z), P n -> P (pred n)) + (i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m)) + (i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m)) + (n : Z) + , apD (Z_ind P a s p i1 i2) (inv1 n) = i1 n (Z_ind P a s p i1 i2 n). + +Axiom Z_ind_beta_inv2 : forall + (P : Z -> Type) + (a : P nul) + (s : forall (n : Z), P n -> P (succ n)) + (p : forall (n : Z), P n -> P (pred n)) + (i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m)) + (i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m)) + (n : Z) + , apD (Z_ind P a s p i1 i2) (inv2 n) = i2 n (Z_ind P a s p i1 i2 n). + +End Ints. + +Definition negate : Z -> Z. +Proof. +intro x. +refine (Z_rec _ _ _ _ _ _ x). + Unshelve. + Focus 1. + apply nul. + + Focus 3. + apply pred. + + Focus 3. + apply succ. + + Focus 2. + apply inv1. + + apply inv2. +Defined. + +Definition plus : Z -> Z -> Z. +Proof. +intro x. +refine (Z_rec _ _ _ _ _ _). + Unshelve. + Focus 1. + apply x. + + Focus 3. + apply succ. + + Focus 3. + apply pred. + + Focus 1. + apply inv1. + + apply inv2. +Defined. + +Definition minus (x : Z) (y : Z) := plus x (negate y). + +Definition Z_to_S : Z -> S1. +Proof. +refine (Z_rec _ _ _ _ _ _). + Unshelve. + + Focus 1. + apply base. + + Focus 3. + intro x. + apply x. + + Focus 3. + intro x. + apply x. + + Focus 1. + intro m. + compute. + reflexivity. + + refine (S1_ind _ _ _). + Unshelve. + + Focus 2. + apply loop. + + rewrite useful. + rewrite ap_idmap. + rewrite concat_Vp. + rewrite concat_1p. + reflexivity. +Defined. + +Lemma eq1 : ap Z_to_S (inv1 (pred (succ (pred nul)))) = reflexivity base. +Proof. +rewrite Z_rec_beta_inv1. +reflexivity. +Qed. + + +Lemma eq2 : ap Z_to_S (ap pred (inv2 (succ (pred nul)))) = loop. +Proof. +rewrite <- ap_compose. +enough (forall (n m : Z) (p : n = m), ap Z_to_S p = ap (fun n : Z => Z_to_S(pred n)) p). + Focus 2. + compute. + reflexivity. + + rewrite Z_rec_beta_inv2. + compute. + reflexivity. +Qed. + +Module Export AltInts. + +Private Inductive Z' : Type0 := +| positive : nat -> Z' +| negative : nat -> Z'. + +Axiom path : positive 0 = negative 0. + +Fixpoint Z'_ind + (P : Z' -> Type) + (po : forall (x : nat), P (positive x)) + (ne : forall (x : nat), P (negative x)) + (i : path # (po 0) = ne 0) + (x : Z') + {struct x} + : P x + := + (match x return _ -> P x with + | positive n => fun _ => po n + | negative n => fun _ => ne n + end) i. + +Axiom Z'_ind_beta_inv1 : forall + (P : Z' -> Type) + (po : forall (x : nat), P (positive x)) + (ne : forall (x : nat), P (negative x)) + (i : path # (po 0) = ne 0) + , apD (Z'_ind P po ne i) path = i. +End AltInts. + +Definition succ_Z' : Z' -> Z'. +Proof. +refine (Z'_ind _ _ _ _). + Unshelve. + Focus 2. + intro n. + apply (positive (S n)). + + Focus 2. + intro n. + induction n. + apply (positive 1). + + apply (negative n). + + simpl. + rewrite transport_const. + reflexivity. +Defined. + +Definition pred_Z' : Z' -> Z'. +Proof. +refine (Z'_ind _ _ _ _). + Unshelve. + Focus 2. + intro n. + induction n. + apply (negative 1). + + apply (positive n). + + Focus 2. + intro n. + apply (negative (S n)). + + simpl. + rewrite transport_const. + reflexivity. +Defined. + + +Fixpoint Nat_to_Pos (n : nat) : Pos := + match n with + | 0 => Int.one + | S k => succ_pos (Nat_to_Pos k) + end. + +Definition Z'_to_Int : Z' -> Int. +Proof. +refine (Z'_ind _ _ _ _). + Unshelve. + + Focus 2. + intro x. + induction x. + apply (Int.zero). + apply (succ_int IHx). + + Focus 2. + intro x. + induction x. + apply (Int.zero). + apply (pred_int IHx). + + simpl. + rewrite transport_const. + reflexivity. +Defined. + +Definition Pos_to_Nat : Pos -> nat. +Proof. +intro x. +induction x. +apply 1. +apply (S IHx). +Defined. + + +Definition Int_to_Z' (x : Int) : Z'. +Proof. +induction x. +apply (negative (Pos_to_Nat p)). +apply (positive 0). +apply (positive (Pos_to_Nat p)). +Defined. + +Lemma Z'_to_int_pos_homomorphism : + forall n : nat, Z'_to_Int (positive (S n)) = succ_int (Z'_to_Int (positive n)). +Proof. +intro n. +reflexivity. +Qed. + +Lemma Z'_to_int_neg_homomorphism : + forall n : nat, Z'_to_Int (negative (S n)) = pred_int (Z'_to_Int (negative n)). +Proof. +intro n. +reflexivity. +Qed. + +Theorem isoEq1 : forall x : Int, Z'_to_Int(Int_to_Z' x) = x. +Proof. +intro x. +induction x. +induction p. +reflexivity. + +rewrite Z'_to_int_neg_homomorphism. +rewrite IHp. +reflexivity. + +reflexivity. + +induction p. +reflexivity. + +rewrite Z'_to_int_pos_homomorphism. +rewrite IHp. +reflexivity. +Defined. + +Lemma Int_to_Z'_succ_homomorphism : + forall x : Int, Int_to_Z' (succ_int x) = succ_Z' (Int_to_Z' x). +Proof. +simpl. +intro x. +simpl. +induction x. + induction p. + compute. + apply path. + + reflexivity. + + reflexivity. + + induction p. + reflexivity. + + reflexivity. +Qed. + +Lemma Int_to_Z'_pred_homomorphism : + forall x : Int, Int_to_Z' (pred_int x) = pred_Z' (Int_to_Z' x). +Proof. +intro x. +induction x. + induction p. + reflexivity. + + reflexivity. + + reflexivity. + + induction p. + reflexivity. + + reflexivity. + +Qed. + +Theorem isoEq2 : forall x : Z', Int_to_Z'(Z'_to_Int x) = x. +Proof. +refine (Z'_ind _ _ _ _). + Unshelve. + + Focus 2. + intro x. + induction x. + reflexivity. + rewrite Z'_to_int_pos_homomorphism. + rewrite Int_to_Z'_succ_homomorphism. + rewrite IHx. + reflexivity. + + Focus 2. + intro x. + induction x. + apply path. + rewrite Z'_to_int_neg_homomorphism. + rewrite Int_to_Z'_pred_homomorphism. + rewrite IHx. + reflexivity. + + simpl. + rewrite useful. + rewrite concat_p1. + rewrite ap_idmap. + + enough (ap (fun x : Z' => Z'_to_Int x) path = reflexivity Int.zero). + rewrite ap_compose. + rewrite X. + apply concat_1p. + + apply axiomK_hset. + apply hset_int. +Defined. + +Theorem adj : + forall x : Z', isoEq1 (Z'_to_Int x) = ap Z'_to_Int (isoEq2 x). +Proof. +intro x. +apply hset_int. +Defined. + +Definition isomorphism : IsEquiv Z'_to_Int. +Proof. +apply (BuildIsEquiv Z' Int Z'_to_Int Int_to_Z' isoEq1 isoEq2 adj). +Qed. \ No newline at end of file diff --git a/Mod2.v b/Mod2.v new file mode 100644 index 0000000..26e5304 --- /dev/null +++ b/Mod2.v @@ -0,0 +1,396 @@ +Require Import HoTT. +Require Export HoTT. + +Theorem useful : + forall (A B : Type) + (f g : A -> B) + (a a' : A) + (p : a = a') + (q : f a = g a), + transport (fun x => f x = g x) p q = (ap f p)^ @ q @ (ap g p). +Proof. +intros. +induction p. +rewrite transport_1. +rewrite ap_1. +rewrite ap_1. +rewrite concat_p1. +simpl. +rewrite concat_1p. +reflexivity. +Qed. + +Module Export modulo. + +Private Inductive Mod2 : Type0 := + | Z : Mod2 + | succ : Mod2 -> Mod2. + +Axiom mod : Z = succ(succ Z). + +Fixpoint Mod2_ind + (P : Mod2 -> Type) + (a : P Z) + (s : forall (n : Mod2), P n -> P (succ n)) + (mod' : mod # a = s (succ Z) (s Z a)) + (x : Mod2) + {struct x} + : P x + := + (match x return _ -> P x with + | Z => fun _ => a + | succ n => fun _ => s n ((Mod2_ind P a s mod') n) + end) mod'. + +Axiom Mod2_ind_beta_mod : forall + (P : Mod2 -> Type) + (a : P Z) + (s : forall (n : Mod2), P n -> P (succ n)) + (mod' : mod # a = s (succ Z) (s Z a)) + , apD (Mod2_ind P a s mod') mod = mod'. + +Fixpoint Mod2_rec + (P : Type) + (a : P) + (s : P -> P) + (mod' : a = s (s a)) + (x : Mod2) + {struct x} + : P + := + (match x return _ -> P with + | Z => fun _ => a + | succ n => fun _ => s ((Mod2_rec P a s mod') n) + end) mod'. + +Axiom Mod2_rec_beta_mod : forall + (P : Type) + (a : P) + (s : P -> P) + (mod' : a = s (s a)) + , ap (Mod2_rec P a s mod') mod = mod'. + +End modulo. + +Module Export moduloAlt. + +Private Inductive Mod2A : Type0 := + | ZA : Mod2A + | succA : Mod2A -> Mod2A. + +Axiom modA : forall n : Mod2A, n = succA(succA n). + +Fixpoint Mod2A_ind + (P : Mod2A -> Type) + (z : P ZA) + (s : forall n : Mod2A, P n -> P (succA n)) + (mod' : forall (n : Mod2A) (a : P n), + modA n # a = s (succA n) (s n a)) + (x : Mod2A) + {struct x} + : P x + := + (match x return _ -> P x with + | ZA => fun _ => z + | succA n => fun _ => s n ((Mod2A_ind P z s mod') n) + end) mod'. + + +Axiom Mod2A_ind_beta_mod : forall + (P : Mod2A -> Type) + (z : P ZA) + (s : forall n : Mod2A, P n -> P (succA n)) + (mod' : forall (n : Mod2A) (a : P n), + modA n # a = s (succA n) (s n a)) + (n : Mod2A) + , apD (Mod2A_ind P z s mod') (modA n) = mod' n (Mod2A_ind P z s mod' n). + +Fixpoint Mod2A_rec + (P : Type) + (z : P) + (s : P -> P) + (mod' : forall (a : P), + a = s (s a)) + (x : Mod2A) + {struct x} + : P + := + (match x return _ -> P with + | ZA => fun _ => z + | succA n => fun _ => s ((Mod2A_rec P z s mod') n) + end) mod'. + +Axiom Mod2A_rec_beta_mod : forall + (P : Type) + (z : P) + (s : P -> P) + (mod' : forall (a : P), + a = s (s a)) + (n : Mod2A) + , ap (Mod2A_rec P z s mod') (modA n) = mod' (Mod2A_rec P z s mod' n). + +End moduloAlt. + +Definition negate : Mod2 -> Mod2. +Proof. +refine (Mod2_ind _ _ _ _). + Unshelve. + Focus 2. + apply (succ Z). + + Focus 2. + intros. + apply (succ H). + + simpl. + rewrite transport_const. + rewrite <- mod. + reflexivity. +Defined. + +Theorem modulo2 : forall n : Mod2, n = succ(succ n). +Proof. +refine (Mod2_ind _ _ _ _). + Unshelve. + Focus 2. + apply mod. + + Focus 2. + intro n. + intro p. + apply (ap succ p). + + simpl. + rewrite useful. + rewrite ap_idmap. + rewrite concat_Vp. + rewrite concat_1p. + rewrite ap_compose. + reflexivity. +Defined. + +Definition plus : Mod2 -> Mod2 -> Mod2. +Proof. +intro n. +refine (Mod2_ind _ _ _ _). + Unshelve. + + Focus 2. + apply n. + + Focus 2. + intro m. + intro k. + apply (succ k). + + simpl. + rewrite transport_const. + apply modulo2. +Defined. + +Definition Bool_to_Mod2 : Bool -> Mod2. +Proof. +intro b. +destruct b. + apply (succ Z). + + apply Z. +Defined. + +Definition Mod2_to_Bool : Mod2 -> Bool. +Proof. +refine (Mod2_ind _ _ _ _). + Unshelve. + Focus 2. + apply false. + + Focus 2. + intro n. + apply negb. + + Focus 1. + simpl. + apply transport_const. +Defined. + +Theorem eq1 : forall n : Bool, Mod2_to_Bool (Bool_to_Mod2 n) = n. +Proof. +intro b. +destruct b. + Focus 1. + compute. + reflexivity. + + compute. + reflexivity. +Qed. + +Theorem Bool_to_Mod2_negb : forall x : Bool, + succ (Bool_to_Mod2 x) = Bool_to_Mod2 (negb x). +Proof. +intros. +destruct x. + compute. + apply mod^. + + compute. + apply reflexivity. +Defined. + +Theorem eq2 : forall n : Mod2, Bool_to_Mod2 (Mod2_to_Bool n) = n. +Proof. +refine (Mod2_ind _ _ _ _). + Unshelve. + Focus 2. + compute. + reflexivity. + + Focus 2. + intro n. + intro IHn. + symmetry. + transitivity (succ (Bool_to_Mod2 (Mod2_to_Bool n))). + + Focus 1. + symmetry. + apply (ap succ IHn). + + transitivity (Bool_to_Mod2 (negb (Mod2_to_Bool n))). + apply Bool_to_Mod2_negb. + enough (negb (Mod2_to_Bool n) = Mod2_to_Bool (succ n)). + apply (ap Bool_to_Mod2 X). + + compute. + reflexivity. + simpl. + rewrite concat_p1. + rewrite concat_1p. + rewrite useful. + rewrite concat_p1. + rewrite ap_idmap. + rewrite ap_compose. + + enough (ap Mod2_to_Bool mod = reflexivity false). + rewrite X. + simpl. + rewrite concat_1p. + rewrite inv_V. + reflexivity. + + enough (IsHSet Bool). + apply axiomK_hset. + apply X. + apply hset_bool. +Defined. + +Theorem adj : + forall x : Mod2, eq1 (Mod2_to_Bool x) = ap Mod2_to_Bool (eq2 x). +Proof. +intro x. +enough (IsHSet Bool). +apply set_path2. +apply hset_bool. +Defined. + +Definition isomorphism : IsEquiv Mod2_to_Bool. +Proof. +apply (BuildIsEquiv Mod2 Bool Mod2_to_Bool Bool_to_Mod2 eq1 eq2 adj). +Qed. + +Definition Mod2ToMod2A : Mod2 -> Mod2A. +Proof. +refine (Mod2_rec _ _ _ _). + Unshelve. + Focus 2. + apply ZA. + + Focus 2. + apply succA. + + Focus 1. + simpl. + apply modA. + +Defined. + +Definition Mod2AToMod2 : Mod2A -> Mod2. +Proof. +refine (Mod2A_rec _ _ _ _). + Unshelve. + Focus 1. + apply Z. + + Focus 2. + apply succ. + + Focus 1. + intro a. + apply (modulo2 a). +Defined. + +Lemma Mod2AToMod2succA : + forall (n : Mod2A), Mod2AToMod2(succA n) = succ (Mod2AToMod2 n). +Proof. +reflexivity. +Defined. + +Lemma Mod2ToMod2Asucc : + forall (n : Mod2), Mod2ToMod2A(succ n) = succA (Mod2ToMod2A n). +Proof. +reflexivity. +Defined. + + +Theorem eqI1 : forall (n : Mod2), n = Mod2AToMod2(Mod2ToMod2A n). +Proof. +refine (Mod2_ind _ _ _ _). + Unshelve. + Focus 2. + reflexivity. + + Focus 2. + intro n. + intro H. + rewrite Mod2ToMod2Asucc. + rewrite Mod2AToMod2succA. + rewrite <- H. + reflexivity. + + simpl. + rewrite useful. + rewrite ap_idmap. + rewrite concat_p1. + rewrite ap_compose. + rewrite Mod2_rec_beta_mod. + rewrite Mod2A_rec_beta_mod. + simpl. + simpl. + enough (modulo2 Z = mod). + rewrite X. + apply concat_Vp. + + compute. + reflexivity. + +Defined. + +Theorem eqI2 : forall (n : Mod2A), n = Mod2ToMod2A(Mod2AToMod2 n). +Proof. +refine (Mod2A_ind _ _ _ _). + Focus 1. + reflexivity. + + Unshelve. + Focus 2. + intros. + rewrite Mod2AToMod2succA. + rewrite Mod2ToMod2Asucc. + rewrite <- X. + reflexivity. + + intros. + simpl. + rewrite useful. + rewrite ap_idmap. + rewrite ap_compose. + rewrite Mod2A_rec_beta_mod. \ No newline at end of file