diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index bc3defb..57b8a51 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -103,13 +103,13 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur public export record Algebra (0 sig : Signature) where constructor MkAlgebra - raw : RawAlgebra sig - 0 rel : IRel (uncurry raw.U) - algebra : IsAlgebra sig raw rel + raw : RawAlgebra sig + 0 relation : IRel (uncurry raw.U) + algebra : IsAlgebra sig raw relation public export (.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T)) -(.setoid) a = MkISetoid (uncurry a.raw.U) a.rel a.algebra.equivalence +(.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence public export record IsHomomorphism @@ -118,19 +118,19 @@ record IsHomomorphism where constructor MkIsHomomorphism cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx} - -> a.rel (t, ctx) tm tm' -> b.rel (t, ctx) (f t ctx tm) (f t ctx tm') + -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (f t ctx tm) (f t ctx tm') renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx) - -> b.rel (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm) + -> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm) semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) -> (tms : extend a.raw.U ctx ^ op.arity) - -> b.rel (t, ctx) + -> b.relation (t, ctx) (f t ctx $ a.raw.sem ctx op tms) (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms) varHomo : forall t, ctx . (i : Elem t ctx) - -> b.rel (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i) + -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i) substHomo : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx') -> (tms : flip a.raw.U ctx ^ ctx') - -> b.rel (t, ctx) + -> b.relation (t, ctx) (f t ctx $ a.raw.subst t ctx tm tms) (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms) |