module Soat.FirstOrder.Algebra import Data.Morphism.Indexed import Data.Setoid.Indexed import public Soat.Data.Product import Soat.FirstOrder.Signature %default total %hide Control.Relation.Equivalence infix 5 ~> public export 0 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 record RawAlgebra (0 sig : Signature) where constructor MkRawAlgebra 0 U : sig.T -> Type sem : sig `algebraOver` U public export record RawSetoidAlgebra (0 sig : Signature) where constructor MkRawSetoidAlgebra raw : RawAlgebra sig 0 relation : IRel raw.U public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where constructor MkIsAlgebra 0 relation : IRel a.U equivalence : IEquivalence a.U relation semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity} -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms') public export record Algebra (0 sig : Signature) where constructor MkAlgebra raw : RawAlgebra sig algebra : IsAlgebra sig raw public export 0 (.relation) : (0 a : Algebra sig) -> IRel a.raw.U (.relation) a = a.algebra.relation public export (.setoid) : Algebra sig -> ISetoid sig.T (.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence public export (.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig (.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation public export record (~>) {0 sig : Signature} (a, b : Algebra sig) where constructor MkHomomorphism func : (t : sig.T) -> a.raw.U t -> b.raw.U t cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm') semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity) -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms)) public export id : {a : Algebra sig} -> a ~> a id = MkHomomorphism { func = \_ => id , cong = \_ => id , semHomo = \op, tms => (a.algebra.equivalence _).equalImpliesEq $ sym $ cong (a.raw.sem op) $ mapId tms } public export (.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c (.) f g = MkHomomorphism { func = \t => f.func t . g.func t , cong = \t => f.cong t . g.cong t , semHomo = \op, tms => (c.algebra.equivalence _).transitive (f.cong _ $ g.semHomo op tms) $ (c.algebra.equivalence _).transitive (f.semHomo op (map g.func tms)) $ (c.algebra.equivalence _).equalImpliesEq $ sym $ cong (c.raw.sem op) $ mapComp tms }