{-# OPTIONS --without-K --rewriting #-} open import HoTT open import homotopy.HSpace module homotopy.CircleHSpace where ⊙S¹-hSpace : HSpaceStructure ⊙S¹ ⊙S¹-hSpace = hSpaceStructure μ μ-e-l μ-e-r μ-coh where turn-around : (x : S¹) → x == x turn-around = S¹-elim loop (↓-idf=idf-in' (∙=∙' loop loop)) module Mu = S¹Rec (idf S¹) (λ= turn-around) μ : S¹ → S¹ → S¹ μ = Mu.f μ-e-l : (x : S¹) → μ base x == x μ-e-l x = idp μ-e-r : (x : S¹) → μ x base == x μ-e-r = S¹-elim idp (↓-app=idf-in (idp ∙' loop =⟨ ∙'-unit-l loop ⟩ loop =⟨ idp ⟩ turn-around base =⟨ ! (app=-β turn-around base) ⟩ ap (λ z → z base) (λ= turn-around) =⟨ ! (Mu.loop-β |in-ctx (ap (λ z → z base))) ⟩ ap (λ z → z base) (ap μ loop) =⟨ ! (ap-∘ (λ z → z base) μ loop) ⟩ ap (λ z → μ z base) loop =⟨ ! (∙-unit-r _) ⟩ ap (λ z → μ z base) loop ∙ idp ∎)) μ-coh = idp