From 2bd69bf893b7e1ebe4186639526451caf2083b12 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 2 Dec 2022 14:14:44 +0000 Subject: WIP: Frex is free --- src/Soat/FirstOrder/Algebra.idr | 8 ++ src/Soat/FirstOrder/Algebra/Coproduct.idr | 118 +++++++++++++++----------- src/Soat/FirstOrder/Algebra/FreeExtension.idr | 58 +++++++++++++ src/Soat/FirstOrder/Term.idr | 118 +++++++++++++++++--------- 4 files changed, 213 insertions(+), 89 deletions(-) create mode 100644 src/Soat/FirstOrder/Algebra/FreeExtension.idr (limited to 'src/Soat/FirstOrder') diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index 245af6d..26370cc 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -104,3 +104,11 @@ compIsHomo fHomo gHomo = MkIsHomomorphism public export compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo + +public export +record Isomorphism {0 sig : Signature} (a, b : Algebra sig) where + constructor MkIsomorphism + to : Homomorphism a b + from : Homomorphism b a + fromTo : {t : sig.T} -> (x : a.raw.U t) -> a.relation t (from.func t $ to.func t x) x + toFrom : {t : sig.T} -> (x : b.raw.U t) -> b.relation t (to.func t $ from.func t x) x 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) diff --git a/src/Soat/FirstOrder/Algebra/FreeExtension.idr b/src/Soat/FirstOrder/Algebra/FreeExtension.idr new file mode 100644 index 0000000..675c65b --- /dev/null +++ b/src/Soat/FirstOrder/Algebra/FreeExtension.idr @@ -0,0 +1,58 @@ +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)) diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 4a51f94..dc0c182 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -15,25 +15,6 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where Done : (i : v t) -> Term sig v t Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t -public export -bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t - -public export -bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts - -bindTerm env (Done i) = env _ i -bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts) - -bindTerms env [] = [] -bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts - -public export -bindTermsIsMap : {auto a : RawAlgebra sig} - -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts) - -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms -bindTermsIsMap env [] = Refl -bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts) - -- FIXME: these names shouldn't be public. Indication of bad API design namespace Rel public export @@ -137,43 +118,86 @@ public export FreeAlgebra : ISetoid sig.T -> Algebra sig FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) +public export +inject : IFunc v (Term sig v) +inject _ = Done + +public export +injectFunc : IFunction v (FreeAlgebra v).setoid +injectFunc = MkIFunction (\_ => Done) (\_ => Done') + +public export +bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc (Term sig v) a.U + +public export +bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc ((^) (Term sig v)) ((^) a.U) + +bindTerm env _ (Done i) = env _ i +bindTerm env _ (Call op ts) = a.sem op (bindTerms env _ ts) + +bindTerms env _ [] = [] +bindTerms env _ (t :: ts) = bindTerm env _ t :: bindTerms env _ ts + +public export +free : IFunc v u -> IFunc (Term sig v) (Term sig u) +free f = bindTerm {a = Free u} (\i => inject i . f i) + +public export +bindTermsIsMap : {a : RawAlgebra sig} + -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts) + -> bindTerms (\tm => env tm) _ tms = map (bindTerm (\tm => env tm)) tms +bindTermsIsMap env [] = Refl +bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env _ t)) (bindTermsIsMap env ts) + public export bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v} -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y)) - -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm' - -> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm') + -> (t : sig.T) -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm' + -> a.relation t (bindTerm {a = a.raw} env t tm) (bindTerm {a = a.raw} env' t tm') public export bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v} -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y)) - -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms' - -> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms') + -> (ts : List sig.T) -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms' + -> Pointwise a.relation (bindTerms {a = a.raw} env _ tms) (bindTerms {a = a.raw} env' _ tms') -bindTermCong' cong (Done' i) = cong _ i -bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts) +bindTermCong' cong _ (Done' i) = cong _ i +bindTermCong' cong _ (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong _ ts) -bindTermsCong' cong [] = [] -bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts +bindTermsCong' cong _ [] = [] +bindTermsCong' cong _ (t :: ts) = bindTermCong' cong _ t :: bindTermsCong' cong _ ts + +public export +freeCong' : {u : ISetoid sig.T} -> {f, g : IFunc v u.U} -> {0 rel : IRel v} + -> (cong : (t : sig.T) -> {i, j : v t} -> rel t i j -> u.relation t (f t i) (g t j)) + -> (t : sig.T) -> {tm, tm' : Term sig v t} + -> (~=~) rel t tm tm' -> (~=~) u.relation t (free f t tm) (free g t tm') +freeCong' cong = bindTermCong' {a = FreeAlgebra u} (\i => Done' . cong i) public export bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid) - -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm' - -> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm') + -> (t : sig.T) -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm' + -> a.relation t (bindTerm {a = a.raw} env.func t tm) (bindTerm {a = a.raw} env.func t tm') bindTermCong env = bindTermCong' env.cong public export bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid) - -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms' + -> (ts : List sig.T) -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms' -> Pointwise a.relation - (bindTerms {a = a.raw} env.func tms) - (bindTerms {a = a.raw} env.func tms') + (bindTerms {a = a.raw} env.func ts tms) + (bindTerms {a = a.raw} env.func ts tms') bindTermsCong env = bindTermsCong' env.cong +public export +freeCong : {u : ISetoid sig.T} -> (f : IFunction v u) -> (t : sig.T) -> {tm, tm' : Term sig v.U t} + -> (~=~) v.relation t tm tm' -> (~=~) u.relation t (free f.func t tm) (free f.func t tm') +freeCong f = freeCong' f.cong + public export bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) - -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func) + -> IsHomomorphism (FreeAlgebra v) a (bindTerm {a = a.raw} env.func) bindIsHomo a env = MkIsHomomorphism - (\t, eq => bindTermCong env eq) + (bindTermCong env) (\op, tms => a.algebra.semCong op $ map (\t => (a.algebra.equivalence t).equalImpliesEq) $ @@ -185,14 +209,19 @@ bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (Fr bindHomo env = MkHomomorphism _ (bindIsHomo _ env) public export -bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} +freeHomo : {u : ISetoid sig.T} -> IFunction v u + -> Homomorphism {sig = sig} (FreeAlgebra v) (FreeAlgebra u) +freeHomo f = bindHomo $ compFunc injectFunc f + +public export +bindUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig} -> (f, g : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.relation t (f.func t tm) (g.func t tm) public export -bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} +bindsUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig} -> (f, g : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) @@ -213,7 +242,7 @@ bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.se -> (f : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) -> {t : sig.T} -> (tm : Term sig v.U t) - -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm) + -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func t tm) bindUnique env f = bindUnique' f (bindHomo env) public export @@ -221,8 +250,17 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s -> (f : Homomorphism (FreeAlgebra v) a) -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) - -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms) + -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func ts tms) bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $ |~ map f.func ts - ~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts ) - ~~ bindTerms {a = a.raw} env.func ts .=<( bindTermsIsMap {a = a.raw} env.func ts ) + ~~ map (bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts ) + ~~ bindTerms {a = a.raw} env.func _ ts .=<( bindTermsIsMap {a = a.raw} env.func ts ) + +public export +freeUnique : {v, u : ISetoid sig.T} -> (f : IFunction v u) + -> (g : Homomorphism (FreeAlgebra v) (FreeAlgebra u)) + -> (cong : {t : sig.T} -> (i : v.U t) + -> (FreeAlgebra u).relation t (g.func t (Done i)) (Done (f.func t i))) + -> {t : sig.T} -> (tm : Term sig v.U t) + -> (FreeAlgebra u).relation t (g.func t tm) (free f.func t tm) +freeUnique f = bindUnique $ compFunc injectFunc f -- cgit v1.2.3