open import SOAS.Common

-- Free construction with respect to a forgetful functor between categories
module SOAS.Construction.Free {β„‚ π•Š : Category 1β„“ 0β„“ 0β„“}
                               (U : Functor π•Š β„‚) where

open import Categories.Adjoint
import Categories.Morphism.Reasoning as MR
open import Categories.Category.Equivalence using (WeakInverse; StrongEquivalence)
open import Categories.Adjoint.Properties
open import Categories.Monad


private module β„‚ = Category β„‚
private module π•Š = Category π•Š
private module U = Functor U

-- Mapping from an object of the carrier category to the carrier of an object
-- from the structure category
_β†ͺ_ : β„‚.Obj β†’ π•Š.Obj β†’ Set
C β†ͺ S = β„‚ [ C , U.β‚€ S ]


-- Definition of F being a free structure over a carrier C:
-- any carrier map c : C β†’ S into the carrier of a structure S factorises
-- through a unique extension of c to a structure homomorphism cΜ‚ : F C β†’ S:
--
--           ⌊-βŒ‹
--   C ────────────── FC
--  ╰─────── S ───────╯
--      c         cΜ‚

record FreeConstruction (F : β„‚.Obj β†’ π•Š.Obj)
                        (C : β„‚.Obj)
                        (embed : C β†ͺ F C)
                        (S : π•Š.Obj)
                        (c : C β†ͺ S)
                        : Set₁ where

  field
    -- Given another structure S, any mapping from C to the carrier of S can be
    -- extended into a structure homomorphism from F C to S.
    extend : π•Š [ F C , S ]

    -- Any map from C to the carrier of a structure S factors through the
    -- embedding and extension
    factor : U.₁ extend β„‚.∘ embed β„‚.β‰ˆ c

    -- Extension is the unique factorising morphism
    unique : (e : π•Š [ F C , S ])
           β†’ (p : (U.₁ e β„‚.∘ embed) β„‚.β‰ˆ c)
           β†’ π•Š [ e β‰ˆ extend ]

