Pointed Types and Loop Spaces
Contents
{-# OPTIONS --without-K --safe #-} module pointed where open import mltt open import twocatconstructions open import naturals using (ℕ) renaming (suc to S) open import negation using ( _⟺_ ) open ≡-Reasoning open ◾-lemmas open ap-lemmas
Pointed Types
Let us begin by defining the type of pointed types (note that it belongs to a higher universe). Again, we use a record so we can name the fields. Note also that Agda allows to overload the constructors. We reuse _,_ for pointed types. Indeed, an alternative definition would have been
module PointedTypes where record Ptd (ℓ : Level) : Set (lsuc ℓ) where constructor _,_ field U⊙ : Set ℓ --forget pt : U⊙ open Ptd
By “opening” the record (module, really) we make the two names U⊙ and pt visible without the prefix Ptd; that is we can write U⊙ instead of Ptd.U⊙.
ptd : ∀ {ℓ} (A : Set ℓ) → A → Ptd ℓ ptd {ℓ} A x = A , x
Another familiar operation in Topology is to add a disjoint point to make a space pointed. We do the same here:
⊙F : ∀{ℓ} (A : Set ℓ) → Ptd ℓ U⊙ (⊙F A) = 𝟙 + A pt (⊙F A) = inl * pattern + = inl * -- base point
It is conventional to denote the disjoint base point as \(+\), so we have added a pattern to achieve that.
Morphisms of pointed spaces are the obvious thing: a function respecting the base point. Here, we define it as a pair consisting of a term f : A → B and an identification of base points in f x ≡ y:
infix 10 _⊙→_ _⊙→_ : ∀{ℓ ℓ'} → Ptd ℓ → Ptd ℓ' → Set (ℓ ⊔ ℓ') (A , x) ⊙→ (B , y) = Σ[ f ∈ (A → B) ] (f x ≡ y )
The identity function, explicit and implicit versions:
-- explicit version ⊙id : ∀{ℓ} (X : Ptd ℓ) → X ⊙→ X Σ.fst (⊙id X) = id Σ.snd (⊙id X) = idp (pt X) -- implicit version ⊙id′ : ∀{ℓ} {X : Ptd ℓ} → X ⊙→ X ⊙id′ {X = X} = ⊙id X
Since the types are pointed, we can define the constant morphism collapsing everything to the target’s base point
⊙cst : ∀{ℓ ℓ'} {X : Ptd ℓ} {Y : Ptd ℓ'} → X ⊙→ Y ⊙cst {Y = Y} = (λ x → pt Y) , idp (pt Y)
The type 𝟙 is naturally pointed; we denote it by ⊙𝟙:
⊙𝟙 : Ptd 0ℓ U⊙ ⊙𝟙 = 𝟙 pt ⊙𝟙 = *
It acts as a zero object among pointed types. There is a morphism to any pointed type
⊙𝟙⊙→ : ∀{ℓ} (X : Ptd ℓ) → ⊙𝟙 ⊙→ X Σ.fst (⊙𝟙⊙→ X) = 𝟙-rec (pt X) Σ.snd (⊙𝟙⊙→ X) = idp (pt X)
and of course a morphism from any pointed type:
⊙→⊙𝟙 : ∀{ℓ} (X : Ptd ℓ) → X ⊙→ ⊙𝟙 ⊙→⊙𝟙 X = ⊙cst {X = X}
There is of course the composition of pointed maps:
infix 2 _⊙∘_ _⊙∘_ : ∀{ℓ ℓ' ℓ''} {X : Ptd ℓ} {Y : Ptd ℓ'} {Z : Ptd ℓ''} → Y ⊙→ Z → X ⊙→ Y → X ⊙→ Z Σ.fst ((g , q) ⊙∘ (f , p)) = g ∘′ f Σ.snd ((g , q) ⊙∘ (f , p)) = (ap g p) ◾ q
Loop Spaces
module LoopSpaces {ℓ : Level} where open PointedTypes
First, let us define a generic loop functor. Analogously to the same situation in Topology, we consider the based loop functor, as opposed to the free one, hence we define it in the context of pointed types. Thus, given a pointed type (U⊙ , pt), its loop “space” is defined as the type of identifications of its base point, pointed by the reflexivity identificaction of said base point:
⊙Ω : Ptd ℓ → Ptd ℓ ⊙Ω (U⊙ , pt) = (pt ≡ pt) , (idp pt)
with the underlying carrier type (without the base point):
Ω⊙ : Ptd ℓ → Set ℓ Ω⊙ = Ptd.U⊙ ∘′ ⊙Ω
The loop construction can of course be iterated:
⊙Ω^ : (n : ℕ) → Ptd ℓ → Ptd ℓ ⊙Ω^ 0 X = X ⊙Ω^ (S n) X = ⊙Ω (⊙Ω^ n X)
which is to say that the \(n^\mathrm{th}\) loop space is the loop space of the one at level \(n-1\). This definition can be tweaked to make it look more like the recursive ones we are using in Type Theory:
-- Definition in HoTT book ⊙Ω′^ : (n : ℕ) → Ptd ℓ → Ptd ℓ ⊙Ω′^ 0 X = X ⊙Ω′^ (S n) X = ⊙Ω^ n (⊙Ω X)
Now we introduce a more ordinary version of the loop functor where we explicitly mark the base point: given a type and a term a : A, Ω A a is the loop space based at a : A. Note that this is an ordinary type, not a pointed one.
Ω : (A : Set ℓ) → A → Set ℓ Ω A a = Ω⊙ (ptd A a)
We iterate it one more time. For the double loop space we do not need to specify the base point, as the previous iteration comes naturally pointed.
Ω² : (A : Set ℓ) → A → Set ℓ Ω² A a = Ω (Ω A a) (idp a) --explicitly mark the identity path at the base point
module Eckmann-Hilton {A : Set ℓ} {a : A} where lemma[i] : (α β : Ω² A a) → (α ◾ʳ idp a) ◾ (idp a ◾ˡ β) ≡ α ◾ β lemma[i] α β = (α ◾ʳ idp a) ◾ (idp a ◾ˡ β) ≡⟨ (◾ʳrefl α) ★ (refl◾ˡ β) ⟩ (α ◾ refl) ◾ (β ◾ refl) ≡⟨ ru α ★ ru β ⟩ α ◾ β ∎ lemma[ii] : (α β : Ω² A a) → (idp a ◾ˡ β) ◾ (α ◾ʳ idp a) ≡ β ◾ α lemma[ii] α β = (idp a ◾ˡ β) ◾ (α ◾ʳ idp a) ≡⟨ (refl◾ˡ β) ★ (◾ʳrefl α) ⟩ (β ◾ refl) ◾ (α ◾ refl) ≡⟨ ru β ★ ru α ⟩ β ◾ α ∎ Thm[EH] : (α β : Ω² A a) → α ★ β ≡ β ★ α Thm[EH] α β = α ★ β ≡⟨ ★-is-★′ α β ⟩ α ★′ β ≡⟨ refl ⟩ (idp a ◾ˡ β) ◾ (α ◾ʳ idp a) ≡⟨ lemma[ii] α β ⟩ β ◾ α ≡⟨ (lemma[i] β α) ⁻¹ ⟩ (β ◾ʳ idp a) ◾ (idp a ◾ˡ α) ≡⟨ refl ⟩ β ★ α ∎ Corollary : (α β : Ω² A a) → α ◾ β ≡ β ◾ α Corollary α β = α ◾ β ≡⟨ (lemma[i] α β) ⁻¹ ⟩ α ★ β ≡⟨ Thm[EH] α β ⟩ β ★ α ≡⟨ lemma[i] β α ⟩ β ◾ α ∎