module Soat.FirstOrder.Algebra

import Control.Relation

import Soat.Data.Product
import Soat.FirstOrder.Signature
import Soat.Relation

%default total
%hide Control.Relation.Equivalence

public export
algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t

public export
algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t

public export
record RawAlgebra (0 sig : Signature) where
  constructor MakeRawAlgebra
  0 U : sig.T -> Type
  sem : sig `algebraOver` U

public export
MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))

public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
  constructor MkIsAlgebra
  equivalence : IEquivalence a.U rel
  semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
    -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')

public export
record Algebra (0 sig : Signature) where
  constructor MkAlgebra
  raw     : RawAlgebra sig
  0 rel   : IRel raw.U
  algebra : IsAlgebra sig raw rel

public export
(.setoid) : Algebra sig -> ISetoid sig.T
(.setoid) a = MkISetoid a.raw.U a.rel a.algebra.equivalence

public export
record IsHomomorphism
  {0 sig : Signature} (a, b : Algebra sig)
  (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
  where
  constructor MkIsHomomorphism
  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm')
  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
    -> b.rel t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))

public export
record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
  where
  constructor MkHomomorphism
  f    : (t : sig.T) -> a.raw.U t -> b.raw.U t
  homo : IsHomomorphism a b f