@@ -177,7 +177,7 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
177177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
178178
179179||| Sets equipped with a binary operation that is commutative, associative and
180−||| idempotent and supplied with a neutral element. Must satisfy the following
180+||| idempotent and supplied with a unitary element. Must satisfy the following
181181||| laws:
182182|||
183183||| + Associativity of join:
@@ -186,8 +186,8 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
186186||| forall a b, join a b == join b a
187187||| + Idempotency of join:
188188||| forall a, join a a == a
189−||| + Bottom:
190−||| forall a, join a bottom == bottom
189+||| + Bottom (Unitary Element):
190+||| forall a, join a bottom == a
191191|||
192192||| Join semilattices capture the notion of sets with a "least upper bound"
193193||| equipped with a "bottom" element.
@@ -195,10 +195,10 @@ class JoinSemilattice a => BoundedJoinSemilattice a where
195195 bottom : a
196196
197197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
198− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
198+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e
199199
200200||| Sets equipped with a binary operation that is commutative, associative and
201−||| idempotent and supplied with a neutral element. Must satisfy the following
201+||| idempotent and supplied with a unitary element. Must satisfy the following
202202||| laws:
203203|||
204204||| + Associativity of meet:
@@ -207,8 +207,8 @@ class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJo
207207||| forall a b, meet a b == meet b a
208208||| + Idempotency of meet:
209209||| forall a, meet a a == a
210−||| + Top:
211−||| forall a, meet a top == top
210+||| + Top (Unitary Element):
211+||| forall a, meet a top == a
212212|||
213213||| Meet semilattices capture the notion of sets with a "greatest lower bound"
214214||| equipped with a "top" element.
@@ -216,7 +216,7 @@ class MeetSemilattice a => BoundedMeetSemilattice a where
216216 top : a
217217
218218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
219− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
219+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = e
220220
221221||| Sets equipped with two binary operations that are both commutative,
222222||| associative and idempotent, along with absorbtion laws for relating the two