summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Algebra/Coproduct.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr')
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr118
1 files changed, 69 insertions, 49 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index d0b1b14..a29080f 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -73,14 +73,13 @@ Coproduct x y = MakeRawAlgebra
}
public export
-CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel'
- -> IsAlgebra sig (Coproduct x y)
- ((~=~) (MkRawAlgebraWithRelation x rel) (MkRawAlgebraWithRelation y rel'))
-CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
+CoproductIsAlgebra : (x, y : Algebra sig)
+ -> IsAlgebra sig (Coproduct x.raw y.raw) ((~=~) x.rawWithRelation y.rawWithRelation)
+CoproductIsAlgebra x y = MkIsAlgebra
{ equivalence = \t => MkEquivalence
{ refl = MkReflexive $ coprodRelRefl
- (\t => (xIsAlgebra.equivalence t).refl)
- (\t => (yIsAlgebra.equivalence t).refl)
+ (\t => (x.algebra.equivalence t).refl)
+ (\t => (y.algebra.equivalence t).refl)
_
, sym = MkSymmetric $ Sym
, trans = MkTransitive $ Trans
@@ -90,44 +89,88 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
public export
CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra
-
-public export
-injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
-injectLIsHomo = MkIsHomomorphism
- { cong = \_ => DoneL
- , semHomo = InjectL
- }
-
-public export
-injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
-injectRIsHomo = MkIsHomomorphism
- { cong = \_ => DoneR
- , semHomo = InjectR
- }
+CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x y
public export
injectLHomo : Homomorphism x (CoproductAlgebra x y)
-injectLHomo = MkHomomorphism _ $ injectLIsHomo
+injectLHomo = MkHomomorphism _ $ MkIsHomomorphism { cong = \_ => DoneL , semHomo = InjectL }
public export
injectRHomo : Homomorphism y (CoproductAlgebra x y)
-injectRHomo = MkHomomorphism _ $ injectRIsHomo
+injectRHomo = MkHomomorphism _ $ MkIsHomomorphism { cong = \_ => DoneR , semHomo = InjectR }
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))
+coproduct f g = bindTerm (\i => either (f i) (g i))
public export
coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
-> CoproductSet sig x y ^ ts -> z.U ^ ts
-coproducts f g _ = bindTerms (\i => either (f i) (g i))
+coproducts f g = bindTerms (\i => either (f i) (g i))
+
+public export
+coproductCong' : {x, y, z : Algebra sig}
+ -> (f, f' : Homomorphism x z) -> (g, g' : Homomorphism y z)
+ -> (congL : (t : _) -> {i, j : x.raw.U t} -> x.relation t i j
+ -> z.relation t (f.func t i) (f'.func t j))
+ -> (congR : (t : _) -> {i, j : y.raw.U t} -> y.relation t i j
+ -> z.relation t (g.func t i) (g'.func t j))
+ -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm'
+ -> z.relation t
+ (coproduct {z = z.raw} f.func g.func t tm)
+ (coproduct {z = z.raw} f'.func g'.func t tm')
+
+public export
+coproductsCong' : {x, y, z : Algebra sig}
+ -> (f, f' : Homomorphism x z) -> (g, g' : Homomorphism y z)
+ -> (congL : (t : _) -> {i, j : x.raw.U t} -> x.relation t i j
+ -> z.relation t (f.func t i) (f'.func t j))
+ -> (congR : (t : _) -> {i, j : y.raw.U t} -> y.relation t i j
+ -> z.relation t (g.func t i) (g'.func t j))
+ -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
+ -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms'
+ -> Pointwise z.relation
+ (coproducts {z = z.raw} f.func g.func ts tms)
+ (coproducts {z = z.raw} f'.func g'.func ts tms')
+
+coproductCong' f f' g g' congL congR _ (DoneL eq) = congL _ eq
+coproductCong' f f' g g' congL congR _ (DoneR eq) = congR _ eq
+coproductCong' f f' g g' congL congR _ (Call op eqs) =
+ z.algebra.semCong op $
+ coproductsCong' f f' g g' congL congR _ eqs
+coproductCong' f f' g g' congL congR _ (InjectL op ts) = CalcWith (z.setoid.index _) $
+ |~ f.func _ (x.raw.sem op ts)
+ ~~ f'.func _ (x.raw.sem op ts) ...(congL _ $ (x.algebra.equivalence _).reflexive {x = x.raw.sem op ts})
+ ~~ z.raw.sem op (map f'.func ts) ...(f'.homo.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 f' g g' congL congR _ (InjectR op ts) = CalcWith (z.setoid.index _) $
+ |~ g.func _ (y.raw.sem op ts)
+ ~~ g'.func _ (y.raw.sem op ts) ...(congR _ $ (y.algebra.equivalence _).reflexive {x = y.raw.sem op ts})
+ ~~ z.raw.sem op (map g'.func ts) ...(g'.homo.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 f' g g' congL congR _ (Sym eq) =
+ (z.algebra.equivalence _).symmetric $
+ coproductCong' f' f g' g
+ (\t => (z.algebra.equivalence t).symmetric . congL t . (x.algebra.equivalence t).symmetric)
+ (\t => (z.algebra.equivalence t).symmetric . congR t . (y.algebra.equivalence t).symmetric)
+ _
+ eq
+coproductCong' f f' g g' congL congR _ (Trans eq eq') = (z.algebra.equivalence _).transitive
+ (coproductCong' f f g g f.homo.cong g.homo.cong _ eq)
+ (coproductCong' f f' g g' congL congR _ eq')
+
+coproductsCong' f f' g g' congL congR _ [] = []
+coproductsCong' f f' g g' congL congR _ (eq :: eqs) =
+ coproductCong' f f' g g' congL congR _ eq :: coproductsCong' f f' g g' congL congR _ eqs
public export
coproductCong : {x, y, z : Algebra sig}
-> (f : Homomorphism x z) -> (g : Homomorphism y z)
-> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm'
-> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
+coproductCong f g = coproductCong' f f g g f.homo.cong g.homo.cong
public export
coproductsCong : {x, y, z : Algebra sig}
@@ -135,30 +178,7 @@ coproductsCong : {x, y, z : Algebra sig}
-> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
-> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) 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 _ (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 (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 (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
-coproductCong f g _ (Trans eq eq') = (z.algebra.equivalence _).transitive
- (coproductCong f g _ eq)
- (coproductCong f g _ eq')
-
-coproductsCong f g _ [] = []
-coproductsCong f g _ (eq :: eqs) =
- coproductCong f g _ eq :: coproductsCong f g _ eqs
+coproductsCong f g = coproductsCong' f f g g f.homo.cong g.homo.cong
public export
coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:26:44 +0000