-- {-# OPTIONS --universe-polymorphism #-}

open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
module free-monoid { c c₁ c₂ ℓ : Level }   where

open import Category.Sets
open import Category.Cat
open import HomReasoning
open import cat-utility
open import Relation.Binary.Core
open import  Relation.Binary.PropositionalEquality



infixr 40 _::_
data  List  (A : Set c ) : Set c where
   [] : List A
   _::_ : A -> List A -> List A


infixl 30 _++_
_++_ :   {A : Set c } -> List A -> List A -> List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

≡-cong = Relation.Binary.PropositionalEquality.cong 

list-id-l : { A : Set c } -> { x : List A } ->  [] ++ x ≡ x
list-id-l {_} {_} = refl
list-id-r : { A : Set c } -> { x : List A } ->  x ++ [] ≡ x
list-id-r {_} {[]} =   refl
list-id-r {A} {x :: xs} =  ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) 
list-assoc : {A : Set c} -> { xs ys zs : List A } ->
      ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
list-assoc  {_} {[]} {_} {_} = refl
list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( \y  -> x :: y ) 
         ( list-assoc {A} {xs} {ys} {zs} )
list-o-resp-≈ :  {A : Set c} ->  {f g : List A } → {h i : List A } → 
                  f ≡  g → h ≡  i → (h ++ f) ≡  (i ++ g)
list-o-resp-≈  {A} refl refl = refl
list-isEquivalence : {A : Set c} -> IsEquivalence {_} {_} {List A }  _≡_ 
list-isEquivalence {A} =      -- this is the same function as A's equivalence but has different types
   record { refl  = refl
     ; sym   = sym
     ; trans = trans
     } 

open import Algebra.FunctionProperties using (Op₁; Op₂)
open import Algebra.Structures
open import Data.Product


record ≡-Monoid : Set (suc c) where
  infixl 7 _∙_
  field
    Carrier  : Set c
    _∙_      : Op₂ Carrier
    ε        : Carrier
    isMonoid : IsMonoid _≡_ _∙_ ε

open ≡-Monoid

list  : (a : Set c) -> ≡-Monoid
list a = record {
    Carrier    =  List a
    ; _∙_      = _++_
    ; ε        = []
    ; isMonoid = record {
          identity = ( ( \x -> list-id-l {a}  ) , ( \x -> list-id-r {a} ) ) ;
          isSemigroup = record {
               assoc =  \x -> \y -> \z -> sym ( list-assoc {a} {x} {y} {z} )
             ; isEquivalence = list-isEquivalence
             ; ∙-cong = \x -> \y ->  list-o-resp-≈ y x
          }
      }
    }


record Monomorph ( a b : ≡-Monoid )  : Set (suc c) where
  field
      morph : Carrier a -> Carrier b  
      identity     :  morph (ε a)  ≡  ε b
      mdistr :  ∀{x y} -> morph ( _∙_ a x  y ) ≡ ( _∙_ b (morph  x ) (morph  y) )

open Monomorph

_+_ : { a b c : ≡-Monoid } -> Monomorph b c -> Monomorph a b -> Monomorph a c
_+_ {a} {b} {c} f g =  record {
      morph = \x ->  morph  f ( morph g x ) ;
      identity  = identity1 ;
      mdistr  = mdistr1 
   } where
      identity1 : morph f ( morph g (ε a) )  ≡  ε c
      -- morph f (ε b) = ε c ,  morph g (ε a) ) ≡  ε b
      -- morph f  morph g (ε a) ) ≡  morph f (ε b) = ε c
      identity1 = trans ( ≡-cong (morph f ) ( identity g ) )  ( identity f )
      mdistr1 :  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
      --  ∀{x y} -> morph f ( morph g ( _∙_ a x  y )) ≡ morph f ( ( _∙_ c  (morph  g x )) (morph  g y) ) 
      --  ∀{x y} -> morph f ( ( _∙_ c  (morph  g x )) (morph  g y) )  ≡ ( _∙_ c (morph f (morph  g x )) (morph f (morph  g y) ) )
      mdistr1 = trans  (≡-cong (morph f ) ( mdistr g) ) ( mdistr f ) 

M-id : { a : ≡-Monoid } -> Monomorph a a 
M-id = record { morph = \x -> x  ; identity = refl ; mdistr = refl }

_==_ : { a b : ≡-Monoid } -> Monomorph a b -> Monomorph a b -> Set c 
_==_  f g =  morph f ≡ morph g

isMonoidCategory : IsCategory ≡-Monoid Monomorph _==_  _+_  (M-id)
isMonoidCategory  = record  { isEquivalence =  isEquivalence1 
                    ; identityL =  refl
                    ; identityR =  refl
                    ; associative = refl
                    ; o-resp-≈ =    \{a} {b} {c} {f} {g} {h} {i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
                    }
     where
        o-resp-≈ :  {a b c :  ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } → 
                          f ==  g → h ==  i → (h + f) ==  (i + g)
        o-resp-≈  {A} refl refl = refl
        isEquivalence1 : { a b : ≡-Monoid } -> IsEquivalence {_} {_} {Monomorph a b}  _==_ 
        isEquivalence1  =      -- this is the same function as A's equivalence but has different types
           record { refl  = refl
             ; sym   = sym
             ; trans = trans
             } 
MonoidCategory : Category _ _ _
MonoidCategory  =
  record { Obj =  ≡-Monoid 
         ; Hom = Monomorph
         ; _o_ = _+_  
         ; _≈_ = _==_
         ; Id  =  M-id
         ; isCategory = isMonoidCategory 
           }


A = Sets {c}
B = MonoidCategory  

open Functor

U : Functor B A
U = record {
       FObj = \m -> Carrier m ;
       FMap = \f -> morph f ;
       isFunctor = record {
              ≈-cong   = \x -> x
             ; identity = refl
             ; distr    = refl
       }
   } 

-- FObj 

Generator : Obj A -> Obj B
Generator s =  list s

-- η

postulate eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )

-- solution

solution : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (Generator a ) b 
solution = {!!}

universalMapping :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → 
                             _≈_ A  ( FMap U ( f * ) o  η a ]  ≈ f ]
universalMapping =   ?
uniquness :   {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g :  Hom B (F a) b } → 
                             A [ A [ FMap U g o  η a ]  ≈ f ] → B [ f * ≈ g ]
uniquness = ?


FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta 
FreeMonoidUniveralMapping = 
    record {
       _* = solution ; 
       isUniversalMapping = record {
             universalMapping = universalMapping ; 
             uniquness = uniquness
       }
    }