fixup: wording + change opaque for abstract

src/Order/Base.lagda.md

@@ -29,7 +29,7 @@ notions of "order" in mathematics:
   When ordering the naturals, the integers, and the rationals, we can
   say more: they are _linear_ orders. That is, in addition to the
   properties of $\le$ required to be a poset, we have, for any pair of
-  elements,
+  elements $x$ and $y$,
 
   $$(x \le y) \lor (y \le x)\text{.}$$
 
@@ -114,18 +114,18 @@ which, _a priori_, might not be a proposition: we have not included the
 assumption that `Ob`{.Agda} is actually a set. Therefore, it might be
 the case that an identification between posets does _not_ correspond to
 an identification of the underlying types and one of the relation.
-However, since the "symmetric part" of $\le$, the relation $x \sim y$
+However, since the "symmetric part" of $\le$, the relation
 iff.
 
 $$
-(x \le y) \land (y \le x)\text{,}
+x \sim y = (x \le y) \land (y \le x)\text{,}
 $$
 
 is a reflexive mere relation which implies identity, the type of objects
 is automatically a set.
 
 ```agda
-  opaque
+  abstract
     Ob-is-set : is-set Ob
     Ob-is-set =
       identity-system→hlevel 1
@@ -138,7 +138,7 @@ is automatically a set.
 
 <!--
 ```agda
-  opaque
+  abstract
     ≤-refl' : ∀ {x y} → x ≡ y → x ≤ y
     ≤-refl' {x = x} p = subst (x ≤_) p ≤-refl