open import 1Lab.Path.Reasoning
open import 1Lab.Prelude

open import Algebra.Group

open import Data.Sum.Properties
open import Data.List.Base
open import Data.Dec.Base
open import Data.Sum.Base

import Algebra.Group.Free.Words as W
import Algebra.Group.Cayley as C

module Homotopy.Space.Rose where

Roses🔗

The rose with $n$ petals $⋁_{n} S^{1}$ is the space described by the higher inductive type containing a single point base and $n$ distinct path constructors from base to base. For example, the following picture illustrates the rose with 3 petals.

More generally, we can allow the arity $n$ to be given by an arbitrary type $A —$ but for the computation of the fundamental group below, we restrict ourselves to roses with a discrete number of petals.

data Rose {ℓ} (A : Type ℓ) : Type ℓ where
  base : Rose A
  loop : A → base ≡ base

The loop space of a rose🔗

When looking at the picture above, it’s easy to imagine some properties of the fundamental group of the rose with 3 petals: we can go around the space and end up back at the endpoint by taking any of the petals, and once we’re back at the basepoint, we can then walk along a different petal; and walking along different petals generates different paths.

One can imagine that a general loop on base is thus described by the list of petals we have taken, subject to the relation that walking backwards and then forwards along the same petal does not contribute anything to the list. This is a combinatorial description of the free group on a discrete type, and indeed the purpose of this section is to show that $Ω (⋁_{A} S^{1}) = F (A) .$

module _ {ℓ} (A : Type ℓ) ⦃ _ : Discrete A ⦄ where
  open W A
  open C Free-group renaming (Cayley to rot)
  module F = Group-on (Free-group .snd)

The proof follows exactly the same outline as the computation of the fundamental group of the circle: we define a type family Cover over the rose on $A$ petals, sending the base point to the type underlying the group $F (A),$ and the path generated by $x$ to the identification $ua (rot x) : F (A) \equiv F (A)$ generated by Cayley’s theorem. Transport along this type family converts loops in Rose to elements of the free group.

  Cover : Rose A → Type ℓ
  Cover base       = ⌞ Free-group ⌟
  Cover (loop x i) = ua (rot (inl x ∷ [] , one _)) i

  encode : ∀ x → base ≡ x → Cover x
  encode x = J (λ x p → Cover x) F.unit

In the other direction, we define by case analysis a mapping from letters to loops, and extend this to words by recursion; the letter $x$ is sent to the loop $loop x,$ and the letter $x^{- 1}$ is thus sent to $(loop x)^{- 1} .$

  loopˡ : Letter → base ≡ base
  loopˡ (inl x) = loop x
  loopˡ (inr x) = sym (loop x)

  loopʷ : Word → base ≡ base
  loopʷ []       = refl
  loopʷ (x ∷ xs) = loopʷ xs ∙ loopˡ x

To write a decoding function, we have to show that this function sends the action of a letter $x$ on a word $w$ to the composition of the paths generated by $w$ and $x;$ this is a simple case bash.

  loop-act : (x : Letter) (w : Word) → loopʷ (act x w) ≡ loopʷ w ∙ loopˡ x
  loop-act x [] = refl
  loop-act x (y ∷ w) with x ≡? opp y
  ... | no ¬p = refl
  ... | yes p with x | y
  ... | inl a | inl b = absurd (inl≠inr p)
  ... | inr a | inr b = absurd (inr≠inl p)
  ... | inl a | inr b = sym $
    (loopʷ w ∙ sym (loop b)) ∙ loop a ≡⟨ ∙-pullr (ap₂ _∙_ refl (ap loop (inl-inj p)) ∙ ∙-invl _) ⟩≡
    loopʷ w ∙ refl                    ≡⟨ ∙-idr _ ⟩≡
    loopʷ w                           ∎
  ... | inr a | inl b = sym $ ∙-pullr (ap₂ _∙_ (ap loop (inr-inj (sym p))) refl ∙ ∙-invr _) ∙ ∙-idr _

