Last active
December 4, 2025 05:19
-
-
Save lovely-error/238770367c5de06658c67d5dfe5c19a2 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib.Logic.Basic | |
| import Mathlib.Logic.Function.Basic | |
| import Mathlib.Tactic | |
| import Mathlib.Logic.Equiv.Basic | |
| def wmap (A:Sort _)(B:Sort _) : Sort _ := | |
| { p: (A -> B) ×' (B -> A) // ∀ i, p.2 (p.1 i) = i } | |
| def fiber (h:B->A)(a:A) := { b:B // h b = a } | |
| def wtransp : (w:wmap A B) -> ∀ a:A , fiber w.1.2 a := by | |
| intro w i | |
| refine .mk (w.1.1 i) ?_ | |
| apply w.property | |
| @[simp] | |
| def wtransp_eqn_1 (w:wmap A B): (wtransp w k).val = w.1.1 k := by | |
| unfold wtransp | |
| let (.mk (.mk f h) _) := w | |
| simp only | |
| @[simp] | |
| def wtransp_eqn_2 (w:wmap A B): wtransp w i = (.mk (w.1.1 i) (w.property _)) := by | |
| rfl | |
| @[reducible] | |
| def SubstRule1 (h:B->A) := ∀ (a:A), (b:B) ×' (∀ (P:A->Sort _), P (h b) -> P a) | |
| def wsubst (w:wmap A B): SubstRule1 w.1.2 := by | |
| unfold SubstRule1 | |
| intro a | |
| refine .mk ?_ ?_ | |
| exact (wtransp w a).val | |
| intro P | |
| simp only [wtransp_eqn_1] | |
| rw [w.property] | |
| apply id | |
| @[simp] | |
| def wsubst_eqn_1 (w:wmap A B) : (wsubst w i).fst = w.1.1 i := rfl | |
| def mkwmap (f: A->B)(h:B->A)(p: ∀ i, h (f i) = i) : wmap A B := ⟨ ⟨ f , h ⟩ , p ⟩ | |
| def id_wmap : wmap T T := by | |
| refine mkwmap id id ?_ | |
| intro i | |
| rfl | |
| @[simp] | |
| def mkwmap_eqn_1 : mkwmap f h p = .mk (.mk f h) p := rfl | |
| def hmor1 (op1:B->B)(op2:A->A)(p:A->B) := ∀ a1, op1 (p a1) = p (op2 a1) | |
| def hmor2 (op1:B->B->B)(op2:A->A->A)(p:A->B) := ∀ a1 a2, op1 (p a1) (p a2) = p (op2 a1 a2) | |
| def hmor2_exists {A:Sort _}{B:Sort _}(w:wmap A B) (op:A->A->A): | |
| let (.mk (.mk f h) _) := w; | |
| @Subtype (B->B->B) fun opm => (hmor2 op opm h) ∧ | |
| (opm = fun (b1:B) (b2:B) => f (op (h b1) (h b2))) | |
| := by | |
| let (.mk (.mk f h) p1) := w | |
| simp | |
| refine ⟨?val, ?property⟩ | |
| exact fun b1 b2 => | |
| f (op (h b1) (h b2)) | |
| simp at p1 | |
| unfold hmor2 | |
| dsimp | |
| apply And.intro | |
| intro a b | |
| rewrite [(p1 (op (h a) (h b)))] | |
| rfl | |
| rfl | |
| set_option pp.proofs true in | |
| def shift_tr_fun (w:wmap A B)(h1:w.1.1 a = b): w.1.2 b = a := by | |
| let (.mk (.mk f h) p1) := w | |
| dsimp at p1 h1 | |
| dsimp | |
| rw [<-h1] | |
| rw [p1] | |
| @[reducible] | |
| def SubstRule2 {A:Sort _} (a b:A) := ∀ (P:A->Sort _), P a -> P b | |
| def oeq_is_eq : SubstRule2 a b = (a = b) := by | |
| apply propext | |
| apply Iff.intro | |
| { | |
| intro k | |
| unfold SubstRule2 at k | |
| let eq := k (fun i => a = i) rfl | |
| dsimp at eq | |
| exact eq | |
| } | |
| { | |
| intro i | |
| cases i | |
| intro k | |
| apply id | |
| } | |
| def invertible {A:Sort _}{B:Sort _}(f:A->B) := { h:B->A // ∀ i, h (f i) = i } | |
| def invertible_to_wmap {f:A->B} : (invertible f) -> (wmap A B) := by | |
| intro (.mk h eq1) | |
| exact mkwmap f h eq1 | |
| def wmap_to_invertible : (w:wmap A B) -> (invertible w.1.1) := by | |
| intro (.mk (.mk f h) eq1) | |
| exact .mk h eq1 | |
| def invertible_is_wmap {f:A->B}: wmap (invertible f) ({ w:wmap A B // w.1.1 = f }) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro i | |
| refine .mk (invertible_to_wmap i) ?_ | |
| let (.mk _ _) := i | |
| unfold invertible_to_wmap mkwmap | |
| simp | |
| } | |
| { | |
| intro (.mk w p) | |
| subst p | |
| exact wmap_to_invertible w | |
| } | |
| intro _ | |
| rfl | |
| def wmap_left_injective (w:wmap A B) : Function.Injective w.1.1 := by | |
| let (.mk (.mk f h) eq) := w | |
| exact Function.LeftInverse.injective eq | |
| def invertible_to_injective (w:invertible f): f a = f b -> a = b := by | |
| intro h | |
| let x := invertible_to_wmap w | |
| let k := wmap_left_injective x | |
| exact k h | |
| @[reducible] | |
| def wmap_quot_eq_rel (w:wmap A B)(b1 b2: B) := w.1.2 b1 = w.1.2 b2 | |
| def wmap_to_quot (w:wmap A B) : wmap A (@Quot B (wmap_quot_eq_rel w)) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro i | |
| exact Quot.mk _ (w.1.1 i) | |
| } | |
| { | |
| intro i | |
| refine Quot.lift w.1.2 (fun _ _ => id) i | |
| } | |
| { | |
| intro _ | |
| simp | |
| rw [w.property] | |
| } | |
| set_option pp.proofs true in | |
| def wmap_to_quot_inv (w:wmap A B) : wmap (@Quot B (wmap_quot_eq_rel w)) A := by | |
| refine .mk (.mk ?_ ?_) ?_ | |
| { | |
| intro i | |
| refine Quot.lift w.1.2 (fun _ _ => id) i | |
| } | |
| { | |
| intro a | |
| exact Quot.mk _ (w.1.1 a) | |
| } | |
| { | |
| dsimp | |
| intro i | |
| let ⟨ _ , p ⟩ := Quot.exists_rep i | |
| rewrite [<-p] | |
| apply Quot.sound | |
| unfold wmap_quot_eq_rel | |
| rewrite [w.property] | |
| rfl | |
| } | |
| @[simp] | |
| def quot_transp_eqn_2 : (wtransp (wmap_to_quot_inv m1) (wtransp (wmap_to_quot m1) k).1).1 = k := by | |
| let (.mk j1 p) := wtransp id_wmap (wtransp (wmap_to_quot m1) k) | |
| rw [<-p] | |
| simp [id_wmap] | |
| let (.mk v1 p) := j1 | |
| simp | |
| rw [<-p] | |
| rfl | |
| def wmap_eqvc_can_el_eqn (w:wmap A B): | |
| (@Quot.mk B (wmap_quot_eq_rel w) (w.1.1 (w.1.2 i))) | |
| = | |
| (@Quot.mk B (wmap_quot_eq_rel w) (i)) | |
| := by | |
| refine Quot.sound ?_ | |
| unfold wmap_quot_eq_rel | |
| rw [w.property _] | |
| def hmor_shl {A:Sort _}{B:Sort _}(op:A->A->A)(opm:B->B->B)(w:wmap A B): | |
| ∀ a b, ((opm a b) = w.1.1 (op (w.1.2 a) (w.1.2 b))) -> | |
| (w.1.2 (opm a b) = op (w.1.2 a) (w.1.2 b)) | |
| := by | |
| intro _ _ | |
| let ⟨ (.mk f h), p ⟩ := w | |
| simp at p; simp | |
| intro i | |
| rw [i, p] | |
| def wmap_comp (w1:wmap A B)(w2: wmap B C): wmap A C := by | |
| let (.mk (.mk f1 f2) p1) := w1 | |
| dsimp at p1 | |
| let (.mk (.mk f3 f4) p2) := w2 | |
| dsimp at p2 | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro a | |
| exact f3 $ f1 a | |
| } | |
| { | |
| intro c | |
| exact f2 $ f4 c | |
| } | |
| { | |
| intro i | |
| rw [p2, p1] | |
| } | |
| def fun2 (w:wmap A (@Quot B r)): B -> A := by | |
| intro i | |
| let x := wmap_to_quot_inv w | |
| let k := wtransp x (Quot.mk _ (Quot.mk _ i)) | |
| reduce at k | |
| exact k.val | |
| def fun3 {h:B->A}(k:invertible h)(w:wmap A (@Quot B (fun a b => h a = h b))): A -> B := by | |
| intro i | |
| let (.mk v p2) := wtransp w i | |
| refine Quot.recOn v ?_ ?_ | |
| apply id | |
| intro a b p | |
| simp only [id_eq, eq_rec_constant] | |
| let x := invertible_to_injective k p | |
| exact x | |
| -- example : wmap (wmap A B) (A = B) | |
| def SEq A B := (w:wmap A B) ×' SubstRule1 w.1.2 | |
| def half_uv : wmap (wmap A B) (SEq A B) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro w | |
| refine .mk ?_ ?_ | |
| exact w | |
| intro k | |
| exact wsubst w k | |
| } | |
| { | |
| intro s | |
| unfold SEq at s | |
| let (.mk r m) := s | |
| exact r | |
| } | |
| { | |
| intro i | |
| simp | |
| } | |
| def nat2list : Nat -> List Unit | |
| | .zero => .nil | |
| | .succ a => .cons () (nat2list a) | |
| def list2nat : List Unit -> Nat | |
| | .nil => .zero | |
| | .cons .unit t => .succ (list2nat t) | |
| def ln_coh : (a : List Unit) -> nat2list (list2nat a) = a := by | |
| intro i | |
| match i with | |
| | .cons () a => unfold list2nat nat2list; simp; exact (ln_coh a) | |
| | .nil => unfold list2nat nat2list; simp; | |
| def list_nat : wmap (List Unit) Nat := mkwmap list2nat nat2list ln_coh | |
| def hmor_append_plus : hmor2 (List.append) (Nat.add) (nat2list) := by | |
| intro a1 a2 | |
| dsimp only [List.append_eq, Nat.add_eq] | |
| cases a1 | |
| { | |
| cases a2 <;> unfold nat2list <;> simp | |
| } | |
| { | |
| cases a2 | |
| { | |
| case _ a => | |
| unfold nat2list | |
| simp | |
| } | |
| { | |
| case _ a b => | |
| dsimp only [Nat.succ_eq_add_one] | |
| rw [Nat.add_add_add_comm] | |
| unfold nat2list | |
| simp only [List.cons_append, List.cons.injEq, true_and] | |
| induction a | |
| { | |
| simp [nat2list] | |
| } | |
| { | |
| case _ n ih => | |
| simp [nat2list] | |
| rw [ih] | |
| rw [Nat.add_right_comm _ 1 b] | |
| } | |
| } | |
| } | |
| example : hmor2 (List.append) Nat.add nat2list := by | |
| intro a b | |
| symm | |
| fun_induction nat2list (a) | |
| { | |
| simp only [Nat.zero_eq, Nat.add_eq, zero_add, List.append_eq, List.nil_append] | |
| } | |
| { | |
| case _ a ih => | |
| simp_all only [Nat.add_eq, List.append_eq, Nat.succ_eq_add_one, List.cons_append] | |
| rw [<-ih] | |
| rw [Nat.add_right_comm, Nat.add_one] | |
| conv => | |
| arg 1 | |
| unfold nat2list | |
| } | |
| -- example : hmor2 (List.append) Nat.add nat2list := by | |
| -- intro a b | |
| -- symm | |
| -- fun_induction nat2list (a) | |
| -- repeat aesop | |
| -- rw [<-ih1] | |
| -- rw [Nat.add_right_comm, Nat.add_one] | |
| -- conv => | |
| -- arg 1 | |
| -- unfold nat2list | |
| example : (p:List Unit) ++ q = q ++ p := by | |
| let x := wtransp half_uv list_nat | |
| unfold list_nat half_uv at x | |
| simp at x | |
| let (.mk (.mk _ x2) p) := x | |
| simp at p | |
| subst p | |
| unfold SubstRule1 at x2 | |
| let (.mk a r1) := x2 p | |
| dsimp at r1 | |
| apply r1 | |
| let (.mk b r2) := x2 q | |
| dsimp at r2 | |
| apply r2 | |
| let h := hmor_append_plus | |
| unfold hmor2 at h | |
| dsimp at h | |
| repeat rewrite [h] | |
| apply congrArg | |
| apply Nat.add_comm | |
| def is_contr (T:Sort _) := (cc:T) ×' ∀ i, i = cc | |
| def is_equiv (f:A->B) := ∀ i, is_contr (fiber f i) | |
| def weq (A B) := (f:A->B) ×' is_equiv f | |
| def weq_to_inv (w:weq A B): B -> A := by | |
| intro b | |
| exact (w.snd b).fst.val | |
| @[simp] | |
| def weq_to_inv_eqn_1 (w:weq A B) : weq_to_inv w = fun i => (w.snd i).fst.val := rfl | |
| def weq_cancel_eqn_1 (w:weq A B) : w.fst (weq_to_inv w i) = i := by | |
| let (.mk f cf) := w | |
| simp only [weq_to_inv_eqn_1] | |
| let (.mk k p) := wtransp id_wmap (cf i) | |
| simp [id_wmap] at p | |
| rw [<-p] | |
| let (.mk (.mk v eq1) _) := k | |
| simp only | |
| exact eq1 | |
| def weq_subst (w:weq A B): SubstRule1 w.fst := by | |
| intro b | |
| refine .mk ?_ ?_ | |
| { | |
| exact (weq_to_inv w) b | |
| } | |
| { | |
| intro P | |
| rw [weq_cancel_eqn_1] | |
| apply id | |
| } | |
| def id_weq : weq T T := by | |
| refine .mk id ?_ | |
| intro i | |
| refine .mk ?_ ?_ | |
| refine .mk i ?_ | |
| rfl | |
| intro k | |
| let (.mk _ p) := k | |
| subst p | |
| rfl | |
| def id_subst_rule : SubstRule1 (@id T) := by | |
| intro i | |
| refine .mk i ?_ | |
| intro P | |
| apply id | |
| def iso A B := @Subtype ((A->B) ×' (B->A)) fun (.mk f h) => (∀ i, f (h i) = i) ∧ (∀ i, h (f i) = i) | |
| def mkiso (f:A->B)(h:B->A)(c1:∀ i, f (h i) = i)(c2:∀ i, h (f i) = i): iso A B := .mk (.mk f h) (.intro c1 c2) | |
| @[simp] | |
| def mkiso_eqn_1 : mkiso f h p1 p2 = .mk (.mk f h) (.intro p1 p2) := rfl | |
| def subtype_ext_rev {p:A->Prop}{a b:Subtype p} : (a = b) -> (a.val = b.val) := by | |
| exact fun a_1 => congrArg Subtype.val a_1 | |
| def weq_is_iso : wmap (weq A B) (iso A B) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro w | |
| refine .mk (.mk ?_ ?_) (.intro ?_ ?_) | |
| exact w.fst | |
| { | |
| intro b | |
| let (.mk (.mk a _) _) := w.snd b | |
| exact a | |
| } | |
| intro b | |
| let (.mk j1 k) := wtransp id_wmap (w.snd b) | |
| simp [id_wmap] at k | |
| rw [<-k] | |
| let (.mk (.mk _ p) _) := j1 | |
| simp | |
| exact p | |
| { | |
| intro a | |
| let (.mk j1 k) := wtransp id_wmap (w.snd (w.fst a)) | |
| simp [id_wmap] at k | |
| rw [<-k] | |
| let (.mk (.mk v p) z) := j1 | |
| simp | |
| let fa : fiber w.fst (w.fst a) := by | |
| refine .mk a ?_ | |
| rfl | |
| let x := z fa | |
| unfold fa at x | |
| let k := subtype_ext_rev x | |
| simp at k | |
| symm | |
| exact k | |
| } | |
| } | |
| { | |
| intro w | |
| refine .mk w.1.1 ?_ | |
| intro b | |
| let cf : fiber w.1.1 b := by | |
| refine .mk (w.1.2 b) ?_ | |
| exact w.property.left _ | |
| refine .mk cf ?_ | |
| intro (.mk v p) | |
| unfold cf | |
| subst p | |
| let x := w.property.right v | |
| simp only [x] | |
| } | |
| { | |
| intro i | |
| exact rfl | |
| } | |
| def weq_transp (w:weq A B): ∀ i, fiber (weq_to_inv w) i := by | |
| intro i | |
| refine .mk (w.fst i) ?_ | |
| unfold weq_to_inv | |
| let (.mk (.mk (.mk f h) (.intro _ r)) p) := wtransp weq_is_iso w | |
| rw [<-p] | |
| unfold weq_is_iso mkwmap | |
| simp | |
| apply r | |
| def weq_inv_is_weq (w:weq A B): is_equiv (weq_to_inv w) := by | |
| intro i | |
| refine .mk ?_ ?_ | |
| { | |
| exact weq_transp w i | |
| } | |
| { | |
| intro p | |
| unfold weq_transp | |
| let (.mk v k) := p | |
| subst k | |
| unfold weq_to_inv | |
| let (.mk f q) := w | |
| simp | |
| unfold is_equiv at q | |
| congr | |
| let (.mk (.mk _ j) _) := q v | |
| simp | |
| rw [j] | |
| } | |
| def weq_inverse (w:weq A B): weq B A := by | |
| refine .mk ?_ ?_ | |
| exact weq_to_inv w | |
| exact weq_inv_is_weq w | |
| def weq_to_wmap (w:weq A B): wmap B A := by | |
| let (.mk f eq) := w | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro b | |
| let (.mk (.mk a _) _) := eq b | |
| exact a | |
| } | |
| exact f | |
| { | |
| intro i | |
| let (.mk (.mk _ p) _) := eq i | |
| simp | |
| rw [p] | |
| } | |
| def quot_map_is_equiv (w:wmap A B) : is_equiv (wmap_to_quot_inv w).1.1 := by | |
| unfold is_equiv | |
| intro i | |
| refine .mk ?_ ?_ | |
| { | |
| refine .mk ?_ ?_ | |
| exact Quot.mk _ (w.1.1 i) | |
| unfold wmap_to_quot_inv | |
| simp | |
| rw [w.property] | |
| } | |
| unfold wmap_to_quot_inv | |
| simp | |
| intro k | |
| let (.mk q p) := k | |
| subst p | |
| simp | |
| congr | |
| let (.intro _ x) := Quot.exists_rep q | |
| subst x | |
| simp | |
| exact Eq.symm (wmap_eqvc_can_el_eqn w) | |
| def wmap_to_weq_on_quot (w:wmap A B): weq (@Quot B (wmap_quot_eq_rel w)) A := by | |
| refine .mk ?_ ?_ | |
| let x := wmap_to_quot_inv w | |
| exact x.1.1 | |
| simp | |
| exact quot_map_is_equiv w | |
| def rule1 | |
| (w:wmap A B) | |
| (h2:invertible w.1.2) | |
| : is_contr (fiber (fun b => w.1.2 b) a) | |
| := by | |
| let p1 := quot_map_is_equiv w | |
| let x1 := p1 a | |
| let (.mk cc p1) := x1 | |
| let (.mk cc2 p2) := cc | |
| rw [<-p2] | |
| unfold fiber at p1 | |
| simp only [Subtype.forall, Subtype.mk.injEq] at p1 | |
| let x := Quot.mk (wmap_quot_eq_rel w) (w.1.1 a) | |
| unfold wmap_quot_eq_rel at x | |
| let k := by | |
| refine p1 x ?_ | |
| exact shift_tr_fun w rfl | |
| rw [<-k] | |
| refine .mk ?_ ?_ | |
| { | |
| refine .mk ?_ ?_ | |
| exact (wtransp w a).val | |
| unfold x | |
| reduce | |
| rfl | |
| } | |
| unfold fiber x | |
| simp only [wtransp_eqn_2, Subtype.forall, Subtype.mk.injEq] | |
| intro b h | |
| let x := invertible_to_injective h2 h | |
| exact x | |
| def wmap_to_weq (w1:wmap A B)(h1:invertible w1.1.2) : weq B A := by | |
| refine .mk ?_ ?_ | |
| { | |
| intro b | |
| let (.mk v _) := wtransp (wmap_to_quot_inv w1) (Quot.mk _ b) | |
| exact v | |
| } | |
| { | |
| intro a | |
| exact rule1 w1 h1 | |
| } | |
| -- #print axioms wmap_to_weq | |
| def wmap_to_weq_2 (w1:wmap A B)(w2:wmap B A)(c1: w1.1.2 = w2.1.1) : weq B A := by | |
| let x := wmap_to_invertible w2 | |
| rw [<-c1] at x | |
| exact wmap_to_weq w1 x | |
| def wmap_invert (w1:wmap A B)(h1:invertible w1.1.2)(c1: w1.1.1 = h1.1) : wmap B A := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { exact w1.1.2 } | |
| { exact h1.1 } | |
| intro i | |
| reduce | |
| let (.mk a b) := h1 | |
| reduce; reduce at c1; reduce at b; | |
| exact b i | |
| def wmap_loop (w1:wmap A B)(w2:wmap B A)(c1: w1.1.2 = w2.1.1) : w1.1.1 = w2.1.2 := by | |
| cases w1 | |
| cases w2 | |
| case _ a b c d => | |
| cases a | |
| cases c | |
| case _ f1 f2 f3 f4 => | |
| simp at b d c1 | |
| dsimp only | |
| subst c1 | |
| funext i | |
| let x := d (f1 i) | |
| rw [<-x] | |
| congr | |
| rw [b] | |
| def wmap_to_iso (w1:wmap A B)(w2:wmap B A)(c1: w1.1.2 = w2.1.1): iso A B := by | |
| refine mkiso ?_ ?_ ?_ ?_ | |
| { exact w2.1.2 } | |
| { exact w1.1.2 } | |
| { | |
| intro i | |
| rw [c1] | |
| exact shift_tr_fun w2 rfl | |
| } | |
| { | |
| intro i | |
| let x := wmap_loop w1 w2 c1 | |
| rw [<-x] | |
| exact shift_tr_fun w1 rfl | |
| } | |
| def iso_is_weq : wmap (iso A B) (weq A B) := by | |
| refine wmap_invert ?_ ?_ ?_ | |
| { exact weq_is_iso } | |
| { | |
| refine .mk ?_ ?_ | |
| intro i | |
| refine mkiso ?_ ?_ ?_ ?_ | |
| exact i.1 | |
| { exact (weq_inverse i).1 } | |
| { | |
| intro v | |
| apply weq_cancel_eqn_1 | |
| } | |
| { | |
| intro v | |
| let (.mk f cf) := i | |
| unfold weq_inverse | |
| reduce | |
| let (.mk fib cp) := cf (f v) | |
| dsimp | |
| let x := cp (.mk v (by rfl)) | |
| rw [<-x] | |
| } | |
| { | |
| intro i | |
| reduce | |
| let (.mk (.mk _ _) _) := i | |
| dsimp | |
| } | |
| } | |
| { | |
| rfl | |
| } | |
| def wmap_two_out_of_three | |
| {A B C : Sort _} | |
| (w_gf : wmap A C) | |
| (w_g : wmap B C) | |
| (f : A -> B) | |
| (h_comp : w_gf.1.1 = fun i => w_g.1.1 (f i)) | |
| : wmap A B | |
| := by | |
| let h_f := fun i => w_gf.1.2 (w_g.1.1 i) | |
| refine mkwmap f h_f ?_ | |
| intro a | |
| unfold h_f | |
| rw [funext_iff] at h_comp | |
| rw [<-h_comp] | |
| exact w_gf.property a | |
| structure Functorial (F:Sort _ -> Sort _) where | |
| map : (A -> B) -> (F A -> F B) | |
| map_id : ∀ (x : F A), map (id : A -> A) x = x | |
| map_comp : ∀ (f : A -> B) (g : B -> C) (x : F A), | |
| map (fun i => g (f i)) x = (map g) (map f x) | |
| def wmap_fun_map (fu : Functorial F)(w : wmap A B) : wmap (F A) (F B) := by | |
| let p := w.1 | |
| let f := p.1 | |
| let h := p.2 | |
| refine mkwmap (fu.map f) (fu.map h) ?_ | |
| intro x | |
| rw [<- fu.map_comp] | |
| let k : (fun i => h (f i)) = id := funext w.2 | |
| rw [k] | |
| exact fu.map_id x | |
| #print axioms wmap_fun_map | |
| def wsubst2 (w:wmap A B)(fu:Functorial F): F A -> F B := (wmap_fun_map fu w).1.1 | |
| def option_fu : Functorial Option := by | |
| refine { | |
| map := ?_ | |
| map_id := ?_ | |
| map_comp := ?_ | |
| } | |
| exact Option.map | |
| intro _ x | |
| exact Option.map_id_apply | |
| intro _ _ _ f g p | |
| cases p | |
| simp only [Option.map_none] | |
| case _ val => | |
| simp only [Option.map_some] | |
| @[reducible] | |
| def Example1 := | |
| let x := wmap_fun_map option_fu list_nat | |
| let k := wtransp x (.some []) | |
| k.val = .some 0 | |
| example : Example1 := by rfl | |
| def iterf (n:Nat)(k:T->T): T -> T := | |
| match n with | |
| | .zero => id | |
| | .succ a => fun i => k ((iterf a k) i) | |
| def orbit (a:T)(k:T->T) := { i // iterf i k a = a } | |
| def contr_to_contr_fun_sp: is_contr T -> is_contr (T -> T) := by | |
| intro (.mk cc p) | |
| refine .mk id ?_ | |
| intro f | |
| funext i | |
| let (.mk k p2) := wtransp id_wmap (f i) | |
| simp [id_wmap] at p2 | |
| rw [<-p2] | |
| rewrite [p i, p k, id_def] | |
| rfl | |
| def contr_sp_fun_irrel (c:is_contr T)(f h:T->T): f = h := by | |
| let (.mk cc cp) := contr_to_contr_fun_sp c | |
| rw [cp f, <-cp h] | |
| set_option pp.proofs true in | |
| def contr_ty_to_contr_wmap : is_contr T -> is_contr (wmap T T) := by | |
| intro cpo | |
| let (.mk cc cp) := cpo | |
| refine .mk ?_ ?_ | |
| exact id_wmap | |
| intro w | |
| let (.mk (.mk f h) p1) := w | |
| dsimp at p1 | |
| let eq1 := contr_sp_fun_irrel cpo (f:=f) (h:=id) | |
| let eq2 := contr_sp_fun_irrel cpo (f:=h) (h:=id) | |
| simp only [eq1] | |
| simp only [eq2] | |
| rfl | |
| set_option pp.proofs true in | |
| def uvp (A:Prop)(B:Prop) : wmap (wmap A B) (A = B) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro w | |
| refine Eq.propIntro ?_ ?_ | |
| { | |
| intro i | |
| let b := wtransp w i | |
| exact b.val | |
| } | |
| { | |
| let x := wmap_to_quot w | |
| exact fun2 x | |
| } | |
| } | |
| { | |
| intro k | |
| cases k | |
| exact id_wmap | |
| } | |
| { | |
| intro i | |
| let (.mk (.mk _ _) _) := i | |
| symm | |
| congr | |
| } | |
| #print axioms uvp | |
| def hmor_hf_to_fh (w1:wmap A B)(w2:wmap B A)(c1:w1.1.2 = w2.1.1)(h1:hmor1 h f w1.1.1): hmor1 f h w1.1.2 := by | |
| intro x | |
| let (.mk (.mk a b) p1) := w1 | |
| let (.mk (.mk c d) p2) := w2 | |
| unfold hmor1 at h1 | |
| simp at p1 h1 p2 c1 | |
| simp | |
| subst c1 | |
| grind | |
| inductive EqT {T:Sort k} (a:T): T -> Type u where | |
| | refl : EqT a a | |
| def eqt_to_eq (eq:EqT a b): a = b := by | |
| cases eq | |
| rfl | |
| def trivial_subst_on_id {T:Sort _} : is_contr (SubstRule1 (@id T)) := by | |
| refine .mk ?_ ?_ | |
| { | |
| intro i | |
| refine .mk i ?_ | |
| intro P | |
| apply id | |
| } | |
| { | |
| intro k | |
| funext i | |
| let (.mk j k) := wtransp id_wmap (k i) | |
| simp [id_wmap] at k | |
| rw [<-k] | |
| let (.mk v p) := j | |
| simp only [id_eq] at p | |
| let x := (p (Eq v) (rfl)) | |
| congr | |
| } | |
| structure WRules (A:Sort _)(B:Sort _) where | |
| eqv_fun: A -> B | |
| subst : SubstRule1 eqv_fun | |
| -- hmors1 : ∀ f:B->B, (h:A->A) ×' hmor1 f h eqv_fun | |
| hmors2 : ∀ f:B->B->B, (h:A->A->A) ×' hmor2 f h eqv_fun | |
| def no_conf_hmor (w:WRules A B)(h)(f): (h = (w.hmors2 f).1) ∨ Not (h = (w.hmors2 f).1) := by | |
| exact eq_or_ne h (w.hmors2 f).fst | |
| def wmap_to_wrules (w:wmap A B): WRules B A := by | |
| refine { eqv_fun := ?_, subst := ?_, hmors2 := ?_ } | |
| exact w.1.2 | |
| exact wsubst w | |
| { | |
| intro f | |
| refine .mk ?_ ?_ | |
| let (.mk h p) := hmor2_exists w f | |
| exact h | |
| let (.mk j k) := wtransp id_wmap (hmor2_exists w f) | |
| simp [id_wmap] at k | |
| rw [<-k] | |
| let (.mk _ p) := j | |
| simp | |
| exact p.1 | |
| } | |
| -- example : hmor2 (List.append) Nat.add nat2list := by | |
| -- unfold hmor2 | |
| -- simp | |
| -- intro a b | |
| -- let k := hmor_shl List.append Nat.add list_nat a b | |
| -- unfold list_nat at k | |
| -- simp at k | |
| -- symm | |
| -- apply k | |
| -- let x := wmap_to_wrules list_nat | |
| -- let k2 := no_conf_hmor x (Nat.add) (List.append) | |
| -- unfold x wmap_to_wrules list_nat hmor2_exists at k2 | |
| -- simp at k2 | |
| -- cases k2 | |
| -- { | |
| -- case _ p => | |
| -- rw [funext_iff] at p | |
| -- let p := p a | |
| -- rw [funext_iff] at p | |
| -- let p := p b | |
| -- simp at p | |
| -- apply p | |
| -- } | |
| -- { | |
| -- case _ n => | |
| -- eta_expand at n | |
| -- simp at n | |
| -- conv at n => | |
| -- arg 1 | |
| -- rw [funext_iff] | |
| -- pattern _ = _ | |
| -- rw [funext_iff] | |
| -- simp only [not_forall] at n | |
| -- admit | |
| -- } | |
| def is_unit (T) := ∀ (a b:T), a = b | |
| def is_equiv_contr (f:A->B) : is_unit (is_equiv f) := by | |
| unfold is_equiv | |
| intro a b | |
| funext i | |
| generalize a i = k1 | |
| generalize b i = k2 | |
| let (.mk fi1 p1) := k1 | |
| let (.mk fi2 p2) := k2 | |
| congr | |
| rw [<-p1 fi2] | |
| inductive PreEq : A -> B -> Sort _ where | |
| | iden : PreEq i i | |
| | path (w: weq A B) : PreEq A B | |
| -- | glue1 : @PreEq2.path A A (@id_weq A) = @PreEq2.iden _ A | |
| def pre_eq_eq_rel {a:A}{b:B}(x y: PreEq a b): Prop := | |
| match x, y with | |
| | .iden, .iden => True | |
| | .path f, .path h => ∀ i, f.1 i = h.1 i | |
| | .path i, .iden => i = id_weq | |
| | .iden, .path i => i = id_weq | |
| def Eq2 (a:A)(b:B) : Sort _ := @Quot (PreEq a b) pre_eq_eq_rel | |
| def Eq2.iden {A : Sort _}{a:A} : Eq2 a a := Quot.mk _ PreEq.iden | |
| def Eq2.path {A : Sort _}{B : Sort _} (w : weq A B) : Eq2 A B := Quot.mk _ (PreEq.path w) | |
| def eq2_glue_1 : Eq2.path (@id_weq A) = Eq2.iden := by | |
| refine Quot.sound ?_ | |
| unfold pre_eq_eq_rel | |
| rfl | |
| def weq_to_eq2 (w:weq A B): Eq2 A B := by | |
| exact Eq2.path w | |
| def eq2_to_weq (eq:Eq2 A B) : weq A B := by | |
| refine Quot.recOn eq ?_ ?_ | |
| { | |
| intro eq | |
| cases eq | |
| { | |
| exact id_weq | |
| } | |
| { | |
| case _ w => | |
| exact w | |
| } | |
| } | |
| { | |
| intro a b rel | |
| cases a | |
| { | |
| cases b | |
| { | |
| simp | |
| } | |
| { | |
| case _ w => | |
| unfold pre_eq_eq_rel at rel | |
| simp at rel | |
| subst rel | |
| simp | |
| } | |
| } | |
| { | |
| cases b | |
| { | |
| case _ w => | |
| unfold pre_eq_eq_rel at rel | |
| simp at rel | |
| subst rel | |
| simp | |
| } | |
| { | |
| case _ w1 w2 => | |
| unfold pre_eq_eq_rel at rel | |
| simp at rel | |
| unfold weq at w1 w2 | |
| let x : w1 = w2 := by | |
| let (.mk f p1) := w1 | |
| let (.mk h p2) := w2 | |
| simp at rel | |
| rw [<-funext_iff] at rel | |
| subst rel | |
| simp only [PSigma.mk.injEq, heq_eq_eq, true_and] | |
| let x := is_equiv_contr f p1 p2 | |
| exact x | |
| simp only [eq_rec_constant] | |
| exact x | |
| } | |
| } | |
| } | |
| def eq2_is_weq : iso (Eq2 A B) (weq A B) := by | |
| refine mkiso eq2_to_weq weq_to_eq2 ?_ ?_ | |
| { | |
| intro i | |
| cases i | |
| case _ f eqp => | |
| unfold weq_to_eq2 eq2_to_weq | |
| rfl | |
| } | |
| { | |
| intro i | |
| refine Quot.recOn i ?_ ?_ | |
| { | |
| intro k | |
| cases k | |
| { | |
| unfold weq_to_eq2 eq2_to_weq Eq2.path | |
| apply Quot.sound | |
| unfold pre_eq_eq_rel | |
| simp | |
| } | |
| { | |
| case _ w => | |
| unfold weq_to_eq2 eq2_to_weq Eq2.path | |
| apply Quot.sound | |
| unfold pre_eq_eq_rel | |
| simp | |
| } | |
| } | |
| { | |
| intro a b rel | |
| repeat rfl | |
| } | |
| } | |
| -- https://github.com/ekiciburak/ua_funext/blob/master/UA_FE.v | |
| def arrow_fu (T:Sort _): Functorial (fun K => T -> K) := by | |
| refine { map := ?_, map_id := ?_, map_comp := ?_ } | |
| { | |
| intro A B f h t | |
| exact f (h t) | |
| } | |
| { | |
| intro A B | |
| rfl | |
| } | |
| { | |
| intro A B C f g x | |
| rfl | |
| } | |
| def s442_2 (w:wmap A B): wmap (X -> A) (X -> B) := by | |
| let x := wmap_fun_map (arrow_fu X) w | |
| exact x | |
| def s442 (w:wmap A B): wmap (X -> A) (X -> B) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro k x | |
| let v := k x | |
| let x := wtransp w v | |
| exact x.val | |
| } | |
| { | |
| intro k x | |
| let v := k x | |
| let k2 := fun2 (wmap_to_quot w) | |
| exact k2 v | |
| } | |
| intro f | |
| reduce | |
| apply funext | |
| intro i | |
| let x := w.2 | |
| reduce at x | |
| rw [x (f i)] | |
| -- #print axioms s442 | |
| def s443 (P:A->Sort _)(p:∀ x:A, is_contr (P x)) : wmap (A -> (x:A) ×' P x) (A -> A) := by | |
| apply s442_2 | |
| refine mkwmap ?_ ?_ ?_ | |
| exact fun i => i.1 | |
| { | |
| intro a | |
| refine .mk a ?_ | |
| let x := p a | |
| exact x.1 | |
| } | |
| intro x | |
| cases x | |
| simp only [PSigma.mk.injEq, heq_eq_eq, true_and] | |
| case _ v p2 => | |
| let (.mk j k) := wtransp id_wmap (p v) | |
| simp [id_wmap] at k | |
| rw [<-k] | |
| let (.mk cc cp) := j | |
| simp only [cp] | |
| def h437_2 {A B : Sort _} (re : wmap B A) (c : is_contr A) : is_contr B := by | |
| let (.mk (.mk r s) eps) := re | |
| let (.mk a p) := c | |
| refine .mk ?_ ?_ | |
| exact s (a) | |
| intro y | |
| simp only at eps | |
| rw [<-eps y] | |
| congr | |
| exact p (r y) | |
| def wfunext {A : Sort _} {P : A → Sort _} : (∀ x:A, is_contr (P x)) → is_contr (∀ x:A, P x) := by | |
| intro k | |
| let x := s443 P k | |
| let map := x.1.1 | |
| let h1 : invertible x.1.2 := .mk map (by intro; rfl) | |
| let x2 := wmap_to_iso x ((wtransp invertible_is_wmap h1).1.1) rfl | |
| let x3 := (wtransp iso_is_weq x2).1 | |
| let cf := x3.2 id | |
| refine h437_2 ?_ cf | |
| refine mkwmap ?_ ?_ ?_ | |
| { | |
| intro f | |
| refine .mk (fun x => .mk x (f x)) ?_ | |
| reduce | |
| rfl | |
| } | |
| { | |
| intro (.mk sec q) v | |
| let x1 := (sec v).snd | |
| let x2 := congr_arg P (congr_fun q v) | |
| simp only [id_eq] at x2 | |
| rw [<-x2] | |
| reduce | |
| exact x1 | |
| } | |
| { | |
| intro f | |
| simp only [eq_mpr_eq_cast] | |
| rfl | |
| } | |
| #print axioms wfunext | |
| -- def fext | |
| -- {A : Sort _} | |
| -- {B : A → Sort _} | |
| -- {f g : (x : A) → B x} | |
| -- (h : ∀ x, f x = g x) | |
| -- : f = g := by | |
| -- -- 1. Define the "singleton" fiber P. | |
| -- -- P x is the type of pairs (y, path) where path : f x = y. | |
| -- let P (x : A) := (y : B x) ×' (f x = y) | |
| -- -- 2. Prove that P x is contractible for every x. | |
| -- -- This is the "based path induction" or "singleton contractibility" principle. | |
| -- let h_contr (x : A) : is_contr (P x) := by | |
| -- -- The center of contraction is (f x, rfl) | |
| -- refine .mk (.mk (f x) rfl) ?_ | |
| -- intro w | |
| -- let (.mk y p) := w | |
| -- -- Path induction (subst) proves any (y, p) equals (f x, rfl) | |
| -- subst p | |
| -- rfl | |
| -- -- 3. Apply your 'wfunext' to lift this pointwise contractibility | |
| -- -- to the function space. | |
| -- let global_contr := wfunext h_contr | |
| -- -- 4. Extract the center and the property that everything equals the center. | |
| -- let (.mk _ all_eq) := global_contr | |
| -- -- 5. Construct two dependent functions in this space: | |
| -- -- seq_f: The "diagonal" map corresponding to f (using refl) | |
| -- let seq_f := fun x => PSigma.mk (f x) rfl | |
| -- -- seq_g: The map corresponding to g (using the hypothesis h) | |
| -- let seq_g := fun x => PSigma.mk (g x) (h x) | |
| -- -- 6. Since the space is contractible, both sequences equal the center, | |
| -- -- and therefore equal each other. | |
| -- let e1 := all_eq seq_f | |
| -- let e2 := all_eq seq_g | |
| -- rw [<-e2] at e1 | |
| -- -- e1 is now: seq_f = seq_g | |
| -- -- 7. Project out the first component to show f = g. | |
| -- -- We prove (fun x => f x) = (fun x => g x) by congruence on the first component. | |
| -- let e_fun : (fun x => (seq_f x).1) = (fun x => (seq_g x).1) := by | |
| -- congr | |
| -- exact e1 | |
| -- -- 8. Lean performs eta-reduction automatically (f = \x. f x), concluding the proof. | |
| -- dsimp at e_fun | |
| -- exact e_fun | |
| -- https://inria.hal.science/hal-01966714/document | |
| def PreInt := Nat × Nat | |
| def int_canon_repr (n:PreInt): PreInt := | |
| let (.mk a b) := n | |
| match a, b with | |
| | .succ a, .succ b => int_canon_repr (.mk a b) | |
| | .zero, n => .mk .zero n | |
| | n, .zero => .mk n .zero | |
| termination_by n.fst + n.snd | |
| decreasing_by { | |
| omega | |
| } | |
| def IntNFCst (n:PreInt) := n.1 = 0 ∨ n.2 = 0 | |
| def int_add (a b:PreInt): PreInt := | |
| let (.mk a_1 b_1) := a | |
| let (.mk a_2 b_2) := b | |
| .mk (a_1 + a_2) (b_1 + b_2) | |
| def negated (n:PreInt): PreInt := .mk (n.2) (n.1) | |
| def repr_eqn_1 (k) : int_canon_repr (.mk a b) = int_canon_repr (.mk (a + k) (b + k)) := by | |
| cases k | |
| { | |
| rfl | |
| } | |
| { | |
| case _ k => | |
| rw [Nat.add_succ] | |
| conv => | |
| arg 2 | |
| unfold int_canon_repr | |
| simp only [Nat.add_eq] | |
| apply repr_eqn_1 | |
| } | |
| def canon_repr_eqn_2 (i) : let v := int_canon_repr i; v.1 = 0 ∨ v.2 = 0 := by | |
| let (.mk a b) := i | |
| simp only | |
| cases a | |
| { | |
| unfold int_canon_repr | |
| simp only [Nat.zero_eq, true_or] | |
| } | |
| { | |
| case _ k => | |
| cases b | |
| { | |
| unfold int_canon_repr | |
| simp only [Nat.succ_eq_add_one, Nat.add_eq_zero_iff, one_ne_zero, and_false, Nat.zero_eq, or_true] | |
| } | |
| { | |
| case _ k2 => | |
| unfold int_canon_repr | |
| simp only | |
| apply canon_repr_eqn_2 (k,k2) | |
| } | |
| } | |
| termination_by i.1 + i.2 | |
| def IntNF := { n // IntNFCst n } | |
| def pre_int_to_int_nf (n:PreInt): IntNF := by | |
| refine .mk ?_ ?_ | |
| exact int_canon_repr n | |
| unfold IntNFCst | |
| exact canon_repr_eqn_2 n | |
| def int_nf_to_pre_int (n:IntNF): PreInt := .mk (n.1.1) (n.1.2) | |
| def eqn_87 (k:PreInt) : { j // int_canon_repr k = j } := by | |
| refine .mk ?_ ?_ | |
| exact int_canon_repr k | |
| rfl | |
| def c1 : Function.Injective int_nf_to_pre_int := by | |
| exact (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a => a | |
| def canon_repr_red_eqn_1 : int_canon_repr (.mk 0 b) = (.mk 0 b) := by unfold int_canon_repr; simp | |
| def canon_repr_red_eqn_2 : int_canon_repr (.mk a 0) = (.mk a 0) := by | |
| unfold int_canon_repr | |
| cases a -- ugh, case trees are annoying | |
| simp | |
| simp | |
| def eqn_33 : ∀ (i : IntNF), pre_int_to_int_nf (int_nf_to_pre_int i) = i := by | |
| intro i | |
| let (.mk v p) := i | |
| unfold int_nf_to_pre_int pre_int_to_int_nf | |
| simp only | |
| congr | |
| unfold IntNFCst at p | |
| let (.mk a b) := v | |
| cases p | |
| { | |
| case _ h => | |
| simp only at h; simp only | |
| rw [h] | |
| unfold int_canon_repr | |
| simp only [Nat.zero_eq] | |
| } | |
| { | |
| case _ h => | |
| simp only at h; simp only | |
| rw [h] | |
| exact canon_repr_red_eqn_2 | |
| } | |
| example : wmap IntNF PreInt := by | |
| refine mkwmap ?_ ?_ ?_ | |
| exact int_nf_to_pre_int | |
| exact pre_int_to_int_nf | |
| intro i | |
| exact eqn_33 i | |
| def loops (n:Nat)(A)(B) := | |
| match n with | |
| | .zero => wmap A B | |
| | .succ a => wmap (loops a A B) (loops a A B) | |
| def eq_level_decay : (is_contr (loops n A B)) -> is_contr (loops (n + 1) A B) := by | |
| intro c | |
| let x := contr_ty_to_contr_wmap c | |
| exact x | |
| def not_wmap : wmap Bool Bool := mkwmap not not (by | |
| intro i | |
| simp | |
| ) | |
| -- We define a predicate for "Has a Non-Identity Involution" | |
| structure Involutive (T : Sort _) where | |
| f : wmap T T | |
| is_invol : wmap_comp f f = id_wmap | |
| not_id : f ≠ id_wmap | |
| -- Base case: Level 0 (wmap Bool Bool) | |
| def base_involution : Involutive Bool := by | |
| refine .mk ?_ ?_ ?_ | |
| { | |
| exact not_wmap | |
| } | |
| { | |
| -- Verify involution: not ∘ not = id | |
| apply Subtype.ext; | |
| congr | |
| unfold wmap_comp id_wmap not_wmap | |
| dsimp | |
| simp only [Bool.not_not, Subtype.mk.injEq, PProd.mk.injEq, and_self] | |
| rfl | |
| } | |
| { | |
| -- Verify not distinct from id | |
| intro h | |
| have h_val : not true = id true := by | |
| apply congrFun (congrArg (fun x => x.1.1) h) true | |
| simp only [Bool.not_true, id_eq, Bool.false_eq_true] at h_val | |
| } | |
| -- Inductive Step | |
| -- set_option pp.proofs true in | |
| def step_involution {T : Sort _} (prev : Involutive T) : Involutive (wmap T T) := by | |
| let f_new : wmap (wmap T T) (wmap T T) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| { intro w; exact wmap_comp w prev.f } -- map w -> w ∘ f_prev | |
| { intro w; exact wmap_comp w prev.f } -- Inverse is same because f_prev is involution | |
| { | |
| intro w | |
| -- w ∘ f ∘ f = w ∘ id = w | |
| let (.mk m p1 p2) := prev | |
| dsimp | |
| unfold wmap_comp mkwmap | |
| reduce | |
| congr | |
| { | |
| funext k | |
| let p2 : (fun i => m.1.1 (m.1.1 i)) = id := by | |
| reduce at p1 | |
| let k := subtype_ext_rev p1 | |
| dsimp at k | |
| simp only [PProd.mk.injEq] at k | |
| let (.intro fst _) := k | |
| reduce | |
| exact fst | |
| reduce at p2 | |
| rw [funext_iff] at p2 | |
| rw [p2 _] | |
| } | |
| { | |
| funext k | |
| let p2 : (fun i => m.1.2 (m.1.2 i)) = id := by | |
| reduce at p1 | |
| let k := subtype_ext_rev p1 | |
| dsimp at k | |
| simp only [PProd.mk.injEq] at k | |
| let (.intro _ snd) := k | |
| reduce | |
| exact snd | |
| reduce at p2 | |
| rw [funext_iff] at p2 | |
| rw [p2 _] | |
| } | |
| } | |
| refine .mk f_new ?_ ?_ | |
| { | |
| -- Show f_new ∘ f_new = id | |
| unfold wmap_comp id_wmap f_new | |
| dsimp | |
| reduce | |
| congr | |
| { | |
| funext i | |
| dsimp | |
| congr | |
| { | |
| funext k | |
| let (.mk m p1 p2) := prev | |
| let p2 : (fun i => m.1.1 (m.1.1 i)) = id := by | |
| reduce at p1 | |
| let k := subtype_ext_rev p1 | |
| dsimp at k | |
| simp only [PProd.mk.injEq] at k | |
| let (.intro fst _) := k | |
| reduce | |
| exact fst | |
| reduce at p2 | |
| rw [funext_iff] at p2 | |
| rw [p2 _] | |
| } | |
| { | |
| funext k | |
| let (.mk m p1 p2) := prev | |
| let p2 : (fun i => m.1.2 (m.1.2 i)) = id := by | |
| reduce at p1 | |
| let k := subtype_ext_rev p1 | |
| dsimp at k | |
| simp only [PProd.mk.injEq] at k | |
| let (.intro _ snd) := k | |
| reduce | |
| exact snd | |
| reduce at p2 | |
| rw [funext_iff] at p2 | |
| rw [p2 _] | |
| } | |
| } | |
| { | |
| funext k | |
| let (.mk m p1 p2) := prev | |
| reduce | |
| let p2 : (fun i => m.1.1 (m.1.1 i)) = id := by | |
| reduce at p1 | |
| let k := subtype_ext_rev p1 | |
| dsimp at k | |
| simp only [PProd.mk.injEq] at k | |
| let (.intro fst _) := k | |
| reduce | |
| exact fst | |
| reduce at p2 | |
| rw [funext_iff] at p2 | |
| simp only [p2] | |
| let p2 : (fun i => m.1.2 (m.1.2 i)) = id := by | |
| reduce at p1 | |
| let k := subtype_ext_rev p1 | |
| dsimp at k | |
| simp only [PProd.mk.injEq] at k | |
| let (.intro _ snd) := k | |
| reduce | |
| exact snd | |
| reduce at p2 | |
| rw [funext_iff] at p2 | |
| simp only [p2 _] | |
| rfl | |
| } | |
| } | |
| { | |
| -- Show f_new != id | |
| intro h | |
| -- If f_new = id, then f_new(id) = id | |
| have eval : f_new.1.1 id_wmap = id_wmap.1.1 id_wmap := by rw [h] | |
| dsimp [id_wmap, mkwmap] at eval | |
| -- LHS is id ∘ f_prev = f_prev | |
| -- RHS is id | |
| -- So f_prev = id | |
| -- But we know f_prev != id from hypothesis | |
| apply prev.not_id | |
| exact eval | |
| } | |
| -- Recursively build the involution for level n | |
| def mk_involution (n : Nat) : Involutive (loops n Bool Bool) := | |
| match n with | |
| | 0 => step_involution base_involution | |
| | n + 1 => step_involution (mk_involution n) | |
| -- Final Proof | |
| theorem level_n_not_contr (n : Nat) : is_contr (loops n Bool Bool) -> False := by | |
| intro h_contr | |
| -- 1. Lift contractibility from T to (wmap T T) | |
| let wmap_is_contr := contr_ty_to_contr_wmap h_contr | |
| -- 2. Extract the single element (center) of the contractible wmap space | |
| let (.mk w_center w_all_eq) := wmap_is_contr | |
| -- 3. Retrieve our constructed distinct maps for this level | |
| let inv_struct := mk_involution n | |
| let f := inv_struct.f | |
| let id_map := id_wmap (T := loops n Bool Bool) | |
| -- 4. Both f and id_map must be equal to the center | |
| have h_f_eq_center : f = w_center := w_all_eq f | |
| have h_id_eq_center : id_map = w_center := w_all_eq id_map | |
| -- 5. Therefore f must equal id_map | |
| rw [<-h_id_eq_center] at h_f_eq_center | |
| -- 6. This contradicts the property of our constructed involution | |
| exact inv_struct.not_id h_f_eq_center | |
| -- variable {α : Sort u} {β : α → Sort v} | |
| -- def extEq (f g : (x : α) → β x) : Prop := ∀ x, f x = g x | |
| -- def ExtFun (α : Sort u) (β : α → Sort v) := Quot (@extEq α β) | |
| -- def extApp | |
| -- (f : ExtFun α β) | |
| -- (x : α) : | |
| -- β x := | |
| -- Quot.lift (fun k => k x) (fun _ _ p => p x) f | |
| -- theorem funext' | |
| -- {f g : (x : α) → β x} | |
| -- (h : ∀ x, f x = g x) : | |
| -- f = g := by | |
| -- let k : extApp (Quot.mk _ f) = extApp (Quot.mk _ g) -> f = g := by | |
| -- unfold extApp | |
| -- dsimp | |
| -- apply id | |
| -- apply k | |
| -- let k2 : Quot.mk extEq f = Quot.mk extEq g -> extApp (Quot.mk _ f) = extApp (Quot.mk _ g) := by | |
| -- apply congrArg | |
| -- apply k2 | |
| -- apply Quot.sound | |
| -- exact h | |
| def PointwiseEq {A : Sort u} {B : A -> Sort v} (f g : (x:A) -> B x) := ∀ x, f x = g x | |
| def hap {A : Sort u} {B : A -> Sort v} {f g : (x:A) -> B x} (p : f = g) : PointwiseEq f g := by | |
| subst p | |
| intro x | |
| rfl | |
| def sing_contr {A : Sort _} (a : A) : is_contr ((x : A) ×' a = x) := by | |
| refine .mk (.mk a rfl) ?_ | |
| intro p | |
| let (.mk v eq) := p | |
| subst eq | |
| rfl | |
| -- 2. Use `wfunext` to prove that the "total homotopy space" is contractible. | |
| -- This transforms pointwise contractibility into function space contractibility. | |
| def total_hmtp_contr | |
| {A : Sort _} | |
| {B : A -> Sort _} | |
| (f : (x:A) -> B x) | |
| : is_contr ((g : (x:A) -> B x) ×' PointwiseEq f g) | |
| := by | |
| -- 1. Define the fiber type for each x (Sigma type of value and equality) | |
| let P := fun x => (y : B x) ×' f x = y | |
| -- 2. Establish that fibers are contractible (using your singleton_contr) | |
| let c : ∀ x, is_contr (P x) := fun x => sing_contr (f x) | |
| -- 3. Use wfunext to prove the Pi-type is contractible | |
| let (.mk center_pi contr_pi) := wfunext c | |
| refine .mk ?_ ?_ | |
| { | |
| -- Center of the total space: (f, refl) | |
| refine .mk f ?_ | |
| exact congrFun rfl | |
| } | |
| { | |
| intro (.mk g p) | |
| -- 4. Define the mapping from the Pi-type (∀ x, Σ y, ...) to the Sigma-type (Σ g, ∀ x, ...) | |
| -- This acts as a distributor | |
| let to_sig (k : ∀ x, P x) : ((g : (x:A) -> B x) ×' PointwiseEq f g) := | |
| .mk (fun x => (k x).1) (fun x => (k x).2) | |
| -- 5. Construct the specific element in the Pi-type corresponding to (g, p) | |
| let el_pi : ∀ x, P x := fun x => .mk (g x) (p x) | |
| -- 6. Use the contraction from wfunext to find the path in the Pi-type | |
| -- This gives: (fun x => .mk (f x) rfl) = (fun x => .mk (g x) (p x)) | |
| let path := contr_pi el_pi | |
| let dest := congrArg to_sig path | |
| let el_pi_2 : ∀ x, P x := fun x => .mk (f x) rfl | |
| let path2 := contr_pi el_pi_2 | |
| let dest2 := congrArg to_sig path2 | |
| rw [<-dest2] at dest | |
| reduce at dest | |
| simp only [PSigma.mk.injEq] at dest | |
| congr | |
| eta_expand | |
| apply dest.1 | |
| } | |
| #print axioms total_hmtp_contr | |
| -- def funext_thm | |
| -- {A : Sort _} | |
| -- {B : A -> Sort _} | |
| -- {f g : (x:A) -> B x} | |
| -- (p : PointwiseEq f g) | |
| -- : f = g := by | |
| -- let (.mk _ _) := total_homotopy_contr f | |
| @[reducible] | |
| def k_cyclic (n)(f:A->A) := iterf n f = id | |
| def not_cyclic : k_cyclic 2 not := by | |
| unfold k_cyclic | |
| funext i | |
| repeat unfold iterf | |
| simp only [id_eq, Bool.not_not] | |
| def comp_limit (n): (iterf n not = id) ∨ (iterf n not = not) := by | |
| fun_induction (iterf n not) | |
| left; rfl | |
| case _ ih => | |
| cases ih | |
| { | |
| case _ h => | |
| simp only [h] | |
| right | |
| rfl | |
| } | |
| { | |
| case _ h => | |
| simp only [h] | |
| left | |
| simp only [Bool.not_not] | |
| rfl | |
| } | |
| example : k_cyclic 2 (fun (i:wmap Bool Bool) => wmap_comp i not_wmap) := by | |
| unfold k_cyclic | |
| repeat unfold iterf | |
| funext i | |
| let (.mk (.mk _ _) _) := i | |
| repeat unfold wmap_comp not_wmap | |
| simp only [id_eq, mkwmap_eqn_1, Bool.not_not] | |
| def wmap_Bool_Bool_eq_dec (w : wmap Bool Bool) : | |
| PSum (w.1.1 true = true ∧ w.1.1 false = false) (w.1.1 true = false ∧ w.1.1 false = true) := by | |
| let x := wmap_left_injective w | |
| have ne : w.1.1 true ≠ w.1.1 false := by | |
| intro h; | |
| exact (Bool.eq_not_self true).mp (x (x (congrArg (w.1).fst h))) | |
| by_cases h : w.1.1 true = true | |
| · left | |
| constructor | |
| · exact h | |
| · simp_all | |
| · right | |
| constructor | |
| · exact eq_false_of_ne_true h | |
| · simp_all | |
| def two_autos (w : wmap Bool Bool) : PSum (w = id_wmap) (w = not_wmap) := by | |
| let x := wmap_Bool_Bool_eq_dec w | |
| cases x with | |
| | inl h => | |
| have hf : w.1.1 = id := funext (by simp [h]) | |
| have hg : w.1.2 = id := by | |
| funext b | |
| rw [<-w.2 (w.1.2 b)] | |
| rw [hf] | |
| dsimp | |
| let (.mk (.mk f _) p) := w | |
| dsimp at p h hf | |
| dsimp | |
| cases b | |
| rw [<-h.2, p, <-h.2, p] | |
| rw [hf] | |
| rfl | |
| rw [<-h.1, p, <-h.1, p] | |
| rw [hf] | |
| rfl | |
| let (.mk (.mk f _) p) := w | |
| dsimp at hf hg | |
| subst hf | |
| subst hg | |
| left | |
| reduce | |
| congr | |
| | inr h => | |
| have hf : w.1.1 = not := funext (by simp [h]) | |
| have hg : w.1.2 = not := by | |
| funext b | |
| rw [<-w.2 (w.1.2 b)] | |
| rw [hf] | |
| let (.mk (.mk f _) p) := w | |
| dsimp at p h hf | |
| dsimp | |
| let k (i): Bool.not (f i) = f (Bool.not i) := by | |
| cases i <;> rw [hf] | |
| cases b | |
| { | |
| rw [<-h.1, p, <-h.2] | |
| rw [k] | |
| rw [p, hf] | |
| reduce | |
| rfl | |
| } | |
| { | |
| rw [<-h.2, p, <-h.1] | |
| rw [k, p, hf] | |
| reduce | |
| rfl | |
| } | |
| right | |
| let (.mk (.mk f _) p) := w | |
| dsimp at hf hg | |
| subst hf | |
| subst hg | |
| unfold not_wmap | |
| simp only [mkwmap_eqn_1] | |
| def bool_to_wmap (i:Bool): wmap Bool Bool := | |
| match i with | |
| | .true => id_wmap | |
| | .false => not_wmap | |
| def wmap_to_bool (w : wmap Bool Bool) : Bool := | |
| let x := two_autos w | |
| match x with | |
| | .inl _ => .true | |
| | .inr _ => .false | |
| def bool_bool_aut_cancel (i:Bool): wmap_to_bool (bool_to_wmap i) = i := by | |
| cases i | |
| { | |
| simp [wmap_to_bool, bool_to_wmap]; reduce; rfl | |
| } | |
| { | |
| simp [wmap_to_bool, bool_to_wmap, not_wmap, two_autos]; reduce; rfl | |
| } | |
| def bool_bool_aut_wmap : wmap Bool (wmap Bool Bool) := by | |
| refine mkwmap ?_ ?_ ?_ | |
| exact bool_to_wmap | |
| exact wmap_to_bool | |
| exact bool_bool_aut_cancel | |
| def card_two_equiv : (wmap Bool Bool) ≃ Bool := by | |
| refine { toFun := ?_, invFun := ?_, left_inv := ?_, right_inv := ?_ } | |
| exact wmap_to_bool | |
| exact bool_to_wmap | |
| { | |
| refine Function.leftInverse_iff_comp.mpr ?_ | |
| unfold Function.comp | |
| funext i | |
| simp [wmap_to_bool] | |
| let (.mk v p) := wtransp id_wmap (two_autos i) | |
| simp [id_wmap] at p | |
| rw [<-p] | |
| cases v | |
| { | |
| case _ p2 => | |
| simp [bool_to_wmap] | |
| rw [p2] | |
| } | |
| { | |
| case _ p2 => | |
| simp [bool_to_wmap] | |
| rw [p2] | |
| } | |
| } | |
| { | |
| unfold Function.RightInverse Function.LeftInverse | |
| intro i | |
| exact bool_bool_aut_cancel i | |
| } | |
| def bool_aut_card_is_2 : Cardinal.mk (wmap Bool Bool) = Cardinal.mk (Fin 2) := by | |
| rw [Cardinal.mk_congr card_two_equiv] | |
| simp only [Cardinal.mk_fintype, Fintype.card_bool, Nat.cast_ofNat, Fintype.card_fin] | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment