*laser eyes* minor wording pass

src/Cat/Diagram/Coproduct.lagda.md

@@ -16,7 +16,7 @@ private variable
 ```
 -->
 
-# Coproducts
+# Coproducts {defines="coproduct"}
 
 The **coproduct** $P$ of two objects $A$ and $B$ (if it exists), is the
 smallest object equipped with "injection" maps $A \to P$, $B \to P$.  It

src/Cat/Diagram/Initial.lagda.md

@@ -15,7 +15,7 @@ open import Cat.Morphism C
 ```
 -->
 
-# Initial objects
+# Initial objects {defines="initial-object"}
 
 An object $\bot$ of a category $\mathcal{C}$ is said to be **initial**
 if there exists a _unique_ map to any other object:

src/Cat/Functor/Subcategory.lagda.md

@@ -12,7 +12,7 @@ import Cat.Reasoning
 module Cat.Functor.Subcategory where
 ```
 
-# Subcategories
+# Subcategories {defines="subcategory"}
 
 A **subcategory** $\cD \mono \cC$ is specified by a [predicate]
 $P : C \to \prop$ on objects, and a predicate $Q : P(x) \to P(y) \to \cC(x,y) \to \prop$
@@ -97,7 +97,7 @@ module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {subcat : Subcat C o' ℓ'} whe
   Subcat-hom-is-set = Iso→is-hlevel 2 eqv $
     Σ-is-hlevel 2 (Hom-set _ _) λ _ →
     is-hlevel-suc 1 (is-hom-prop _ _ _)
-    where unquoteDecl eqv = declare-record-iso eqv (quote Subcat-hom) 
+    where unquoteDecl eqv = declare-record-iso eqv (quote Subcat-hom)
 ```
 -->
 
@@ -240,7 +240,7 @@ the forgetful functor is pseudomonic.
 ## Univalent Subcategories
 
 Let $\cC$ be a [univalent] category. A subcategory of $\cC$ is univalent
-when the predicate on objects is a proposition. 
+when the predicate on objects is a proposition.
 
 [univalent]: Cat.Univalent.html
 

src/Order/Base.lagda.md

