{-# 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