“rec base” injectivity & some simple lemmas

GroundZero/Algebra/EilenbergMacLane.lean

@@ -1,4 +1,7 @@
 import GroundZero.Algebra.Group.Basic
+import GroundZero.HITs.Suspension
+import GroundZero.HITs.Trunc
+
 open GroundZero.Theorems.Functions GroundZero.Theorems.Equiv
 open GroundZero.Types.Equiv (idtoeqv)
 open GroundZero.Types.Id (dotted)
@@ -200,4 +203,13 @@ namespace K1
   end
 end K1
 
-end GroundZero.Algebra
+hott def ItS (A : Type) : ℕ → Type
+|      0     => A
+| Nat.succ n => ∑ (ItS A n)
+
+open GroundZero.HITs (Trunc)
+
+hott def K (G : Group) (n : ℕ) :=
+Trunc (hlevel.ofNat (n + 1)) (ItS (K1 G) n)
+
+end GroundZero.Algebra

GroundZero/HITs/Circle.lean

@@ -332,7 +332,8 @@ namespace Circle
     apply Sigma.mapFstOverProd
   end
 
-  hott def inv : S¹ → S¹ := Circle.rec base loop⁻¹
+  hott def turn : S¹ → S¹ := rec base loop
+  hott def inv  : S¹ → S¹ := rec base loop⁻¹
 
   noncomputable hott def invInv (x : S¹) : inv (inv x) = x :=
   let invₚ := @Id.map S¹ S¹ base base (inv ∘ inv);
@@ -513,9 +514,12 @@ namespace Circle
 
   def uarec {A : Type u} (φ : A ≃ A) : S¹ → Type u := rec A (ua φ)
 
-  hott def Ωrec {A : Type u} (zero : A) (succ pred : A → A)
-    (p : succ ∘ pred ~ id) (q : pred ∘ succ ~ id) : Ω¹(S¹) → A :=
-  λ r, @transport S¹ (uarec ⟨succ, (⟨pred, q⟩, ⟨pred, p⟩)⟩) base base r zero
+  abbrev Ωhelix {A : Type u} {succ pred : A → A} (p : succ ∘ pred ~ id) (q : pred ∘ succ ~ id) : S¹ → Type u :=
+  uarec ⟨succ, ⟨pred, q⟩, ⟨pred, p⟩⟩
+
+  hott def Ωrec {x : S¹} {A : Type u} (zero : A) (succ pred : A → A)
+    (p : succ ∘ pred ~ id) (q : pred ∘ succ ~ id) : base = x → Ωhelix p q x :=
+  λ r, @transport S¹ (Ωhelix p q) base x r zero
 
   section
     variable {A : Type u} (zero : A) (succ pred : A → A)
@@ -588,6 +592,24 @@ namespace Circle
     apply recβrule₂; apply Id.invComp
   end
 
+  hott def mapLoopEqv {B : Type u} : (S¹ → B) ≃ (Σ (x : B), x = x) :=
+  begin
+    fapply Sigma.mk; intro φ; exact ⟨φ base, ap φ loop⟩; apply Qinv.toBiinv;
+    fapply Sigma.mk; intro w; exact rec w.1 w.2; apply Prod.mk;
+    { intro w; fapply Sigma.prod; exact idp w.1; transitivity;
+      apply Equiv.transportInvCompComp; transitivity;
+      apply Id.reflRight; apply recβrule₂ };
+    { intro φ; symmetry; apply Theorems.funext; apply mapExt }
+  end
+
+  hott def recBaseInj (p q : Ω¹(S¹)) (ε : rec base p = rec base q) : p = q :=
+  begin
+    have θ := ap (subst ε) (recβrule₂ base p)⁻¹ ⬝ apd (λ f, ap f loop) ε ⬝ recβrule₂ base q;
+    apply transport (p = ·) θ _⁻¹; transitivity; apply Equiv.transportOverHmtpy;
+    -- somewhat surprisingly commutativity of Ω¹(S¹) arises out of nowhere
+    transitivity; apply ap (· ⬝ _ ⬝ _); apply Id.mapInv; apply Id.idConjIfComm; apply comm
+  end
+
   section
     variable {B : Type u} (b : B) (p q : b = b) (H : p ⬝ q = q ⬝ p)
 
@@ -675,8 +697,7 @@ namespace Circle
   section
     variable {A : Type u} {a : A} (B : Π x, a = x → Type v) (w : B a (idp a)) {b : A} (p : a = b)
 
-    hott def ΩJ :=
-    transportconst (Interval.happly (apd B p) p) (transportMeet B w p)
+    hott def ΩJ := transportconst (Interval.happly (apd B p) p) (transportMeet B w p)
 
     noncomputable hott def ΩJDef : J₁ B w p = ΩJ B w p :=
     begin induction p; reflexivity end

GroundZero/HITs/Suspension.lean

@@ -47,4 +47,4 @@ namespace Suspension
 end Suspension
 
 end HITs
-end GroundZero
+end GroundZero

GroundZero/Types/Equiv.lean

@@ -444,6 +444,14 @@ namespace Equiv
     transportconst (bimap f p q) u = transport (f a₂) q (transport (f · b₁) p u) :=
   begin induction p; induction q; reflexivity end
 
+  hott def transportDiag₁ {A : Type u} (B : A → A → Type v) {a b : A} {p : a = b} (w : B a a) :
+    transport (λ x, B x x) p w = transport (B b) p (transport (B · a) p w) :=
+  begin induction p; reflexivity end
+
+  hott def transportDiag₂ {A : Type u} (B : A → A → Type v) {a b : A} {p : a = b} (w : B a a) :
+    transport (λ x, B x x) p w = transport (B · b) p (transport (B a) p w) :=
+  begin induction p; reflexivity end
+
   hott theorem mapOverAS {A : Type u} {a b : A} (f : A → A → A) (g : A → A) (p : a = b) :
     Id.map (AS f g) p = @bimap A A A a b (g a) (g b) f p (Id.map g p) :=
   begin induction p; reflexivity end
@@ -554,4 +562,4 @@ def fib {A : Type u} {B : Type v} (f : A → B) (y : B) := Σ (x : A), f x = y
 def total {A : Type u} (B : A → Type v) := Σ x, B x
 def fiberwise {A : Type u} (B : A → Type v) := Π x, B x
 
-end GroundZero.Types
+end GroundZero.Types

dependency-map.gv

@@ -141,9 +141,9 @@ digraph dependency_map {
     }
     "HITs/Reals"
     "HITs/Simplicial"
-    "HITs/Suspension" -> { "HITs/Circle", "HITs/Join" }
+    "HITs/Suspension" -> { "Algebra/EilenbergMacLane", "HITs/Circle", "HITs/Join" }
     "HITs/Topologization"
-    "HITs/Trunc" -> { "Algebra/Monoid", "HITs/Quotient" }
+    "HITs/Trunc" -> { "Algebra/EilenbergMacLane", "Algebra/Monoid", "HITs/Quotient" }
     "HITs/Wedge"
   }