@@ -145,7 +145,7 @@ is-monotone-is-prop
   : ∀ {o o' ℓ ℓ'} {A : Type o} {B : Type o'}
   → (f : A → B) (P : Poset-on ℓ A) (Q : Poset-on ℓ' B)
   → is-prop (is-monotone f P Q)
-is-monotone-is-prop f P Q = 
+is-monotone-is-prop f P Q =
   Π-is-hlevel³ 1 λ _ _ _ → Poset-on.≤-thin Q
 
 Poset-structure : ∀ ℓ ℓ′ → Thin-structure {ℓ = ℓ} (ℓ ⊔ ℓ′) (Poset-on ℓ′)

src/Order/DCPO.lagda.md

@@ -28,13 +28,11 @@ private variable
 
 # Directed-Complete Partial Orders
 
-Let $(P, \le)$ be a [partial order]. A family of elements $f : I \to P$ is
+Let $(P, \le)$ be a [[partial order]]. A family of elements $f : I \to P$ is
 a **semi-directed family** if for every $i, j$, there merely exists
 some $k$ such $f i \le f k$ and $f j \le f k$. A semidirected family
 $f : I \to P$ is a **directed family** when $I$ is merely inhabited.
 
-[partial order]: Order.Base.html
-
 ```agda
 module _ {o ℓ} (P : Poset o ℓ) where
   open Poset P
@@ -49,8 +47,8 @@ module _ {o ℓ} (P : Poset o ℓ) where
       semidirected : is-semidirected-family f
 ```
 
-Note that if the indexing type of a family is a proposition, then the
-family is semi-directed.
+Note that any family whose indexing type is a proposition is
+automatically semi-directed:
 
 ```agda
   prop-indexed→semidirected
@@ -60,11 +58,8 @@ family is semi-directed.
     inc (i , ≤-refl , path→≤ (ap s (prop j i)))
 ```
 
-
 The poset $(P, \le)$ is a **directed-complete partial order**, or DCPO,
-if it has [least upper bounds] of all directed families.
-
-[least upper bounds]: Order.Diagram.Lub.html
+if it has [[least upper bounds]] of all directed families.
 
 ```agda
   record is-dcpo : Type (lsuc o ⊔ ℓ) where
@@ -79,8 +74,8 @@ if it has [least upper bounds] of all directed families.
     open ⋃ using () renaming (lub to ⋃; fam≤lub to fam≤⋃; least to ⋃-least) public
 ```
 
-Note that being a DCPO is a property of a poset, as least upper bounds
-are unique.
+Since least upper bounds are unique when they exist, being a DCPO is a
+[[property|proposition]] of a poset, and not structure on that poset.
 
 <!--
 ```agda
@@ -95,14 +90,14 @@ module _ {o ℓ} {P : Poset o ℓ} where
   is-dcpo-is-prop = Iso→is-hlevel 1 eqv $
     Π-is-hlevel′ 1 λ _ →
     Π-is-hlevel² 1 λ _ _ → Lub-is-prop P
-    where unquoteDecl eqv = declare-record-iso eqv (quote is-dcpo) 
+    where unquoteDecl eqv = declare-record-iso eqv (quote is-dcpo)
 ```
 
-# Scott-Continuous Maps
+# Scott-continuous functions
 
-Let $(P, \le)$ and $(Q, \lsq)$ be a pair of posets. 
-A monotone map $f : P \to Q$ is **Scott-continuous** if it preserves all
-directed least upper bounds.
+Let $(P, \le)$ and $(Q, \lsq)$ be a pair of posets. A monotone map $f :
+P \to Q$ is called **Scott-continuous** when it preserves all directed
+lubs.
 
 <!--
 ```agda
@@ -129,12 +124,19 @@ module _ {P Q : Poset o ℓ} where
     is-lub-is-prop Q
 ```
 
-If $(P, \le)$ is a DCPO, then any function $f : P \to Q$ that preserves
-directed least upper bounds is monotone. Start by constructing a directed
-family $s : \rm{Bool} \to P$ with $s(true) = x$ and $s(false) = y$.
-Note that $y$ is the least upper bound of this family,
-so $f(y)$ must be an upper bound of $f \circ s$ in $Q$. From this,
-we can deduce that $f(x) \lsq f(y)$.
+If $(P, \le)$ is a DCPO, then any function $f : P \to Q$ which preserves
+directed lubs is automatically a monotone map, and, consequently,
+Scott-continuous.
+
+To see this, suppose we're given $x, y : P$ with $x \le y$. The family
+$s : \rm{Bool} \to P$ that sends $\rm{true}$ to $x$ and $\rm{false}$ to
+$y$ is directed: $\rm{Bool}$ is inhabited, and $\rm{false}$ is a least
+upper bound for arbitrary values of the family. Since $f$ preserves
+lubs, we have
+
+$$
+f(x) \le (\sqcup f(s)) = f(\sqcup s) = f(y)
+$$
 
 ```agda
   opaque
@@ -148,7 +150,7 @@ we can deduce that $f(x) \lsq f(y)$.
       is-lub.fam≤lub fs-lub (lift true)
       where
 
-        s : Lift _ Bool → P.Ob 
+        s : Lift _ Bool → P.Ob
         s (lift b) = if b then x else y
 
         sx≤sfalse : ∀ b → s b P.≤ s (lift false)
@@ -169,8 +171,8 @@ we can deduce that $f(x) \lsq f(y)$.
         fs-lub = scott s s-directed y s-lub
 ```
 
-Next, a small little lemma; if $f : P \to Q$ is monotone and $s : I \to P$
-is a directed family, then $fs : I \to Q$ is also a directed family.
+Moreover, if $f : P \to Q$ is an arbitrary monotone map, and $s : I \to
+P$ is a directed family, then $fs : I \to Q$ is still a directed family.
 
 ```agda
   monotone∘directed
@@ -217,13 +219,12 @@ Scott-continuous functions are closed under composition.
 ```
 
 
-# The Category of DCPOs
-
-DCPOs form a [subcategory] of the category of posets. Furthermore, the category
-of DCPOs is [univalent], as being a DPCO is a property of a poset.
+# The category of DCPOs
 
-[subcategory]: Cat.Functor.Subcategory.html
-[univalent]: Cat.Univalent.html
+DCPOs form a [[subcategory]] of the category of posets. Furthermore,
+since being a DCPO is a property, identity of DCPOs is determined by
+identity of their underlying posets: thus, the category of DCPOs is
+[[univalent|univalent category]].
 
 ```agda
 DCPOs-subcat : ∀ (o ℓ : Level) → Subcat (Posets o ℓ) (lsuc o ⊔ ℓ) (lsuc o ⊔ ℓ)
@@ -254,30 +255,31 @@ Forget-DCPO = πᶠ _ F∘ Forget-subcat
 
 # Reasoning with DCPOs
 
-The following pair of modules re-export facts about underlying
-posets and underlying monotonic maps of DCPOs and Scott-continuous
-functions, resp. They also prove a handful of small lemmas, though
-these are not of particular interest.
+The following pair of modules re-exports facts about the underlying
+posets (resp. monotone maps) of DCPOs (resp. Scott-continuous
+functions). They also prove a plethora of small lemmas that are useful
+in formalisation but not for informal reading.
 
 <details>
 <summary>These proofs are all quite straightforward, so we omit them.
 </summary>
+
 ```agda
 module DCPO {o ℓ} (D : DCPO o ℓ) where
   poset : Poset o ℓ
   poset = D .fst
 
   set : Set o
   set = D .fst .fst
-  
+
   open Poset poset public
-  
+
   poset-on : Poset-on ℓ Ob
   poset-on = D .fst .snd
-  
+
   has-dcpo : is-dcpo poset
   has-dcpo = D .snd
-  
+
   open is-dcpo has-dcpo public
 
   ⋃-pointwise
@@ -346,9 +348,9 @@ module _ {o ℓ} {D E : DCPO o ℓ} where
 ```
 -->
 
-We also provide a couple of means of constructing Scott-continuous maps.
-First, we note that if a function is monotonic and preserves chosen
-least upper bounds, then it is Scott-continuous.
+We also provide a couple methods for constructing Scott-continuous maps.
+First, we note that if a function is monotonic and commutes with some
+chosen _assignment_ of least upper bounds, then it is Scott-continuous.
 
 ```agda
   to-scott
@@ -372,7 +374,7 @@ least upper bounds, then it is Scott-continuous.
 ```
 
 Furthermore, if $f$ preserves arbitrary least upper bounds, then it
-is monotonic, and thus Scott-continuous.
+is monotone, and thus Scott-continuous.
 
 ```agda
   to-scott-directed
@@ -383,4 +385,3 @@ is monotonic, and thus Scott-continuous.
   to-scott-directed f pres =
     sub-hom (total-hom f (dcpo+scott→monotone D.has-dcpo f pres)) pres
 ```
-

src/Order/Diagram/Fixpoint.lagda.md

@@ -40,8 +40,8 @@ record Least-fixpoint (f : Posets.Hom P P) : Type (o ⊔ ℓ) where
 open is-least-fixpoint
 ```
 
-Least fixpoints are unique, so the type of least fixpoints of $f$ is a
-proposition.
+Least fixed points are unique, so the type of least fixpoints of $f$ is
+a proposition.
 
 ```agda
 least-fixpoint-unique

src/Order/Diagram/Glb.lagda.md

@@ -200,9 +200,9 @@ le-meet a≤b l = meet-unique (le→is-meet a≤b) l
 
 ### As products
 
-The categorification of meets is _products_: put another way, if our
-category has propositional homs, then being given a product diagram is
-the same as being given a meet.
+When passing from posets to categories, meets become [[products]]:
+coming from the other direction, if a category $\cC$ has each
+$\hom(x,y)$ a [[proposition]], then products in $\cC$ are simply meets.
 
 ```agda
 open is-product
@@ -219,10 +219,10 @@ is-meet→product glb .has-is-product .π₂∘factor = prop!
 is-meet→product glb .has-is-product .unique _ _ _ = prop!
 ```
 
-## Tops
+## Top elements
 
-A **top** in a partial order $(P, \le)$ is an element $\top : P$ that
-is larger than any other element in $P$. This is the same as being
+A **top element** in a partial order $(P, \le)$ is an element $\top : P$
+that is larger than any other element in $P$. This is the same as being
 a greatest lower bound for the empty family $\bot \to P$.
 
 ```agda
@@ -281,12 +281,10 @@ Top≃Glb = prop-ext! _ Glb→Top .snd
 
 ### As Terminal Objects
 
-Bottoms are the decategorifcation of [terminal objects]; we don't need to
+Bottoms are the decategorifcation of [[terminal objects]]; we don't need to
 require the uniqueness of the universal morphism, as we've replaced our
 hom-sets with hom-props!
 
-[terminal objects]: Cat.Diagram.Terminal.html
-
 ```agda
 is-top→terminal : ∀ {x} → is-top x → is-terminal (poset→category P) x
 is-top→terminal is-top x .centre = is-top x

src/Order/Diagram/Lub.lagda.md

@@ -23,7 +23,7 @@ open Order.Reasoning P
 ```
 -->
 
-# Least upper bounds
+# Least upper bounds {defines="least-upper-bound"}
 
 A **lub** $u$ (short for **least upper bound**) for a family of
 elements $(a_i)_{i : I}$ is, as the name implies, a least elemnet among
@@ -135,7 +135,6 @@ fam-bound→is-lub i ge .fam≤lub = ge
 fam-bound→is-lub i ge .least y le = le i
 ```
 
-
 If $x$ is the least upper bound of a constant family, then
 $x$ must be equal to every member of the family.
 
@@ -182,7 +181,6 @@ const-inhabited-fam→lub {I = I} {F = F} is-const =
       const-inhabited-fam→is-lub (λ j → is-const j i) (inc i)
 ```
 
-
 ## Joins
 
 In the binary case, a least upper bound is called a **join**. A short
@@ -281,9 +279,9 @@ gt-join a≤b l = join-unique (gt→is-join a≤b) l
 
 ### As coproducts
 
-Joins are the “thinning” of coproducts; Put another way, when we allow a
-_set_ of relators rather than insisting on a propositional relation, the
-concept of join needs to be refined to that of coproduct.
+Joins are the “thinning” of [[coproducts]]; Put another way, when we
+allow a _set_ of relators, rather than insisting on a propositional
+relation, the concept of join needs to be refined to that of coproduct.
 
 ```agda
 open is-coproduct
@@ -300,14 +298,14 @@ is-join→coproduct lub .has-is-coproduct .in₁∘factor = prop!
 is-join→coproduct lub .has-is-coproduct .unique _ _ _ = prop!
 ```
 
-## Bottoms
+## Bottom elements
 
-A **bottom** in a partial order $(P, \le)$ is an element $\bot : P$
-that is smaller than any other element of $P$. This is the same as
+A **bottom element** in a partial order $(P, \le)$ is an element $\bot :
+P$ that is smaller than any other element of $P$. This is the same as
 being a least upper upper bound for the empty family $\bot \to P$.
 
 ```agda
-is-bottom : Ob → Type _ 
+is-bottom : Ob → Type _
 is-bottom bot = ∀ x → bot ≤ x
 
 record Bottom : Type (o ⊔ ℓ) where
@@ -366,12 +364,10 @@ Bottom≃Lub = prop-ext! _ Lub→Bottom .snd
 
 ### As initial objects
 
-Bottoms are the decategorifcation of [initial objects]; we don't need to
+Bottoms are the decategorifcation of [[initial objects]]; we don't need to
 require the uniqueness of the universal morphism, as we've replaced our
 hom-sets with hom-props!
 
-[initial objects]: Cat.Diagram.Initial.html
-
 ```agda
 is-bottom→initial : ∀ {x} → is-bottom x → is-initial (poset→category P) x
 is-bottom→initial is-bot x .centre = is-bot x