record FreeMapping (F : β„‚.Obj β†’ π•Š.Obj) : Set₁ where

  field
    embed : {C : β„‚.Obj} β†’ C β†ͺ F C
    univ  : (C : β„‚.Obj) (S : π•Š.Obj)(c : C β†ͺ S)
          β†’ FreeConstruction F C embed S c

  module Universal C S c = FreeConstruction (univ C S c)

  module _ {C : β„‚.Obj} {S : π•Š.Obj}(c : C β†ͺ S) where
    open Universal C S c public

  open MR β„‚
  open β„‚.HomReasoning
  private module π•ŠR = π•Š.HomReasoning
  open NT

  -- The uniqueness of the factors means that any two morphisms
  -- that factorise the same arrow must be equal
  equate : {C : β„‚.Obj}{S : π•Š.Obj}
        β†’ (f g : π•Š [ F C , S ])
        β†’ (p : U.₁ f β„‚.∘ embed β„‚.β‰ˆ U.₁ g β„‚.∘ embed)
        β†’ π•Š [ f β‰ˆ g ]
  equate f g p = unique _ f p π•ŠR.β—‹ π•ŠR.⟺ (unique _ g β„‚.Equiv.refl)

  -- Infix shorthand
  [_≋_]! : {C : β„‚.Obj}{S : π•Š.Obj}
        β†’ (f g : π•Š [ F C , S ])
        β†’ (p : U.₁ f β„‚.∘ embed β„‚.β‰ˆ U.₁ g β„‚.∘ embed)
        β†’ π•Š [ f β‰ˆ g ]
  [ f ≋ g ]! p = equate f g p

  -- Extensions of equal embeddings are equal
  extend-cong : {C : β„‚.Obj}{S : π•Š.Obj}(c₁ cβ‚‚ : C β†ͺ S)
             β†’ β„‚ [ c₁ β‰ˆ cβ‚‚ ] β†’ π•Š [ extend c₁ β‰ˆ extend cβ‚‚ ]
  extend-cong {C}{S} c₁ cβ‚‚ p = unique _ (extend c₁) (factor c₁ β—‹ p)


  -- | Freeness makes F into a functor

  map : {C D : β„‚.Obj} β†’ C β„‚.β‡’ D β†’ F C π•Š.β‡’ F D
  map {C}{D} f = extend (embed β„‚.∘ f)

  embed-commute : {C D : β„‚.Obj}(f : C β„‚.β‡’ D)
               β†’ embed β„‚.∘ f β„‚.β‰ˆ (U.₁ (map f) β„‚.∘ embed)
  embed-commute {C}{D} f = ⟺ (factor (embed β„‚.∘ f))

  identity : {C : β„‚.Obj} β†’ map (β„‚.id {C}) π•Š.β‰ˆ π•Š.id
  identity {C} = π•ŠR.⟺ $αΆ  unique _ π•Š.id (begin
         U.₁ π•Š.id β„‚.∘ embed  β‰ˆβŸ¨ U.identity ⟩∘⟨refl ⟩
         β„‚.id β„‚.∘ embed      β‰ˆβŸ¨ id-comm-sym ⟩
         embed β„‚.∘ β„‚.id      ∎)

  homomorphism : {C D E : β„‚.Obj} {f : β„‚ [ C , D ]} {g : β„‚ [ D , E ]}
              β†’ π•Š [ map (β„‚ [ g ∘ f ])
               β‰ˆ π•Š [ map g ∘ map f ] ]
  homomorphism {C}{D}{E}{f}{g} = π•ŠR.⟺ $αΆ  unique _ (π•Š [ map g ∘ map f ]) (begin
         U.₁ (map g π•Š.∘ map f) β„‚.∘ embed           β‰ˆβŸ¨ pushΛ‘ U.homomorphism ⟩
         U.₁ (map g)  β„‚.∘  U.₁ (map f)  β„‚.∘ embed  β‰ˆβŸ¨ pushΚ³ (⟺ (embed-commute f)) ⟩
         (U.₁ (map g)  β„‚.∘  embed) β„‚.∘ f           β‰ˆβŸ¨ pushΛ‘ (⟺ (embed-commute g)) ⟩
         embed β„‚.∘ g β„‚.∘ f                          ∎)

  -- Free functor from β„‚ to π•Š
  Free : Functor β„‚ π•Š
  Free = record
    { Fβ‚€ = F
    ; F₁ = map
    ; identity = identity
    ; homomorphism = homomorphism
    ; F-resp-β‰ˆ = Ξ» {C}{D}{f}{g} p β†’
          extend-cong (embed β„‚.∘ f) (embed β„‚.∘ g) (β„‚.∘-resp-β‰ˆΚ³ p)
    }

  module F = Functor Free

  -- | Freeness also induces a free-forgetful adjunction

  -- Embedding is a natural transformation
  embed-NT : NT idF (U ∘F Free)
  embed-NT = ntHelper record
    { Ξ· = Ξ» C β†’ embed
    ; commute = embed-commute
    }

  -- Extension of the identity on US is a natural transformation
  extract : (S : π•Š.Obj) β†’ F (U.β‚€ S) π•Š.β‡’ S
  extract S = extend β„‚.id

  -- Extraction is a natural transformation
  extract-NT : NT (Free ∘F U) idF
  extract-NT = ntHelper record
    { Ξ· = extract
    ; commute = Ξ» {S}{T} f β†’ [ extract T π•Š.∘ F.₁ (U.₁ f) ≋ f π•Š.∘ extract S ]!
        (begin
             U.₁ (extract T π•Š.∘ F.₁ (U.₁ f)) β„‚.∘ embed
        β‰ˆβŸ¨ pushΛ‘ U.homomorphism ⟩
             U.₁ (extract T) β„‚.∘ U.₁ (F.₁ (U.₁ f)) β„‚.∘ embed
        β‰ˆβŸ¨ refl⟩∘⟨ sym-commute embed-NT (U.₁ f) ⟩
             U.₁ (extract T) β„‚.∘ embed β„‚.∘ U.₁ f
        β‰ˆβŸ¨ pullΛ‘ (factor β„‚.id) β—‹ β„‚.identityΛ‘ ⟩
             U.₁ f
        β‰ˆΛ˜βŸ¨ (refl⟩∘⟨ factor β„‚.id) β—‹ β„‚.identityΚ³ ⟩
             U.₁ f β„‚.∘ U.₁ (extract S) β„‚.∘ embed
        β‰ˆΛ˜βŸ¨ pushΛ‘ U.homomorphism ⟩
             U.₁ (f π•Š.∘ extract S) β„‚.∘ embed
        ∎)
    }

  -- The free-forgetful adjunction arising from the universal morphisms
  Free⊣Forgetful : Free ⊣ U
  Free⊣Forgetful = record
    { unit = embed-NT
    ; counit = extract-NT
    ; zig = Ξ» {C} β†’ [ extract (F.β‚€ C) π•Š.∘ F.₁ embed ≋ π•Š.id ]!
        (begin
             U.₁ (extract (F.β‚€ C) π•Š.∘ F.₁ embed) β„‚.∘ embed
         β‰ˆβŸ¨ pushΛ‘ U.homomorphism ⟩
             U.₁ (extract (F.β‚€ C)) β„‚.∘ U.₁ (F.₁ embed) β„‚.∘ embed
         β‰ˆβŸ¨ refl⟩∘⟨ (sym-commute embed-NT embed) ⟩
             U.₁ (extract (F.β‚€ C)) β„‚.∘ (embed β„‚.∘ embed)
         β‰ˆβŸ¨ pullΛ‘ (factor (β„‚.id)) ⟩
             β„‚.id β„‚.∘ embed
         β‰ˆΛ˜βŸ¨ U.identity ⟩∘⟨refl ⟩
             U.₁ π•Š.id β„‚.∘ embed
         ∎)
    ; zag = factor β„‚.id
    }

  FreeMonad : Monad β„‚
  FreeMonad = adjointβ‡’monad Free⊣Forgetful