{-# OPTIONS --without-K --rewriting --overlapping-instances #-} module Pi.Coxeter.Group where open import HoTT open import Pi.Coxeter.Coxeter open import Pi.Coxeter.Sn open import Pi.Common.Misc open import Pi.Common.Extra module _ (n : ℕ) where SnGroupStructure : GroupStructure (Sn n) GroupStructure.ident SnGroupStructure = q[ nil ] GroupStructure.inv SnGroupStructure = SetQuot-map reverse (reverse-respects-≈ {n = n}) GroupStructure.comp SnGroupStructure = SetQuot-map2 _++_ (λ l → idp) respects-++ GroupStructure.unit-l SnGroupStructure = SetQuot-elim (λ l → idp) (λ p → prop-has-all-paths-↓) GroupStructure.assoc SnGroupStructure = SetQuot-elim (λ l1 → SetQuot-elim (λ l2 → SetQuot-elim (λ l3 → ap q[_] (++-assoc l1 l2 l3)) (λ r → prop-has-all-paths-↓)) (λ r → prop-has-all-paths-↓)) (λ r → prop-has-all-paths-↓) GroupStructure.inv-l SnGroupStructure = SetQuot-elim (λ l → quot-rel (≈-inv-l l)) (λ r → prop-has-all-paths-↓) SnGroup : Group lzero Group.El SnGroup = Sn n Group.El-level SnGroup = ⟨⟩ Group.group-struct SnGroup = SnGroupStructure