From 121965c3e550f285d3a428cbb6da10c97bfa9846 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 6 Dec 2022 13:50:12 +0000 Subject: refactor: rename pwSetoid -> Product. --- src/Soat/FirstOrder/Algebra/Coproduct.idr | 2 +- src/Soat/FirstOrder/Term.idr | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Soat/FirstOrder') diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index 88db184..548beed 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -175,7 +175,7 @@ termToCoproduct x y = MkHomomorphism { func = MkIndexedSetoidHomomorphism (\_ => id) (\t, _, _ => tmRelImpliesCoprodRel) , semHomo = \op, tms => Call op $ - reflect (index (pwSetoid (CoproductAlgebra x y).setoid) _) $ + reflect (index (Product (CoproductAlgebra x y).setoid) _) $ sym $ mapId tms } diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index ee17093..2042d2f 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -159,7 +159,7 @@ bindHomo env = MkHomomorphism } , semHomo = \op, tms => a.algebra.semCong op $ - reflect (index (pwSetoid a.setoid) _) $ + reflect (index (Product a.setoid) _) $ bindTermsIsMap {a = a.raw} env.H tms } @@ -203,7 +203,7 @@ bindsUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.se -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) -> Pointwise a.relation (map f.func.H tms) (bindTerms {a = a.raw} env.H tms) -bindsUnique env f cong ts = CalcWith (index (pwSetoid a.setoid) _) $ +bindsUnique env f cong ts = CalcWith (index (Product a.setoid) _) $ |~ map f.func.H ts ~~ map (\_ => bindTerm {a = a.raw} env.H) ts ...( bindsUnique' f (bindHomo env) cong ts ) ~~ bindTerms {a = a.raw} env.H ts .=<( bindTermsIsMap {a = a.raw} env.H ts ) -- cgit v1.2.3