summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Data/Setoid/Product.idr4
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr2
-rw-r--r--src/Soat/FirstOrder/Term.idr4
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr26
4 files changed, 18 insertions, 18 deletions
diff --git a/src/Data/Setoid/Product.idr b/src/Data/Setoid/Product.idr
index 90510e5..6693d40 100644
--- a/src/Data/Setoid/Product.idr
+++ b/src/Data/Setoid/Product.idr
@@ -68,8 +68,8 @@ pwEquivalence eq = MkIndexedEquivalence
}
public export
-pwSetoid : IndexedSetoid a -> IndexedSetoid (List a)
-pwSetoid x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence)
+Product : IndexedSetoid a -> IndexedSetoid (List a)
+Product x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence)
-- Introductors and Eliminators
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 )
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 116b5e4..d80eeb1 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -65,7 +65,7 @@ public export
...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms))
...(a.algebra.semCong _ (MkOp (Op op.op)) $
- CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $
+ CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $
|~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)
~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms)
.=.(mapWrap (MkPair []) tms)
@@ -78,7 +78,7 @@ public export
.=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry f)
~~ a.raw.rename t f tm'
...(a.algebra.renameCong t f eq)) $
- (pwSetoid (a.setoidAt ctx)).equivalence.reflexive _ tms))
+ (Product (a.setoidAt ctx)).equivalence.reflexive _ tms))
}
public export
@@ -90,7 +90,7 @@ public export
{ H = \t, tm => a.raw.subst t ctx tm tms
, homomorphic = \t, _, _, eq =>
a.algebra.substCong t ctx eq $
- (pwSetoid (a.setoidAt _)).equivalence.reflexive _ tms
+ (Product (a.setoidAt _)).equivalence.reflexive _ tms
}
, semHomo = \op, tms' => CalcWith (index a.setoid _) $
|~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms
@@ -98,7 +98,7 @@ public export
...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms'))
...(a.algebra.semCong ctx (MkOp (Op op.op)) $
- CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
+ CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
|~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')
~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms')
.=.(mapWrap (MkPair []) tms')
@@ -106,7 +106,7 @@ public export
...(wrapIntro $
mapIntro' (\t, eq =>
a.algebra.substCong t ctx eq $
- CalcWith (index (pwSetoid (a.setoidAt _)) _) $
+ CalcWith (index (Product (a.setoidAt _)) _) $
|~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms
~~ map (\t => id) tms
...(mapIntro'' (\t, tm, tm', eq =>
@@ -118,10 +118,10 @@ public export
...(a.algebra.renameId t ctx tm)
~~ tm'
...(eq)) $
- (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _)
+ (Product (a.setoidAt _)).equivalence.reflexive _ _)
~~ tms
.=.(mapId tms)) $
- (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _))
+ (Product (a.setoidAt _)).equivalence.reflexive _ _))
}
-- renameBodyFunc : (f : ctx `Sublist` ctx')
@@ -179,7 +179,7 @@ InitialIsAlgebra sig = MkIsAlgebra
}
, semNat = \f, (MkOp (Op op)), tms =>
Call (MkOp op) $
- CalcWith (index (pwSetoid (freeAlg _).setoid) _) $
+ CalcWith (index (Product (freeAlg _).setoid) _) $
|~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms)
~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms)
.=.(bindTermsIsMap {a = Free _} _ _)
@@ -189,7 +189,7 @@ InitialIsAlgebra sig = MkIsAlgebra
{rel = \_ => Equal}
{a = freeAlg _}
(\_, Refl => Done $ curryUncurry (curry f) _)) $
- (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
+ (Product (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms)
.=.(mapUnwrap (MkPair []) tms)
, varNat = \_, _ => Done Refl
@@ -239,7 +239,7 @@ InitialIsAlgebra sig = MkIsAlgebra
}
, substCompat = \ctx, (MkOp (Op op)), tms, tms' =>
Call (MkOp op) $
- CalcWith (index (pwSetoid (freeAlg _).setoid) _) $
+ CalcWith (index (Product (freeAlg _).setoid) _) $
|~ bindTerms {a = Free _} (\_ => index tms') (unwrap (MkPair []) tms)
~~ map (\_ => bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms)
.=.(bindTermsIsMap {a = Free _} _ _)
@@ -258,7 +258,7 @@ InitialIsAlgebra sig = MkIsAlgebra
, cong = \i => Done $ sym $ trans (curryUncurry _ i) (curryUncurry id i)
, tm = index tms' _
}))) $
- (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
+ (Product (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
.=.(mapUnwrap (MkPair []) tms)
}
@@ -278,7 +278,7 @@ freeToInitialHomo sig ctx = MkHomomorphism
}
, semHomo = \(MkOp op), tms =>
Call (MkOp op) $
- reflect (index (pwSetoid ((InitialAlgebra sig).setoidAt ctx)) _) $
+ reflect (index (Product ((InitialAlgebra sig).setoidAt ctx)) _) $
sym $
trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId tms)
}
@@ -303,7 +303,7 @@ fromInitialHomo a = MkHomomorphism
(\i => a.algebra.equivalence.symmetric _ _ _ $ a.algebra.varNat f i)
, semHomo = \ctx, (MkOp (Op op)), tms =>
a.algebra.semCong ctx (MkOp (Op op)) $
- CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
+ CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
|~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) (unwrap (MkPair []) tms))
~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms))
.=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:26:43 +0000