-- open import Algebra.Group.Free hiding (Free⊣Forget ; Free)
open import Algebra.Group

open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Equivalence
open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Instances.Comma
open import Cat.Diagram.Monad hiding (Free ; Forget ; Free⊣Forget)
open import Cat.Functor.Base
open import Cat.Prelude

module wip.test where

{-
import Algebra.Group.Free as F

Groups : ∀ ℓ → Precategory (lsuc ℓ) ℓ
Groups ℓ = c where
  open Precategory
  open Group-hom
  open Group-on

  c : Precategory _ _
  c .Ob = Group ℓ
  c .Hom A B = Group[ A ⇒ B ]
  c .Hom-set _ (B , bg) =
    Σ-is-hlevel 2 (fun-is-hlevel 2 (bg .has-is-set))
                  λ _ → is-prop→is-set Group-hom-is-prop
  c .id .fst = λ x → x
  c .id .snd = record { pres-⋆ = λ _ _ → refl }
  c ._∘_ {x} {y} {z} (f , fh) (g , gh) = (λ x → f (g x)) , fogh where abstract
    fogh : Group-hom x z (λ x → f (g x))
    fogh .pres-⋆ x y = ap f (gh .pres-⋆ x y) ∙ fh .pres-⋆ _ _
  c .idr f = Σ-prop-path (λ _ → Group-hom-is-prop) refl
  c .idl f = Σ-prop-path (λ _ → Group-hom-is-prop) refl
  c .assoc f g h = Σ-prop-path (λ _ → Group-hom-is-prop) refl

private variable ℓ : Level

open Functor

Forget : Functor (Groups ℓ) (Sets ℓ)
Forget .F₀ (G , gg) = G , gg .Group-on.has-is-set
Forget .F₁ = fst
Forget .F-id = refl
Forget .F-∘ _ _ = refl

Forget-has-univ : ∀ s → Universal-morphism s (Forget {ℓ})
Forget-has-univ (S , S-set) = um where
  open Group-hom
  open Group-on
  open Initial
  open ↓Obj
  open ↓Hom

  it : ↓Obj _ _
  it .x = tt
  it .y = F.Free S
  it .map = inc

  um : Initial _
  um .bot = it
  um .has⊥ other = contr factor unique where
    factor : ↓Hom _ _ it other
    factor .α  = tt
    factor .β  = equiv→inverse (F.Free⊣Forget {A = S , S-set} .snd) (other .map)
    factor .sq = refl

    unique : ∀ x → factor ≡ x
    unique factoring = ↓Hom-path _ _ refl path where abstract
      path : factor .β ≡ factoring .β
      path = Σ-prop-path (λ _ → Group-hom-is-prop)
        (funext
          (Free-elim-prop _ (λ _ → y other .snd .has-is-set _ _)
            (λ x → happly (factoring .sq) _)
            (λ _ _ p q → ap₂ (other .y .snd ._⋆_) p q
                      ∙ sym (factoring .β .snd .pres-⋆ _ _))
            (λ _ p → ap (other .y .snd .inverse) p
                   ∙ sym (pres-inv (factoring .β .snd) _))
            (sym (pres-id (factoring .β .snd)))))

Free : Functor (Sets ℓ) (Groups ℓ)
Free = universal-maps→L _ Forget-has-univ

Free⊣Forget : Free {ℓ} ⊣ Forget
Free⊣Forget = universal-maps→L⊣R _ Forget-has-univ

{-
Group-is-monadic : is-monadic (Free⊣Forget {ℓ})
Group-is-monadic {ℓ} = ff+split-eso→is-equivalence ff seso where
  C = Comparison (Free⊣Forget {ℓ})
  module C = Functor C

  ff : is-fully-faithful C
  ff = is-iso→is-equiv (iso from rinv linv) where
    open Algebra-hom
    open Group-hom

    from : Algebra-hom _ _ _ → Group[ _ ⇒ _ ]
    from map .fst = map .morphism
    from map .snd .pres-⋆ x y = happly (map .commutes) (inc x ◆ inc y)

    rinv : is-right-inverse from C.₁
    rinv x = Algebra-hom-path refl

    linv : is-left-inverse from C.₁
    linv x = Σ-prop-path (λ _ → Group-hom-is-prop) refl

  import Cat.Reasoning (Eilenberg-Moore (L∘R (Free⊣Forget {ℓ}))) as EM

  seso : is-split-eso C
  seso (Y , Y-alg) .fst = F.Free (Y .fst)
  seso (Y , Y-alg) .snd = EM.make-iso f g {!   !} {!   !} where
    open Algebra-hom
    open Algebra-on
    open Group-hom

    f : Algebra-hom _ _ (Y , Y-alg)
    f .morphism = Y-alg .ν
    f .commutes = {!   !}

    linv : is-left-inverse inc (Y-alg .ν)
    linv x =
      Free-elim-prop
        (λ x₁ → inc (Y-alg .ν x) ≡ x)
        {!   !} {!   !} {!   !} {!   !} {!   !} {!  x !}

    g : Algebra-hom _ (Y , Y-alg) _
    g .morphism = inc
    g .commutes = funext (Free-elim-prop _
      (λ _ → squash _ _)
      (λ x → ap inc (happly (Y-alg .ν-unit) x))
      (λ x y p q → ap inc (sym (happly (Y-alg .ν-mult) (inc x ◆ inc y)))
                ·· ap₂ (λ a b → inc (Y-alg .ν (a ◆ b))) p q
                ·· {! refl !})
      {!   !}
      {!   !})
      -} -}