Inline definition of IsHomomorphism.

1 files changed, 20 insertions, 29 deletions

diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 5e6d4ce..a98391b 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -96,28 +96,22 @@ CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
 CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
 
 public export
-injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
-injectLIsHomo = MkIsHomomorphism
-  { cong = \_ => DoneL
+injectLHomo : x ~> CoproductAlgebra x y
+injectLHomo = MkHomomorphism
+  { func    = \_ => Done . Left
+  , cong    = \_ => DoneL
   , semHomo = InjectL
   }
 
 public export
-injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
-injectRIsHomo = MkIsHomomorphism
-  { cong = \_ => DoneR
+injectRHomo : y ~> CoproductAlgebra x y
+injectRHomo = MkHomomorphism
+  { func    = \_ => Done . Right
+  , cong    = \_ => DoneR
   , semHomo = InjectR
   }
 
 public export
-injectLHomo : x ~> CoproductAlgebra x y
-injectLHomo = MkHomomorphism _ $ injectLIsHomo
-
-public export
-injectRHomo : y ~> CoproductAlgebra x y
-injectRHomo = MkHomomorphism _ $ injectRIsHomo
-
-public export
 coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U
 coproduct f g _ = bindTerm (\i => either (f i) (g i))
 
@@ -137,19 +131,19 @@ coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
   -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
   -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
 
-coproductCong f g _ (DoneL eq)       = f.homo.cong _ eq
-coproductCong f g _ (DoneR eq)       = g.homo.cong _ eq
+coproductCong f g _ (DoneL eq)       = f.cong _ eq
+coproductCong f g _ (DoneR eq)       = g.cong _ eq
 coproductCong f g _ (Call op eqs)    =
   z.algebra.semCong op $
   coproductsCong f g _ eqs
 coproductCong f g _ (InjectL op ts)  = CalcWith (z.setoid.index _) $
   |~ f.func _ (x.raw.sem op ts)
-  ~~ z.raw.sem op (map f.func ts)                                              ...(f.homo.semHomo op ts)
+  ~~ z.raw.sem op (map f.func ts)                                              ...(f.semHomo op ts)
   ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
   ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
 coproductCong f g _ (InjectR op ts)  = CalcWith (z.setoid.index _) $
   |~ g.func _ (y.raw.sem op ts)
-  ~~ z.raw.sem op (map g.func ts)                                               ...(g.homo.semHomo op ts)
+  ~~ z.raw.sem op (map g.func ts)                                               ...(g.semHomo op ts)
   ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
   ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
 coproductCong f g _ (Sym eq)         = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq
@@ -162,10 +156,11 @@ coproductsCong f g _ (eq :: eqs) =
   coproductCong f g _ eq :: coproductsCong f g _ eqs
 
 public export
-coproductIsHomo : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-  -> IsHomomorphism (CoproductAlgebra x y) z (coproduct {z = z.raw} f.func g.func)
-coproductIsHomo f g = MkIsHomomorphism
-  { cong = coproductCong f g
+coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+  -> CoproductAlgebra x y ~> z
+coproductHomo f g = MkHomomorphism
+  { func = coproduct {z = z.raw} f.func g.func
+  , cong = coproductCong f g
   , semHomo = \op, tms =>
     (z.algebra.equivalence _).equalImpliesEq $
     cong (z.raw.sem op) $
@@ -173,16 +168,12 @@ coproductIsHomo f g = MkIsHomomorphism
   }
 
 public export
-coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
-  -> CoproductAlgebra x y ~> z
-coproductHomo f g = MkHomomorphism _ $ coproductIsHomo f g
-
-public export
 termToCoproduct : (x, y : Algebra sig)
   -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
      CoproductAlgebra x y
-termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
-  { cong = \t => tmRelImpliesCoprodRel
+termToCoproduct x y = MkHomomorphism
+  { func    = \_ => id
+  , cong    = \t => tmRelImpliesCoprodRel
   , semHomo = \op, tms =>
     Call op $
     coprodsRelReflexive