module Soat.FirstOrder.Algebra.FreeExtension

import Data.Morphism.Indexed
import Data.Setoid.Indexed

import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Algebra.Coproduct
import Soat.FirstOrder.Signature
import Soat.FirstOrder.Term

%default total

public export
FreeExtension : (a : RawAlgebra sig) -> (v : sig.T -> Type) -> RawAlgebra sig
FreeExtension a v = Coproduct a (Free v)

public export
FreeExtensionAlgebra : (a : Algebra sig) -> (v : ISetoid sig.T) -> Algebra sig
FreeExtensionAlgebra a v = CoproductAlgebra a (FreeAlgebra v)

public export
extend : {a : RawAlgebra sig} -> {u : sig.T -> Type} -> (f : IFunc v u)
  -> IFunc (FreeExtension a v).U (FreeExtension a u).U
extend f = coproduct {z = FreeExtension a u}
  (\_ => Done . Left)
  (\t => Done . Right . free f t)

public export
extendHomo : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
  -> Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u)
extendHomo f = coproductHomo {z = FreeExtensionAlgebra a u}
  (injectLHomo {y = FreeAlgebra u})
  (compHomo injectRHomo (freeHomo f))

public export
extendCong : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
  -> (t : sig.T) -> {tm, tm' : (FreeExtension a.raw v.U).U t}
  -> (FreeExtensionAlgebra a v).relation t tm tm'
  -> ((FreeExtensionAlgebra a u).relation t `on` extend {a = a.raw} f.func t) tm tm'
extendCong f = coproductCong {z = FreeExtensionAlgebra a u}
  (injectLHomo {y = FreeAlgebra u})
  (compHomo injectRHomo (freeHomo f))

public export
extendUnique : {a : Algebra sig} -> {v, u : ISetoid sig.T}
  -> (f : IFunction v u)
  -> (g : Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u))
  -> (congL : {t : sig.T} -> (i : a.raw.U t)
        -> (FreeExtensionAlgebra a u).relation t (g.func t (Done (Left i))) (Done (Left i)))
  -> (congR : {t : sig.T} -> (i : Term sig v.U t)
        -> (FreeExtensionAlgebra a u).relation t
             (g.func t (Done (Right i)))
             (Done (Right (free f.func t i))))
  -> {t : sig.T} -> (tm : _)
  -> (FreeExtensionAlgebra a u).relation t (g.func t tm) (extend {a = a.raw} f.func t tm)
extendUnique f = coproductUnique {z = FreeExtensionAlgebra a u}
  (injectLHomo {y = FreeAlgebra u})
  (compHomo injectRHomo (freeHomo f))