{-# OPTIONS --without-K #-}
open import level
open import algebra.group.core
open import algebra.monoid.mset
open import algebra.monoid.morphism
open import function.extensionality
open import function.isomorphism
open import equality.calculus
open import equality.core
open import sum
open import hott.level
open import hott.equivalence
open import hott.univalence

module algebra.group.gset {i}(G : Set i) ⦃ gG : IsGroup G ⦄ where
  open IsGroup ⦃ ... ⦄

  IsGSet : ∀ {j}(X : Set j) → Set (i ⊔ j)
  IsGSet X = IsMSet G X

  GSet : ∀ j → Set (i ⊔ lsuc j)
  GSet j = Σ (Set j) IsGSet

  GSet₀ : ∀ j → Set (i ⊔ lsuc j)
  GSet₀ j = Σ (Type j ) λ { (X , hX) → G → X → X }

  GSet₁ : ∀ {j} → GSet₀ j → Set (i ⊔ j)
  GSet₁ ((X , _) , _◂_) =
    ((g₁ g₂ : G)(x : X) → (g₁ * g₂) ◂ x ≡ g₁ ◂ (g₂ ◂ x))
    × ((x : X) → e ◂ x ≡ x)

  gset₁-level : ∀ {j}(X : GSet₀ j)
              → h  (GSet₁ X)
  gset₁-level ((X , hX) , act) = ×-level
    (Π-level λ g₁ → Π-level λ g₂ → Π-level λ x → hX _ _)
    (Π-level λ x → hX _ _)

  gset-struct-iso : ∀ {j} → GSet j ≅ Σ (GSet₀ j) GSet₁
  gset-struct-iso = record
    { to = λ { (X , xG) → (((X , IsMSet.mset-level xG) , IsMSet._◂_ xG) ,
                           (IsMSet.◂-hom xG , IsMSet.◂-id xG)) }
    ; from = λ { (((X , hX) , _◂_) , (◂-hom , ◂-id))
             → (X , mk-is-mset _◂_ ◂-hom ◂-id hX) }
    ; iso₁ = λ _ → refl
    ; iso₂ = λ _ → refl }

  open IsMSet ⦃ ... ⦄

  module _ {j k}
           {X : Set j} ⦃ xG : IsGSet X ⦄
           {Y : Set k} ⦃ yG : IsGSet Y ⦄ where
    IsGSetMorphism : (X → Y) → Set (i ⊔ j ⊔ k)
    IsGSetMorphism = IsMSetMorphism G

  module _ {j k}
           (X : Set j) ⦃ xG : IsGSet X ⦄
           (Y : Set k) ⦃ yG : IsGSet Y ⦄ where
    GSetMorphism : Set (i ⊔ j ⊔ k)
    GSetMorphism = Σ (X → Y) IsGSetMorphism

    gsetmorphism-equality : h  Y → {f g : X → Y}
      (f-mor : IsGSetMorphism f) (g-mor : IsGSetMorphism g)
      → f ≡ g
      → _≡_ {A = GSetMorphism}
        (f , f-mor)
        (g , g-mor)
    gsetmorphism-equality hY {f} f-mor g-mor refl =
      ap (λ m → (f , m)) (h1⇒prop (is-mset-morphism-level G hY f) _ _)

  module _ {j} (X : Set j) ⦃ xG : IsGSet X ⦄
               (Y : Set j) ⦃ yG : IsGSet Y ⦄ where
    𝑋 𝑌 : GSet j
    𝑋 = (X , xG)
    𝑌 = (Y , yG)

    X₀ Y₀ : GSet₀ j
    X₀ = ((X , IsMSet.mset-level xG) , _◂_)
    Y₀ = ((Y , IsMSet.mset-level yG) , _◂_)

    GSet-univalence : (𝑋 ≡ 𝑌)
                    ≅ (Σ (GSetMorphism X Y) λ { (f , _) → weak-equiv f })
    GSet-univalence = begin
        (𝑋 ≡ 𝑌)
      ≅⟨ iso≡ gset-struct-iso ·≅ sym≅ (subtype-equality gset₁-level) ⟩
        (X₀ ≡ Y₀)
      ≅⟨ sym≅ Σ-split-iso ⟩
        ( Σ (proj₁ X₀ ≡ proj₁ Y₀) λ p →
            subst (λ { (X , _) → G → X → X }) p (proj₂ X₀) ≡ proj₂ Y₀ )
      ≅⟨ ( Σ-ap-iso (sym≅ (subtype-equality λ X → hn-h1  X)) λ p
         → trans≡-iso (sym (subst-naturality (λ X → G → X → X)
                             proj₁ p (proj₂ X₀)))) ⟩
        ( Σ (X ≡ Y) λ p → subst (λ X → G → X → X) p (proj₂ X₀) ≡ proj₂ Y₀ )
      ≅⟨ Σ-ap-iso refl≅ (λ p → sym≅ (lem₁ p _ _)) ⟩
        ( Σ (X ≡ Y) λ p → ∀ g w → coerce p (proj₂ X₀ g w)
                                ≡ proj₂ Y₀ g (coerce p w) )
      ≅⟨ ( Σ-ap-iso uni-iso λ p → refl≅ ) ⟩
        ( Σ (X ≈ Y) λ f → ∀ g w → apply≈ f (proj₂ X₀ g w)
                                ≡ proj₂ Y₀ g (apply≈ f w))
      ≅⟨  record
            { to = λ { ((f , we), mor) → ((f , mor) , we) }
            ; from = λ { ((f , mor) , we) → ((f , we) , mor) }
            ; iso₁ = λ _ → refl
            ; iso₂ = λ _ → refl } ⟩
        (Σ (GSetMorphism X Y) λ { (f , _) → weak-equiv f })
      ∎
      where
        open ≅-Reasoning

        lem₁ : {U V : Set j}(p : U ≡ V)
             → (act : G → U → U)
             → (act' : G → V → V)
             → (∀ g u → coerce p (act g u) ≡ act' g (coerce p u))
             ≅ (subst (λ { X → G → X → X }) p act ≡ act')
        lem₁ refl act act' = (Π-ap-iso refl≅ λ g → strong-funext-iso)
          ·≅ strong-funext-iso

  instance
    GisGSet : IsGSet G
    GisGSet = record
      { _◂_ = _*_
      ; ◂-hom = assoc
      ; ◂-id = lunit
      ; mset-level = is-set }

  module _ {j} {X : Set j} (hX : h  X) ⦃ xG : IsGSet X ⦄ where
    GSet-repr : (ϕ : G → X) → IsGSetMorphism ϕ
              → (g : G) → ϕ g ≡ g ◂ ϕ e
    GSet-repr ϕ ϕ-mor g = ap ϕ (sym (runit g)) · ϕ-mor g e

    GSet-repr-iso : GSetMorphism G X ≅ X
    GSet-repr-iso = iso f g α β
      where
        f : GSetMorphism G X → X
        f (ϕ , _) = ϕ e

        g : X → GSetMorphism G X
        g x = (ϕ , ϕ-mor)
          where
            ϕ : G → X
            ϕ g = g ◂ x

            ϕ-mor : IsGSetMorphism ϕ
            ϕ-mor g₁ g₂ = ◂-hom g₁ g₂ x

        α : (ϕ : GSetMorphism G X) → g (f ϕ) ≡ ϕ
        α (ϕ , ϕ-mor) = gsetmorphism-equality G X hX _ _
          (funext λ g → sym (GSet-repr ϕ ϕ-mor g))

        β : (x : X) → f (g x) ≡ x
        β x = (IsMSet.◂-id xG) x