This lemma extends to the coherence case of a decoding function exactly as in the case for the circle, i.e. by filling the dotted square face in the diagram

  decode : ∀ x → Cover x → base ≡ x
  decode base (w , _) = loopʷ w
  decode (loop x i) w j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → loopʷ (unglue w .fst) j
    k (i = i0) → ∙→square (loop-act (inl x) (w .fst)) (~ k) j
    k (i = i1) → loopʷ (w .fst) j
    k (j = i0) → base
    k (j = i1) → loop x (i ∨ ~ k)

To show that these functions are inverses at the base point, we do some more case analysis— in one direction, this “case analysis” is path induction, which immediately shows that decoding is inverse to encoding; in the other, we show that transport along Cover takes composition of paths to the corresponding operations on the group $F (A) .$

  encode-decode : ∀ x (p : base ≡ x) → decode x (encode x p) ≡ p
  encode-decode x = J (λ x p → decode x (encode x p) ≡ p) refl

  private
    ε : base ≡ base → ⌞ Free-group ⌟ → ⌞ Free-group ⌟
    ε p = subst Cover p

Really, the proof is just a case bash: we start by showing that ε takes loopˡ at $x$ to the action of the letter $x$ on an arbitrary word; this is by cases both on the letter and the head of the word (if any); but it is nonrecursive.

This is then extended to entire words by recursion.

    encode-loopˡ
      : (w : Word) (r : Reduced w) (x : Letter)
      → ε (loopˡ x) (w , r) .fst ≡ act x w
    encode-loopˡ [] r (inl x) = ap (λ e → inl {B = A} e ∷ []) (transport-refl _)
    encode-loopˡ [] r (inr x) = refl
    encode-loopˡ (y ∷ w) r (inl x) with inl x ≡? opp y
    ... | yes a = transport-refl w
    ... | no ¬a = λ i →
        inl (transp (λ _ → A) i x)
      ∷ transp (λ _ → A ⊎ A) i y
      ∷ transp (λ _ → List (A ⊎ A)) i w

    encode-loopˡ (y ∷ w) r (inr x) with inr x ≡? opp y
    ... | yes a rewrite ≡?-yes' (a ∙ ap opp (sym (transport-refl y)))  =
      transport-refl _
    ... | no ¬a rewrite ≡?-no λ p → ¬a (p ∙ ap opp (transport-refl y)) = λ i →
      inr x ∷ transp (λ i → A ⊎ A) i y ∷ transp (λ i → List (A ⊎ A)) i w

    encode-loopʷ : (w : Word) (r : Reduced w) (w' : ⌞ Free-group ⌟) → ε (loopʷ w) w' .fst ≡ mul w (w' .fst)
    encode-loopʷ [] r w' = transport-refl (w' .fst)
    encode-loopʷ (x ∷ w) r w' =
      ε (loopʷ w ∙ loopˡ x) w'                                .fst ≡⟨ ap fst (subst-∙ Cover (loopʷ w) (loopˡ x) w') ⟩≡
      ε (loopˡ x) ⌜ ε (loopʷ w) w' ⌝                          .fst ≡⟨ ap! (Σ-prop-path! (encode-loopʷ w (uncons-reduced r) w')) ⟩≡
      ε (loopˡ x) (mul w (w' .fst) , mul-reduced w (w' .snd)) .fst ≡⟨ encode-loopˡ (mul w (w' .fst)) (mul-reduced w (w' .snd)) x ⟩≡
      act x (mul w (w' .fst))                                      ∎

As a consequence, the encoding of the word $w$ is precisely the product $w 1,$ which is of course just $w —$ this shows that encoding is inverse to decoding.

  ΩBouquet : (base ≡ base) ≃ ⌞ Free-group ⌟
  ΩBouquet .fst = encode base
  ΩBouquet .snd = is-iso→is-equiv record
    { from = decode base
    ; rinv = λ x → Σ-prop-path! $
        encode base (loopʷ (x .fst)) .fst ≡⟨ encode-loopʷ (x .fst) (x .snd) F.unit ⟩≡
        (x F.⋆ F.unit) .fst               ≡⟨ ap fst (F.idr {_ , x .snd}) ⟩≡
        x .fst                            ∎
    ; linv = encode-decode base
    }