diff --git a/src/1Lab/Resizing.lagda.md b/src/1Lab/Resizing.lagda.md
index c2a60a09a..85c406f40 100644
--- a/src/1Lab/Resizing.lagda.md
+++ b/src/1Lab/Resizing.lagda.md
@@ -4,6 +4,7 @@ open import 1Lab.Path.IdentitySystem
open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
+open import 1Lab.HIT.Truncation
open import 1Lab.Reflection using (arg ; typeError)
open import 1Lab.Univalence
open import 1Lab.HLevel
@@ -144,6 +145,18 @@ elΩ T .is-tr = squash
□-elim pprop go (squash x y i) =
is-prop→pathp (λ i → pprop (squash x y i)) (□-elim pprop go x) (□-elim pprop go y) i
+□-rec-set
+ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+ → (f : A → B)
+ → (∀ x y → f x ≡ f y)
+ → is-set B
+ → □ A → B
+□-rec-set f f-const B-set a =
+ fst $ □-elim
+ (λ _ → is-constant→image-is-prop B-set f f-const)
+ (λ a → f a , inc (a , refl))
+ a
+
□-idempotent : ∀ {ℓ} {A : Type ℓ} → is-prop A → □ A ≃ A
□-idempotent aprop = prop-ext squash aprop (out! {pa = aprop}) inc
diff --git a/src/1Lab/Type/Sigma.lagda.md b/src/1Lab/Type/Sigma.lagda.md
index f493a271a..d33084801 100644
--- a/src/1Lab/Type/Sigma.lagda.md
+++ b/src/1Lab/Type/Sigma.lagda.md
@@ -15,7 +15,7 @@ module 1Lab.Type.Sigma where
```
private variable
ℓ ℓ₁ : Level
- A A' : Type ℓ
+ A A' X X' : Type ℓ
B P Q : A → Type ℓ
```
-->
@@ -252,10 +252,15 @@ If `B` is a family of contractible types, then `Σ B ≃ A`:
the-iso .snd .is-iso.linv (a , b) i = a , bcontr a .paths b i
```
+
-# 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
diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md
index 2d5e88c67..d01cbbd97 100644
--- a/src/Cat/Diagram/Initial.lagda.md
+++ b/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:
diff --git a/src/Cat/Functor/Subcategory.lagda.md b/src/Cat/Functor/Subcategory.lagda.md
new file mode 100644
index 000000000..5a790654d
--- /dev/null
+++ b/src/Cat/Functor/Subcategory.lagda.md
@@ -0,0 +1,263 @@
+
+
+```agda
+module Cat.Functor.Subcategory where
+```
+
+# 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$
+on morphisms between objects within $P$ that is closed under identities
+and composites.
+
+[predicate]: 1Lab.HLevel.html#is-prop
+
+To start, we package up all the data required to define a subcategory up
+into a record. Note that we omit the requirement that the predicate on
+objects is a proposition; this tends to be ill-behaved unless the $\cC$
+is univalent.
+
+
+
+```agda
+ record Subcat (o' ℓ' : Level) : Type (o ⊔ ℓ ⊔ lsuc o' ⊔ lsuc ℓ') where
+ no-eta-equality
+ field
+ is-ob : Ob → Type o'
+ is-hom : ∀ {x y} (f : Hom x y) → is-ob x → is-ob y → Type ℓ'
+ is-hom-prop
+ : ∀ {x y} (f : Hom x y) (px : is-ob x) (py : is-ob y)
+ → is-prop (is-hom f px py)
+ is-hom-id : ∀ {x} → (px : is-ob x) → is-hom id px px
+ is-hom-∘
+ : ∀ {x y z} {f : Hom y z} {g : Hom x y}
+ → {px : is-ob x} {py : is-ob y} {pz : is-ob z}
+ → is-hom f py pz → is-hom g px py
+ → is-hom (f ∘ g) px pz
+```
+
+Morphisms of wide subcategories are defined as morphisms in $\cC$ where
+$Q$ holds.
+
+```agda
+module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} (subcat : Subcat C o' ℓ') where
+ open Cat.Reasoning C
+ open Subcat subcat
+
+ record Subcat-hom (x y : Σ[ ob ∈ Ob ] (is-ob ob)) : Type (ℓ ⊔ ℓ') where
+ no-eta-equality
+ constructor sub-hom
+ field
+ hom : Hom (x .fst) (y .fst)
+ witness : subcat .is-hom hom (x .snd) (y .snd)
+
+open Subcat-hom
+```
+
+
+
+We can then use this data to construct a category.
+
+
+
+```agda
+ Subcategory : Precategory (o ⊔ o') (ℓ ⊔ ℓ')
+ Subcategory .Precategory.Ob = Σ[ ob ∈ Ob ] is-ob ob
+ Subcategory .Precategory.Hom = Subcat-hom subcat
+ Subcategory .Precategory.Hom-set _ _ = Subcat-hom-is-set
+ Subcategory .Precategory.id .hom = id
+ Subcategory .Precategory.id .witness = is-hom-id _
+ Subcategory .Precategory._∘_ f g .hom = f .hom ∘ g .hom
+ Subcategory .Precategory._∘_ f g .witness = is-hom-∘ (f .witness) (g .witness)
+ Subcategory .Precategory.idr f = Subcat-hom-path (idr (f .hom))
+ Subcategory .Precategory.idl f = Subcat-hom-path (idl (f .hom))
+ Subcategory .Precategory.assoc f g h = Subcat-hom-path (assoc (f .hom) (g .hom) (h .hom))
+```
+
+## From pseudomonic functors
+
+There is another way of representing subcategories: By giving a
+[faithful functor] $F : \cD \epi \cC$.
+
+[faithful functor]: Cat.Functor.Properties.html
+
+
+
+We construct a subcategory from a faithful functor $F$ by restricting to
+the objects in the [essential image] of $F$, and restricting the morphisms
+to those that lie in the image of $F$.
+
+[essential image]: Cat.Functor.Properties.html#essential-fibres
+
+```agda
+ Faithful-subcat : Subcat D (o ⊔ ℓ') (ℓ ⊔ ℓ')
+ Faithful-subcat .Subcat.is-ob x = Essential-fibre F x
+ Faithful-subcat .Subcat.is-hom f (y , y-es) (z , z-es) =
+ Σ[ g ∈ C.Hom y z ] (D.to z-es D.∘ F₁ g D.∘ D.from y-es ≡ f)
+ Faithful-subcat .Subcat.is-hom-prop f (y , y-es) (z , z-es) (g , p) (h , q) =
+ Σ-prop-path (λ _ → D.Hom-set _ _ _ _) $
+ faithful $
+ D.iso→epic (y-es D.Iso⁻¹) _ _ $
+ D.iso→monic z-es _ _ $
+ p ∙ sym q
+ Faithful-subcat .Subcat.is-hom-id (y , y-es) =
+ C.id , ap₂ D._∘_ refl (D.eliml F-id) ∙ D.invl y-es
+ Faithful-subcat .Subcat.is-hom-∘
+ {f = f} {g = g} {x , x-es} {y , y-es} {z , z-es} (h , p) (i , q) =
+ (h C.∘ i) ,
+ D.push-inner (F-∘ h i)
+ ·· D.insert-inner (D.invr y-es)
+ ·· ap₂ D._∘_ (sym (D.assoc _ _ _) ∙ p) q
+```
+
+There is an equivalence between canonical subcategory associated
+with $F$ and $C$.
+
+```
+ Faithful-subcat-domain : Functor (Subcategory Faithful-subcat) C
+ Faithful-subcat-domain .Functor.F₀ (x , x-es) = x-es .fst
+ Faithful-subcat-domain .Functor.F₁ f = f .witness .fst
+ Faithful-subcat-domain .Functor.F-id = refl
+ Faithful-subcat-domain .Functor.F-∘ _ _ = refl
+
+ Faithful-subcat-domain-is-ff : is-fully-faithful Faithful-subcat-domain
+ Faithful-subcat-domain-is-ff {x = x , x' , x-es} {y = y , y' , y-es} =
+ is-iso→is-equiv $ iso
+ (λ f → sub-hom (D.to y-es D.∘ F₁ f D.∘ D.from x-es) (f , refl))
+ (λ _ → refl)
+ (λ f → Subcat-hom-path (f .witness .snd))
+
+ Faithful-subcat-domain-is-split-eso : is-split-eso Faithful-subcat-domain
+ Faithful-subcat-domain-is-split-eso x =
+ (F₀ x , x , D.id-iso) , C.id-iso
+```
+
+There is a faithful functor from a subcategory on $\cC$ to $\cC$.
+
+
+
+```agda
+ Forget-subcat : Functor (Subcategory subcat) C
+ Forget-subcat .Functor.F₀ (x , _) = x
+ Forget-subcat .Functor.F₁ f = f .hom
+ Forget-subcat .Functor.F-id = refl
+ Forget-subcat .Functor.F-∘ _ _ = refl
+
+ is-faithful-Forget-subcat : is-faithful Forget-subcat
+ is-faithful-Forget-subcat = Subcat-hom-path
+```
+
+Furthermore, if the subcategory contains all of the isomorphisms of $\cC$, then
+the forgetful functor is pseudomonic.
+
+```agda
+ is-pseudomonic-Forget-subcat
+ : (∀ {x y} {f : Hom x y} {px : is-ob x} {py : is-ob y}
+ → is-invertible f → subcat .is-hom f px py)
+ → is-pseudomonic Forget-subcat
+ is-pseudomonic-Forget-subcat invert .is-pseudomonic.faithful =
+ is-faithful-Forget-subcat
+ is-pseudomonic-Forget-subcat invert .is-pseudomonic.isos-full f =
+ pure $
+ Sub.make-iso
+ (sub-hom (f .to) (invert (iso→invertible f)))
+ (sub-hom (f .from) (invert (iso→invertible (f Iso⁻¹))))
+ (Subcat-hom-path (f .invl))
+ (Subcat-hom-path (f .invr))
+ , ≅-path refl
+```
+
+## Univalent Subcategories
+
+Let $\cC$ be a [univalent] category. A subcategory of $\cC$ is univalent
+when the predicate on objects is a proposition.
+
+[univalent]: Cat.Univalent.html
+
+```agda
+ subcat-iso→iso : ∀ {x y : Σ[ x ∈ Ob ] is-ob x} → x Sub.≅ y → x .fst ≅ y .fst
+ subcat-iso→iso f =
+ make-iso (Sub.to f .hom) (Sub.from f .hom)
+ (ap hom (Sub.invl f)) (ap hom (Sub.invr f))
+
+ subcat-is-category
+ : is-category C
+ → (∀ x → is-prop (is-ob x))
+ → is-category (Subcategory subcat)
+ subcat-is-category cat ob-prop .to-path {a , pa} {b , pb} f =
+ Σ-prop-path ob-prop (cat .to-path (subcat-iso→iso f))
+ subcat-is-category cat ob-prop .to-path-over p =
+ Sub.≅-pathp refl _ $
+ Subcat-hom-pathp refl _ $
+ apd (λ _ → to) (cat .to-path-over (subcat-iso→iso p))
+```
diff --git a/src/Data/Maybe/Base.lagda.md b/src/Data/Maybe/Base.lagda.md
index 53af4220b..1e4bfd6f8 100644
--- a/src/Data/Maybe/Base.lagda.md
+++ b/src/Data/Maybe/Base.lagda.md
@@ -37,6 +37,10 @@ map f nothing = nothing
extend : Maybe A → (A → Maybe B) → Maybe B
extend (just x) k = k x
extend nothing k = nothing
+
+Maybe-rec : (A → B) → B → Maybe A → B
+Maybe-rec f b (just x) = f x
+Maybe-rec f b nothing = b
```
+
We set up the category of posets using our [machinery for displaying]
[univalent categories] over the category of sets. A map between posets
is called a **monotone map**: it's the decategorification of a functor.
@@ -109,12 +133,26 @@ composites, since our "homs" are propositions!
[univalent categories]: Cat.Univalent.html
```agda
+is-monotone
+ : ∀ {o o' ℓ ℓ'} {A : Type o} {B : Type o'}
+ → (f : A → B) → Poset-on ℓ A → Poset-on ℓ' B → Type _
+is-monotone f P Q = ∀ x y → x P.≤ y → f x Q.≤ f y
+ where
+ module P = Poset-on P
+ module Q = Poset-on Q
+
+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-hlevel³ 1 λ _ _ _ → Poset-on.≤-thin Q
+
Poset-structure : ∀ ℓ ℓ′ → Thin-structure {ℓ = ℓ} (ℓ ⊔ ℓ′) (Poset-on ℓ′)
-∣ Poset-structure ℓ ℓ′ .is-hom f P Q ∣ =
- ∀ x y → Poset-on._≤_ P x y → Poset-on._≤_ Q (f x) (f y)
+∣ Poset-structure ℓ ℓ′ .is-hom f P Q ∣ = is-monotone f P Q
Poset-structure ℓ ℓ′ .is-hom f P Q .is-tr =
- Π-is-hlevel³ 1 λ _ _ _ → Poset-on.≤-thin Q
+ is-monotone-is-prop f P Q
Poset-structure ℓ ℓ′ .id-is-hom x y α = α
Poset-structure ℓ ℓ′ .∘-is-hom f g α β x y γ = α (g x) (g y) (β x y γ)
@@ -128,19 +166,11 @@ Then, since equality of poset structures is controlled by equality of
the relations, we have $s = t$!
```agda
-Poset-structure ℓ ℓ′ .id-hom-unique {s = s} {t = t} α β = q where
- module s = Poset-on s
- module t = Poset-on t
- open is-iso
-
- p : s._≤_ ≡ t._≤_
- p i x y = ua (prop-ext s.≤-thin t.≤-thin (α x y) (β x y)) i
-
- q : s ≡ t
- q i .Poset-on._≤_ = p i
- q i .Poset-on.has-is-poset = is-prop→pathp
- (λ i → is-partial-order-is-prop (p i))
- s.has-is-poset t.has-is-poset i
+Poset-structure ℓ ℓ′ .id-hom-unique {s = s} {t = t} α β =
+ Poset-on-path λ x y → ua (prop-ext s.≤-thin t.≤-thin (α x y) (β x y))
+ where
+ module s = Poset-on s
+ module t = Poset-on t
```
+
+```agda
+module Order.DCPO where
+```
+
+
+
+# Directed-Complete Partial Orders
+
+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.
+
+```agda
+module _ {o ℓ} (P : Poset o ℓ) where
+ open Poset P
+
+ is-semidirected-family : ∀ {Ix : Type o} → (Ix → Ob) → Type _
+ is-semidirected-family {Ix = Ix} f = ∀ i j → ∃[ k ∈ Ix ] (f i ≤ f k × f j ≤ f k)
+
+ record is-directed-family {Ix : Type o} (f : Ix → Ob) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ elt : ∥ Ix ∥
+ semidirected : is-semidirected-family f
+```
+
+Note that any family whose indexing type is a proposition is
+automatically semi-directed:
+
+```agda
+ prop-indexed→semidirected
+ : ∀ {Ix : Type o} → (s : Ix → Ob) → is-prop Ix
+ → is-semidirected-family s
+ prop-indexed→semidirected s prop i j =
+ 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.
+
+```agda
+ record is-dcpo : Type (lsuc o ⊔ ℓ) where
+ no-eta-equality
+ field
+ directed-lubs
+ : ∀ {Ix : Type o} (f : Ix → Ob) → is-directed-family f → Lub P f
+
+ module ⋃ {Ix : Type o} (f : Ix → Ob) (dir : is-directed-family f) =
+ Lub (directed-lubs f dir)
+
+ open ⋃ using () renaming (lub to ⋃; fam≤lub to fam≤⋃; least to ⋃-least) public
+```
+
+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
+ is-dcpo-is-prop : is-prop (is-dcpo P)
+ 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)
+```
+
+# Scott-continuous functions
+
+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
+ is-scott-continuous : (f : Posets.Hom P Q) → Type _
+ is-scott-continuous f =
+ ∀ {Ix} (s : Ix → P.Ob) (fam : is-directed-family P s)
+ → ∀ x → is-lub P s x → is-lub Q (f .hom ⊙ s) (f .hom x)
+
+ is-scott-continuous-is-prop
+ : ∀ (f : Posets.Hom P Q) → is-prop (is-scott-continuous f)
+ is-scott-continuous-is-prop _ =
+ Π-is-hlevel′ 1 λ _ → Π-is-hlevel³ 1 λ _ _ _ → Π-is-hlevel 1 λ _ →
+ is-lub-is-prop Q
+```
+
+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
+ dcpo+scott→monotone
+ : is-dcpo P
+ → (f : P.Ob → Q.Ob)
+ → (∀ {Ix} (s : Ix → Poset.Ob P) (fam : is-directed-family P s)
+ → ∀ x → is-lub P s x → is-lub Q (f ⊙ s) (f x))
+ → is-monotone f (P .snd) (Q .snd)
+ dcpo+scott→monotone is-dcpo f scott x y p =
+ is-lub.fam≤lub fs-lub (lift true)
+ where
+
+ s : Lift _ Bool → P.Ob
+ s (lift b) = if b then x else y
+
+ sx≤sfalse : ∀ b → s b P.≤ s (lift false)
+ sx≤sfalse (lift true) = p
+ sx≤sfalse (lift false) = P.≤-refl
+
+ s-directed : is-directed-family P s
+ s-directed .elt =
+ inc (lift true)
+ s-directed .semidirected i j =
+ inc (lift false , sx≤sfalse _ , sx≤sfalse _)
+
+ s-lub : is-lub P s y
+ s-lub .is-lub.fam≤lub = sx≤sfalse
+ s-lub .is-lub.least z lt = lt (lift false)
+
+ fs-lub : is-lub Q (f ⊙ s) (f y)
+ fs-lub = scott s s-directed y s-lub
+```
+
+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
+ : ∀ {Ix : Type o}
+ → {s : Ix → P.Ob}
+ → (f : Posets.Hom P Q)
+ → is-directed-family P s
+ → is-directed-family Q (f .hom ⊙ s)
+ monotone∘directed f dir .elt = dir .elt
+ monotone∘directed f dir .is-directed-family.semidirected i j =
+ ∥-∥-map (Σ-map₂ (×-map (f .preserves _ _) (f .preserves _ _)))
+ (dir .semidirected i j)
+```
+
+
+
+The identity function is Scott-continuous.
+
+```agda
+ scott-id
+ : ∀ {P : Poset o ℓ}
+ → is-scott-continuous (Posets.id {x = P})
+ scott-id s fam x lub = lub
+```
+
+Scott-continuous functions are closed under composition.
+
+```agda
+ scott-∘
+ : ∀ {P Q R : Poset o ℓ}
+ → (f : Posets.Hom Q R) (g : Posets.Hom P Q)
+ → is-scott-continuous f → is-scott-continuous g
+ → is-scott-continuous (f Posets.∘ g)
+ scott-∘ f g f-scott g-scott s dir x lub =
+ f-scott (g .hom ⊙ s)
+ (monotone∘directed g dir)
+ (g .hom x)
+ (g-scott s dir x lub)
+```
+
+
+# The category of DCPOs
+
+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 ⊔ ℓ)
+DCPOs-subcat o ℓ .Subcat.is-ob = is-dcpo
+DCPOs-subcat o ℓ .Subcat.is-hom f _ _ = is-scott-continuous f
+DCPOs-subcat o ℓ .Subcat.is-hom-prop f _ _ = is-scott-continuous-is-prop f
+DCPOs-subcat o ℓ .Subcat.is-hom-id _ = scott-id
+DCPOs-subcat o ℓ .Subcat.is-hom-∘ {f = f} {g = g} = scott-∘ f g
+
+DCPOs : ∀ (o ℓ : Level) → Precategory (lsuc (o ⊔ ℓ)) (lsuc o ⊔ ℓ)
+DCPOs o ℓ = Subcategory (DCPOs-subcat o ℓ)
+
+DCPOs-is-category : ∀ {o ℓ} → is-category (DCPOs o ℓ)
+DCPOs-is-category = subcat-is-category Posets-is-category (λ _ → is-dcpo-is-prop)
+```
+
+
+
+# Reasoning with DCPOs
+
+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.
+
+
+These proofs are all quite straightforward, so we omit them.
+
+
+```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
+ : ∀ {Ix} {s s' : Ix → Ob}
+ → {fam : is-directed-family poset s} {fam' : is-directed-family poset s'}
+ → (∀ ix → s ix ≤ s' ix)
+ → ⋃ s fam ≤ ⋃ s' fam'
+ ⋃-pointwise p = ⋃.least _ _ (⋃ _ _) λ ix →
+ ≤-trans (p ix) (⋃.fam≤lub _ _ ix)
+
+module Scott {o ℓ} {D E : DCPO o ℓ} (f : DCPOs.Hom D E) where
+ private
+ module D = DCPO D
+ module E = DCPO E
+
+ mono : Posets.Hom D.poset E.poset
+ mono = Subcat-hom.hom f
+
+ hom : D.Ob → E.Ob
+ hom x = Total-hom.hom mono x
+
+ monotone : ∀ x y → x D.≤ y → hom x E.≤ hom y
+ monotone = Total-hom.preserves mono
+
+ opaque
+ pres-directed-lub
+ : ∀ {Ix} (s : Ix → D.Ob) → is-directed-family D.poset s
+ → ∀ x → is-lub D.poset s x → is-lub E.poset (hom ⊙ s) (hom x)
+ pres-directed-lub = Subcat-hom.witness f
+
+ directed
+ : ∀ {Ix} {s : Ix → D.Ob} → is-directed-family D.poset s
+ → is-directed-family E.poset (hom ⊙ s)
+ directed dir = monotone∘directed (Subcat-hom.hom f) dir
+
+ pres-⋃
+ : ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
+ → hom (D.⋃ s dir) ≡ E.⋃ (hom ⊙ s) (directed dir)
+ pres-⋃ s dir =
+ E.≤-antisym
+ (is-lub.least (pres-directed-lub s dir (D.⋃ s dir) (D.⋃.has-lub s dir))
+ (E.⋃ (hom ⊙ s) (directed dir))
+ (E.⋃.fam≤lub (hom ⊙ s) (directed dir)))
+ (E.⋃.least (hom ⊙ s) (directed dir) (hom (D.⋃ s dir)) λ i →
+ monotone (s i) (D.⋃ s dir) (D.⋃.fam≤lub s dir i))
+```
+
+
+
+
+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
+ : (f : D.Ob → E.Ob)
+ → (∀ x y → x D.≤ y → f x E.≤ f y)
+ → (∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
+ → is-lub E.poset (f ⊙ s) (f (D.⋃ s dir)))
+ → DCPOs.Hom D E
+ to-scott f monotone pres-⋃ =
+ sub-hom (total-hom f monotone) pres-lub where
+ pres-lub
+ : ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
+ → ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x)
+ pres-lub s dir x x-lub .is-lub.fam≤lub i =
+ monotone _ _ (is-lub.fam≤lub x-lub i)
+ pres-lub s dir x x-lub .is-lub.least y le =
+ f x E.≤⟨ monotone _ _ (is-lub.least x-lub _ (D.⋃.fam≤lub s dir)) ⟩
+ f (D.⋃ s dir) E.=⟨ lub-unique E.poset (pres-⋃ s dir) (E.⋃.has-lub (f ⊙ s) (monotone∘directed (total-hom f monotone) dir)) ⟩
+ E.⋃ (f ⊙ s) _ E.≤⟨ E.⋃.least _ _ y le ⟩
+ y E.≤∎
+```
+
+Furthermore, if $f$ preserves arbitrary least upper bounds, then it
+is monotone, and thus Scott-continuous.
+
+```agda
+ to-scott-directed
+ : (f : D.Ob → E.Ob)
+ → (∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
+ → ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x))
+ → DCPOs.Hom D E
+ to-scott-directed f pres =
+ sub-hom (total-hom f (dcpo+scott→monotone D.has-dcpo f pres)) pres
+```
diff --git a/src/Order/DCPO/Free.lagda.md b/src/Order/DCPO/Free.lagda.md
new file mode 100644
index 000000000..f2474cc81
--- /dev/null
+++ b/src/Order/DCPO/Free.lagda.md
@@ -0,0 +1,577 @@
+
+
+```agda
+module Order.DCPO.Free where
+```
+
+
+
+# Free DCPOs
+
+The [discrete poset] on a set $A$ is a DCPO. To see this, note that
+every semi-directed family $f : I \to A$ in a discrete poset is constant.
+Furthermore, $f$ is directed, so it is merely inhabited.
+
+[discrete poset]: Order.Instances.Discrete.html
+
+```agda
+Disc-is-dcpo : ∀ {ℓ} {A : Set ℓ} → is-dcpo (Disc A)
+Disc-is-dcpo {A = A} .is-dcpo.directed-lubs {Ix = Ix} f dir =
+ const-inhabited-fam→lub (Disc A) disc-fam-const (dir .elt)
+ where
+ disc-fam-const : ∀ i j → f i ≡ f j
+ disc-fam-const i j =
+ ∥-∥-rec! (λ (k , p , q) → p ∙ sym q)
+ (dir .semidirected i j)
+
+Disc-dcpo : (A : Set ℓ) → DCPO ℓ ℓ
+Disc-dcpo A = Disc A , Disc-is-dcpo
+```
+
+This extends to a functor from $\Sets$ to the category of DCPOs.
+
+```agda
+Free-DCPO : ∀ {ℓ} → Functor (Sets ℓ) (DCPOs ℓ ℓ)
+Free-DCPO .F₀ = Disc-dcpo
+Free-DCPO .F₁ f =
+ to-scott-directed f λ s dir x x-lub →
+ const-inhabited-fam→is-lub (Disc _)
+ (λ ix → ap f (disc-is-lub→const x-lub ix))
+ (dir .elt)
+Free-DCPO .F-id = scott-path (λ _ → refl)
+Free-DCPO .F-∘ _ _ = scott-path (λ _ → refl)
+```
+
+Furthermore, this functor is left adjoint to the forgetful functor
+to $\Sets$.
+
+```agda
+Free-DCPO⊣Forget-DCPO : ∀ {ℓ} → Free-DCPO {ℓ} ⊣ Forget-DCPO
+Free-DCPO⊣Forget-DCPO .unit .η _ x = x
+Free-DCPO⊣Forget-DCPO .unit .is-natural _ _ _ = refl
+Free-DCPO⊣Forget-DCPO .counit .η D =
+ to-scott-directed (λ x → x) λ s dir x x-lub → λ where
+ .is-lub.fam≤lub i → path→≤ (disc-is-lub→const x-lub i)
+ .is-lub.least y le →
+ ∥-∥-rec ≤-thin
+ (λ i →
+ x =˘⟨ disc-is-lub→const x-lub i ⟩
+ s i ≤⟨ le i ⟩
+ y ≤∎)
+ (dir .elt)
+ where open DCPO D
+Free-DCPO⊣Forget-DCPO .counit .is-natural x y f =
+ scott-path (λ _ → refl)
+Free-DCPO⊣Forget-DCPO .zig = scott-path (λ _ → refl)
+Free-DCPO⊣Forget-DCPO .zag = refl
+```
+
+# Free Pointed DCPOs
+
+We construct the free [pointed DCPO] on a set $A$; IE a pointed
+DCPO $A_{\bot}$ with the property that for all pointed DCPOs $B$,
+functions $A \to B$ correspond with strictly Scott-continuous maps
+$A_{\bot} \to B$.
+
+[pointed DCPO]: Order.DCPO.Pointed.html
+
+To start, we define a type of **partial elements** of $A$ as a pair
+of a proposition $\varphi$, along with a function $\varphi \to A$.
+
+```agda
+record Part {ℓ} (A : Type ℓ) : Type ℓ where
+ no-eta-equality
+ field
+ def : Ω
+ elt : ∣ def ∣ → A
+
+open Part
+```
+
+We say that a partial element $x$ is **defined** when the associated
+proposition is true, and write $x \downarrow y$ to denote that $x$
+is defined, and it's value is $y$.
+
+```agda
+is-defined : Part A → Type
+is-defined x? = ∣ x? .def ∣
+
+_↓_ : Part A → A → Type _
+x ↓ y = Σ[ d ∈ is-defined x ] (x .elt d ≡ y)
+```
+
+
+Paths between partial elements are given by bi-implications of their
+propositions, along with a path between their values, assuming that both
+elements are defined.
+
+```agda
+Part-pathp
+ : {x : Part A} {y : Part B}
+ → (p : A ≡ B)
+ → (q : x .def ≡ y .def)
+ → PathP (λ i → ∣ q i ∣ → p i) (x .elt) (y .elt)
+ → PathP (λ i → Part (p i)) x y
+Part-pathp {x = x} {y = y} p q r i .def = q i
+Part-pathp {x = x} {y = y} p q r i .elt = r i
+
+part-ext
+ : ∀ {x y : Part A}
+ → (to : is-defined x → is-defined y)
+ → (from : is-defined y → is-defined x)
+ → (∀ (x-def : is-defined x) (y-def : is-defined y) → x .elt x-def ≡ y .elt y-def)
+ → x ≡ y
+part-ext to from p =
+ Part-pathp refl
+ (Ω-ua to from)
+ (funext-dep (λ _ → p _ _))
+```
+
+
+
+We say that a partial element $y$ **refines** $x$ if $y$ is defined
+whenever $x$ is, and their values are equal whenever $x$ is defined.
+
+```
+record _⊑_ {ℓ} {A : Type ℓ} (x y : Part A) : Type ℓ where
+ no-eta-equality
+ field
+ implies : is-defined x → is-defined y
+ refines : (x-def : is-defined x) → (y .elt (implies x-def) ≡ x .elt x-def)
+
+open _⊑_
+```
+
+
+
+This ordering is reflexive, transitive, and anti-symmetric, so the type
+of partial elements forms a poset whenever $A$ is a set.
+
+```
+⊑-refl : ∀ {x : Part A} → x ⊑ x
+⊑-refl .implies x-def = x-def
+⊑-refl .refines _ = refl
+
+⊑-thin : ∀ {x y : Part A} → is-set A → is-prop (x ⊑ y)
+⊑-thin A-set = ⊑-is-hlevel 0 A-set
+
+⊑-trans : ∀ {x y z : Part A} → x ⊑ y → y ⊑ z → x ⊑ z
+⊑-trans p q .implies x-def = q .implies (p .implies x-def)
+⊑-trans p q .refines x-def = q .refines (p .implies x-def) ∙ p .refines x-def
+
+⊑-antisym : ∀ {x y : Part A} → x ⊑ y → y ⊑ x → x ≡ y
+⊑-antisym {x = x} {y = y} p q = part-ext (p .implies) (q .implies) λ x-def y-def →
+ ap (x .elt) (x .def .is-tr _ _) ∙ q .refines y-def
+
+Parts : (A : Set ℓ) → Poset ℓ ℓ
+Parts A = to-poset (Part ∣ A ∣) mk-parts where
+ mk-parts : make-poset _ (Part ∣ A ∣)
+ mk-parts .make-poset.rel = _⊑_
+ mk-parts .make-poset.id = ⊑-refl
+ mk-parts .make-poset.thin = ⊑-thin (A .is-tr)
+ mk-parts .make-poset.trans = ⊑-trans
+ mk-parts .make-poset.antisym = ⊑-antisym
+```
+
+
+Furthermore, the poset of partial elements has [least upper bounds] of all
+[semidirected families].
+
+[least upper bounds]: Order.Diagram.Lub.html
+[semidirected families]: Order.DCPO.html
+
+```agda
+⊑-lub
+ : ∀ {Ix : Type ℓ}
+ → is-set A
+ → (s : Ix → Part A)
+ → (∀ i j → ∃[ k ∈ Ix ] (s i ⊑ s k × s j ⊑ s k))
+ → Part A
+```
+
+Let $s : I \to A$ be a semidirected family, IE: for every $i, j : I$, there
+merely exists some $k : I$ such that $s(i) \lsq s(k)$ and $s(j) \lsq s(k)$.
+The least upper bound of $s$ shall be defined whenever there merely exists
+some $i : I$ such that $s(i)$ is defined.
+
+```agda
+⊑-lub {Ix = Ix} set s dir .def = elΩ (Σ[ i ∈ Ix ] is-defined (s i))
+```
+
+Next, we need to construct an element of $A$ under the assumption that
+there exists such an $i$. The obvious move is to use the value of $s(i)$,
+though this is hindered by the fact that there only _merely_ exists an
+$i$. However, as $A$ is a set, it suffices to show that the map
+$(i , \varphi_i) \mapsto s(i)(\varphi_i)$ is constant.
+
+```
+⊑-lub {Ix = Ix} set s dir .elt =
+ □-rec-set
+ (λ pi → s (fst pi) .elt (snd pi))
+ (λ p q i →
+ is-const p q i .elt $
+ is-prop→pathp (λ i → (is-const p q i) .def .is-tr) (p .snd) (q .snd) i)
+ set
+ where abstract
+```
+
+To see this, we use the fact that $s$ is semidirected to obtain a $k$
+such that $s(i), s(j) \lsq s(k)$. We can then use the fact that $s(k)$
+refines both $s(i)$ and $s(j)$ to obtain the desired path.
+
+```agda
+ is-const
+ : ∀ (p q : Σ[ i ∈ Ix ] is-defined (s i))
+ → s (p .fst) ≡ s (q .fst)
+ is-const (i , si) (j , sj) = ∥-∥-proj {ap = Part-is-set set _ _} $ do
+ (k , p , q) ← dir i j
+ pure $ part-ext (λ _ → sj) (λ _ → si) λ si sj →
+ s i .elt si ≡˘⟨ p .refines si ⟩
+ s k .elt (p .implies si) ≡⟨ ap (s k .elt) (s k .def .is-tr _ _) ⟩
+ s k .elt (q .implies sj) ≡⟨ q .refines sj ⟩
+ s j .elt sj ∎
+```
+
+Next, we show that this actually defines a least upper bound. This is
+pretty straightforward, so we do not dwell on it too deeply.
+
+```agda
+⊑-lub-le
+ : ∀ {Ix : Type ℓ}
+ → {set : is-set A}
+ → {s : Ix → Part A}
+ → {dir : ∀ i j → ∃[ k ∈ Ix ] (s i ⊑ s k × s j ⊑ s k)}
+ → ∀ i → s i ⊑ ⊑-lub set s dir
+⊑-lub-le i .implies si = inc (i , si)
+⊑-lub-le i .refines si = refl
+
+⊑-lub-least
+ : ∀ {Ix : Type ℓ}
+ → {set : is-set A}
+ → {s : Ix → Part A}
+ → {dir : ∀ i j → ∃[ k ∈ Ix ] (s i ⊑ s k × s j ⊑ s k)}
+ → ∀ x → (∀ i → s i ⊑ x) → ⊑-lub set s dir ⊑ x
+⊑-lub-least {Ix = Ix} {set = set} {s = s} {dir = dir} x le .implies =
+ □-rec! λ si → le (si .fst) .implies (si .snd)
+⊑-lub-least {Ix = Ix} {set = set} {s = s} {dir = dir} x le .refines =
+ □-elim (λ _ → set _ _) λ (i , si) → le i .refines si
+```
+
+
+Therefore, the type of partial elements forms a DCPO.
+
+```agda
+Parts-is-dcpo : ∀ {A : Set ℓ} → is-dcpo (Parts A)
+Parts-is-dcpo {A = A} .is-dcpo.directed-lubs s dir .Lub.lub =
+ ⊑-lub (A .is-tr) s (dir .semidirected)
+Parts-is-dcpo {A = A} .is-dcpo.directed-lubs s dir .Lub.has-lub .is-lub.fam≤lub =
+ ⊑-lub-le
+Parts-is-dcpo {A = A} .is-dcpo.directed-lubs s dir .Lub.has-lub .is-lub.least =
+ ⊑-lub-least
+
+Parts-dcpo : (A : Set ℓ) → DCPO ℓ ℓ
+Parts-dcpo A = Parts A , Parts-is-dcpo
+```
+
+Furthermore, it forms a pointed DCPO, as it has least upper bounds of
+all semidirected families. However, we opt to explicitly construct a
+bottom for computational reasons.
+
+```agda
+never : Part A
+never .def = el ⊥ (hlevel 1)
+
+never-⊑ : ∀ {x : Part A} → never ⊑ x
+never-⊑ .implies ()
+never-⊑ .refines ()
+
+Parts-is-pointed-dcpo : ∀ {A : Set ℓ} → is-pointed-dcpo (Parts-dcpo A)
+Parts-is-pointed-dcpo .Bottom.bot = never
+Parts-is-pointed-dcpo .Bottom.has-bottom _ = never-⊑
+
+Parts-pointed-dcpo : ∀ (A : Set ℓ) → Pointed-dcpo ℓ ℓ
+Parts-pointed-dcpo A = Parts-dcpo A , Parts-is-pointed-dcpo
+```
+
+Next, we shall construct a functor from $\Sets$ to the category of pointed
+DCPOs that maps a set $A$ to the pointed DCPO of partial elements of $A$.
+
+```agda
+part-map : (A → B) → Part A → Part B
+part-map f x .def = x .def
+part-map f x .elt px = f (x .elt px)
+
+part-map-⊑
+ : ∀ {f : A → B} {x y : Part A}
+ → x ⊑ y → part-map f x ⊑ part-map f y
+part-map-⊑ p .implies = p .implies
+part-map-⊑ {f = f} p .refines d = ap f (p .refines d)
+
+part-map-id : ∀ (x : Part A) → part-map (λ a → a) x ≡ x
+part-map-id x =
+ part-ext (λ p → p) (λ p → p)
+ (λ _ _ → ap (x .elt) (x .def .is-tr _ _))
+
+part-map-∘
+ : ∀ (f : B → C) (g : A → B)
+ → ∀ (x : Part A) → part-map (f ⊙ g) x ≡ part-map f (part-map g x)
+part-map-∘ f g x =
+ part-ext (λ p → p) (λ p → p)
+ (λ _ _ → ap (f ⊙ g ⊙ x .elt) (x .def .is-tr _ _))
+```
+
+The mapping we just defined also preserves least upper bounds and
+bottom elements, and thus defines a functor.
+
+```agda
+part-map-lub
+ : ∀ {Ix : Type ℓ}
+ → {A : Set o} {B : Set o'}
+ → {s : Ix → Part ∣ A ∣}
+ → {dir : ∀ i j → ∃[ k ∈ Ix ] (s i ⊑ s k × s j ⊑ s k)}
+ → (f : ∣ A ∣ → ∣ B ∣)
+ → is-lub (Parts B) (part-map f ⊙ s) (part-map f (⊑-lub (A .is-tr) s dir))
+part-map-lub f .is-lub.fam≤lub i = part-map-⊑ (⊑-lub-le i)
+part-map-lub f .is-lub.least y le .implies =
+ □-rec! λ si → le (si .fst) .implies (si .snd)
+part-map-lub {B = B} f .is-lub.least y le .refines =
+ □-elim (λ _ → B .is-tr _ _) λ si → le (si .fst) .refines (si .snd)
+
+part-map-never : ∀ {f : A → B} {x} → part-map f never ⊑ x
+part-map-never .implies ()
+part-map-never .refines ()
+
+Free-Pointed-dcpo : Functor (Sets ℓ) (Pointed-DCPOs ℓ ℓ)
+Free-Pointed-dcpo .F₀ A =
+ Parts-pointed-dcpo A
+Free-Pointed-dcpo .F₁ {x = A} f =
+ to-strict-scott-bottom (part-map f)
+ (λ _ _ → part-map-⊑)
+ (λ _ _ → part-map-lub {A = A} f)
+ (λ _ → part-map-never)
+Free-Pointed-dcpo .F-id =
+ strict-scott-path part-map-id
+Free-Pointed-dcpo .F-∘ f g =
+ strict-scott-path (part-map-∘ f g)
+```
+
+Finally, we shall show that this functor is left-adjoint to the
+forgetful functor into $\Sets$. We start by constructing the unit
+of the adjunction, which takes an element $a : A$ to $\top, \lambda tt. a$.
+
+```agda
+always : A → Part A
+always a .def = el ⊤ (hlevel 1)
+always a .elt _ = a
+
+always-inj : ∀ {x y : Type ℓ} → always x ≡ always y → x ≡ y
+always-inj {x = x} p =
+ J (λ y p → (d : is-defined y) → x ≡ y .elt d) (λ _ → refl) p tt
+```
+
+Next, we characterize refinements of `always`{.Agda}, and note that
+it is natural.
+
+```agda
+always-⊑
+ : ∀ {x : Part A} {y : A}
+ → (∀ (d : is-defined x) → x .elt d ≡ y) → x ⊑ always y
+always-⊑ p .implies _ = tt
+always-⊑ p .refines d = sym (p d)
+
+always-⊒
+ : ∀ {x : A} {y : Part A}
+ → (p : is-defined y) → x ≡ y .elt p
+ → always x ⊑ y
+always-⊒ p q .implies _ = p
+always-⊒ p q .refines _ = sym q
+
+always-natural
+ : ∀ {x : A} → (f : A → B) → part-map f (always x) ≡ always (f x)
+always-natural f = part-ext (λ _ → tt) (λ _ → tt) λ _ _ → refl
+```
+
+With that out of the way, we proceed to define the counit of the
+adjunction. Let $x$ be a partial element of a pointed DCPO $D$.
+We can define an element of $D$ that approximates $x$ by taking a
+directed join over the proposition associated with $x$.
+
+
+
+```agda
+ part-counit : Part Ob → Ob
+ part-counit x = ⋃-prop (x .elt ⊙ Lift.lower) def-prop
+ where abstract
+ def-prop : is-prop (Lift o (is-defined x))
+ def-prop = hlevel!
+```
+
+If $x$ is defined, then the counit simply extracts the value of $x$.
+
+```agda
+ part-counit-elt : (x : Part Ob) → (p : is-defined x) → part-counit x ≡ x .elt p
+ part-counit-elt x p =
+ ≤-antisym
+ (⋃-prop-least _ _ _ λ (lift p') → path→≤ (ap (x .elt) (x .def .is-tr _ _)))
+ (⋃-prop-le _ _ (lift p))
+```
+
+Furthermore, if $x$ is not defined, then the counit return the bottom element.
+
+```agda
+ part-counit-¬elt : (x : Part Ob) → (is-defined x → ⊥) → part-counit x ≡ bottom
+ part-counit-¬elt x ¬def =
+ ≤-antisym
+ (⋃-prop-least _ _ _ (λ p → absurd (¬def (Lift.lower p))))
+ (bottom≤x _)
+```
+
+We also note that the counit preserves refinements, least upper bounds, and
+bottom elements.
+
+```agda
+ part-counit-⊑ : (x y : Part Ob) → x ⊑ y → part-counit x ≤ part-counit y
+ part-counit-⊑ x y p =
+ ⋃-prop-least _ _ (part-counit y) λ (lift i) →
+ x .elt i =˘⟨ p .refines i ⟩
+ y .elt (p .implies i) ≤⟨ ⋃-prop-le _ _ (lift (p .implies i)) ⟩
+ ⋃-prop (y .elt ⊙ Lift.lower) _ ≤∎
+
+ part-counit-lub
+ : {Ix : Type o}
+ → (s : Ix → Part Ob)
+ → (sdir : is-semidirected-family (Parts set) s)
+ → is-lub poset (part-counit ⊙ s) (part-counit (⊑-lub (set .is-tr) s sdir))
+ part-counit-lub s sdir .is-lub.fam≤lub i =
+ ⋃-prop-least _ _ _ λ (lift p) →
+ ⋃-prop-le _ _ (lift (inc (i , p)))
+ part-counit-lub {Ix = Ix} s sdir .is-lub.least y le =
+ ⋃-prop-least _ _ _ $ λ (lift p) →
+ □-elim (λ p → ≤-thin {x = ⊑-lub _ s sdir .elt p}) (λ where
+ (i , si) →
+ s i .elt si ≤⟨ ⋃-prop-le _ _ (lift si) ⟩
+ ⋃-prop _ _ ≤⟨ le i ⟩
+ y ≤∎)
+ p
+
+ part-counit-never
+ : ∀ x → part-counit never ≤ x
+ part-counit-never x = ⋃-prop-least _ _ x (absurd ⊙ Lift.lower)
+```
+
+We can tie this all together to obtain the desired adjunction.
+
+```agda
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo
+ : ∀ {ℓ} → Free-Pointed-dcpo {ℓ} ⊣ Forget-Pointed-dcpo
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo .unit .η A x = always x
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo .unit .is-natural x y f =
+ funext λ _ → sym (always-natural f)
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo .counit .η D =
+ to-strict-scott-bottom (part-counit D)
+ (part-counit-⊑ D)
+ (λ s dir → part-counit-lub D s (dir .semidirected))
+ (part-counit-never D)
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo .counit .is-natural D E f =
+ strict-scott-path λ x → sym $ Strict-scott.pres-⋃-prop f _ _ _
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo .zig {A} =
+ strict-scott-path λ x →
+ part-ext
+ (A?.⋃-prop-least _ _ x (λ p → always-⊒ (Lift.lower p) refl) .implies)
+ (λ p → A?.⋃-prop-le _ _ (lift p) .implies tt)
+ (λ p q →
+ sym (A?.⋃-prop-least _ _ x (λ p → always-⊒ (Lift.lower p) refl) .refines p)
+ ∙ ap (x .elt) (x .def .is-tr _ _))
+ where module A? = Pointed-dcpo (Parts-pointed-dcpo A)
+Free-Pointed-dcpo⊣Forget-Pointed-dcpo .zag {B} =
+ funext λ x →
+ sym $ lub-of-const-fam B.poset (λ _ _ → refl) (B.⋃-prop-lub _ _ ) (lift tt)
+ where module B = Pointed-dcpo B
+```
+
+## Monad Structure
+
+The adjunction from the previous section yields a monad on the category of sets,
+but we opt to define it by hand to get better computational behaviour.
+
+```agda
+part-ap : Part (A → B) → Part A → Part B
+part-ap f x .def = el (is-defined f × is-defined x) hlevel!
+part-ap f x .elt (pf , px) = f .elt pf (x .elt px)
+
+part-bind : Part A → (A → Part B) → Part B
+part-bind x f .def =
+ el (Σ[ px ∈ is-defined x ] is-defined (f (x .elt px))) hlevel!
+part-bind x f .elt (px , pfx) =
+ f (x .elt px) .elt pfx
+```
+
+
diff --git a/src/Order/DCPO/Pointed.lagda.md b/src/Order/DCPO/Pointed.lagda.md
new file mode 100644
index 000000000..93cd93e2d
--- /dev/null
+++ b/src/Order/DCPO/Pointed.lagda.md
@@ -0,0 +1,571 @@
+
+
+```agda
+module Order.DCPO.Pointed where
+```
+
+
+
+# Pointed DCPOs
+
+A [DCPO] is **pointed** if it has a least element $\bot$. This is a
+property of a DCPO, as bottom elements are unique.
+
+[DCPO]: Order.DCPO.html
+
+```agda
+is-pointed-dcpo : DCPO o ℓ → Type _
+is-pointed-dcpo D = Bottom (DCPO.poset D)
+
+is-pointed-dcpo-is-prop : ∀ (D : DCPO o ℓ) → is-prop (is-pointed-dcpo D)
+is-pointed-dcpo-is-prop D = Bottom-is-prop (DCPO.poset D)
+```
+
+A DCPO is pointed if and only if it has least upper bounds of all
+semidirected families.
+
+
+
+The forward direction is straightforward: bottom elements are equivalent
+to least upper bounds of the empty family $\bot \to D$, and this family
+is trivially semidirected.
+
+```agda
+ semidirected-lub→pointed
+ : (∀ {Ix : Type o} (s : Ix → Ob) → is-semidirected-family poset s → Lub poset s)
+ → is-pointed-dcpo D
+ semidirected-lub→pointed lub =
+ Lub→Bottom poset (lower-lub poset (lub (absurd ⊙ Lift.lower) (absurd ⊙ Lift.lower)))
+```
+
+Conversely, if $D$ has a bottom element $\bot$, then we can extend any semidirected
+family $I \to D$ to a directed family $\rm{Maybe}(I) \to D$ by sending `nothing`
+to the bottom element.
+
+
+
+```agda
+ extend-bottom : (Ix → Ob) → Maybe Ix → Ob
+ extend-bottom s nothing = bot
+ extend-bottom s (just i) = s i
+
+ extend-bottom-directed
+ : (s : Ix → Ob) → is-semidirected-family poset s
+ → is-directed-family poset (extend-bottom s)
+ extend-bottom-directed s semidir .elt = inc nothing
+ extend-bottom-directed s semidir .semidirected (just i) (just j) = do
+ (k , i≤k , j≤k) ← semidir i j
+ pure (just k , i≤k , j≤k)
+ extend-bottom-directed s semidir .semidirected (just x) nothing =
+ pure (just x , ≤-refl , ¡)
+ extend-bottom-directed s semidir .semidirected nothing (just y) =
+ pure (just y , ¡ , ≤-refl)
+ extend-bottom-directed s semidir .semidirected nothing nothing =
+ pure (nothing , ≤-refl , ≤-refl)
+```
+
+Furthermore, $s$ has a least upper bound only if the extended family does.
+
+```agda
+ lub→extend-bottom-lub
+ : ∀ {s : Ix → Ob} {x : Ob} → is-lub poset s x → is-lub poset (extend-bottom s) x
+ lub→extend-bottom-lub {s = s} {x = x} x-lub .fam≤lub (just i) = x-lub .fam≤lub i
+ lub→extend-bottom-lub {s = s} {x = x} x-lub .fam≤lub nothing = ¡
+ lub→extend-bottom-lub {s = s} {x = x} x-lub .least y le = x-lub .least y (le ⊙ just)
+
+ extend-bottom-lub→lub
+ : ∀ {s : Ix → Ob} {x : Ob} → is-lub poset (extend-bottom s) x → is-lub poset s x
+ extend-bottom-lub→lub x-lub .fam≤lub i = x-lub .fam≤lub (just i)
+ extend-bottom-lub→lub x-lub .least y le = x-lub .least y λ where
+ nothing → ¡
+ (just i) → le i
+```
+
+If we put this all together, we see that any semidirected family has a least
+upper bound in a pointed DCPO.
+
+```agda
+ pointed→semidirected-lub
+ : is-pointed-dcpo D
+ → ∀ {Ix : Type o} (s : Ix → Ob) → is-semidirected-family poset s → Lub poset s
+ pointed→semidirected-lub pointed {Ix = Ix} s semidir .Lub.lub =
+ ⋃ (extend-bottom s) (extend-bottom-directed s semidir)
+ pointed→semidirected-lub pointed {Ix = Ix} s semidir .Lub.has-lub =
+ extend-bottom-lub→lub (⋃.has-lub _ _)
+```
+
+## Fixpoints
+
+Let $D$ be a pointed DCPO. Every Scott continuous function $f : D \to D$ has a
+[least fixed point].
+
+[least fixed point]: Order.Diagram.Fixpoint.html
+
+```agda
+module _ {o ℓ} {D : DCPO o ℓ} where
+ open DCPO D
+
+ pointed→least-fixpoint
+ : is-pointed-dcpo D
+ → (f : DCPOs.Hom D D)
+ → Least-fixpoint poset (Scott.mono f)
+ pointed→least-fixpoint pointed f = f-fix where
+ open Bottom pointed
+ module f = Scott f
+```
+
+We begin by constructing a directed family $\NN \to D$ that maps $n$ to
+$f^n(\bot)$.
+
+```
+ fⁿ : Nat → Ob → Ob
+ fⁿ zero x = x
+ fⁿ (suc n) x = f.hom (fⁿ n x)
+
+ fⁿ-mono : ∀ {i j} → i Nat.≤ j → fⁿ i bot ≤ fⁿ j bot
+ fⁿ-mono Nat.0≤x = ¡
+ fⁿ-mono (Nat.s≤s p) = f.monotone _ _ (fⁿ-mono p)
+
+ fⁿ⊥ : Lift o Nat → Ob
+ fⁿ⊥ (lift n) = fⁿ n bot
+
+ fⁿ⊥-dir : is-directed-family poset fⁿ⊥
+ fⁿ⊥-dir .is-directed-family.elt = inc (lift zero)
+ fⁿ⊥-dir .is-directed-family.semidirected (lift i) (lift j) =
+ inc (lift (Nat.max i j) , fⁿ-mono (Nat.max-≤l i j) , fⁿ-mono (Nat.max-≤r i j))
+```
+
+The least upper bound of this sequence shall be our least fixpoint. We
+begin by proving a slightly stronger variation of the universal property;
+namely for any $y$ such that $f y \le y$, $\bigcup (f^{n}(\bot)) \le y$.
+This follows from som quick induction.
+
+```agda
+ fⁿ⊥≤fix : ∀ (y : Ob) → f.hom y ≤ y → ∀ n → fⁿ⊥ n ≤ y
+ fⁿ⊥≤fix y p (lift zero) = ¡
+ fⁿ⊥≤fix y p (lift (suc n)) =
+ f.hom (fⁿ n bot) ≤⟨ f.monotone _ _ (fⁿ⊥≤fix y p (lift n)) ⟩
+ f.hom y ≤⟨ p ⟩
+ y ≤∎
+
+ least-fix : ∀ (y : Ob) → f.hom y ≤ y → ⋃ fⁿ⊥ fⁿ⊥-dir ≤ y
+ least-fix y p = ⋃.least _ _ _ (fⁿ⊥≤fix y p)
+```
+
+Now, let's show that $\bigcup (f^{n}(\bot))$ is actuall a fixpoint.
+First, the forward direction: $\bigcup (f^{n}(\bot)) \le f (\bigcup (f^{n}(\bot)))$.
+This follows directly from Scott-continuity of $f$.
+
+```agda
+ roll : f.hom (⋃ fⁿ⊥ fⁿ⊥-dir) ≤ ⋃ fⁿ⊥ fⁿ⊥-dir
+ roll =
+ Scott.hom f (⋃ fⁿ⊥ _) =⟨ f.pres-⋃ fⁿ⊥ fⁿ⊥-dir ⟩
+ ⋃ (Scott.hom f ⊙ fⁿ⊥) _ ≤⟨ ⋃.least _ _ _ (λ (lift n) → ⋃.fam≤lub _ _ (lift (suc n))) ⟩
+ ⋃ fⁿ⊥ _ ≤∎
+```
+
+To show the converse, we use universal property we proved earlier to
+re-arrange the goal to $f (f (\bigcup (f^{n}(\bot)))) \le f (\bigcup (f^{n}(\bot)))$.
+We can then apply monotonicity of $f$, and then use the forward direction
+to finish off the proof.
+
+```agda
+ unroll : ⋃ fⁿ⊥ fⁿ⊥-dir ≤ f.hom (⋃ fⁿ⊥ fⁿ⊥-dir)
+ unroll = least-fix (Scott.hom f (⋃ fⁿ⊥ fⁿ⊥-dir)) $
+ f.monotone _ _ roll
+```
+
+All that remains is to package up the data.
+
+```agda
+ f-fix : Least-fixpoint poset f.mono
+ f-fix .Least-fixpoint.fixpoint = ⋃ fⁿ⊥ fⁿ⊥-dir
+ f-fix .Least-fixpoint.has-least-fixpoint .is-least-fixpoint.fixed =
+ ≤-antisym roll unroll
+ f-fix .Least-fixpoint.has-least-fixpoint .is-least-fixpoint.least y y-fix =
+ least-fix y (path→≤ y-fix)
+```
+
+## Strictly Scott-continuous maps
+
+A Scott-continuous map is **strictly continuous** if it preserves bottoms.
+
+
+
+```agda
+ is-strictly-scott-continuous : (f : DCPOs.Hom D E) → Type _
+ is-strictly-scott-continuous f =
+ ∀ (x : D.Ob) → is-bottom D.poset x → is-bottom E.poset (Scott.hom f x)
+```
+
+```agda
+ is-strictly-scott-is-prop
+ : (f : DCPOs.Hom D E) → is-prop (is-strictly-scott-continuous f)
+ is-strictly-scott-is-prop f = Π-is-hlevel² 1 λ x _ →
+ is-bottom-is-prop E.poset (Scott.hom f x)
+```
+
+
+Strictly Scott-continuous functions are closed under identities
+and composites.
+
+```agda
+strict-scott-id
+ : ∀ {D : DCPO o ℓ}
+ → is-strictly-scott-continuous (DCPOs.id {x = D})
+strict-scott-id x x-bot = x-bot
+
+strict-scott-∘
+ : ∀ {D E F : DCPO o ℓ}
+ → (f : DCPOs.Hom E F) (g : DCPOs.Hom D E)
+ → is-strictly-scott-continuous f → is-strictly-scott-continuous g
+ → is-strictly-scott-continuous (f DCPOs.∘ g)
+strict-scott-∘ f g f-strict g-strict x x-bot =
+ f-strict (Scott.hom g x) (g-strict x x-bot)
+```
+
+Pointed DCPOs and strictly Scott-continuous functions form a subcategory
+of the category of DCPOs.
+
+```agda
+Pointed-DCPOs-subcat : ∀ o ℓ → Subcat (DCPOs o ℓ) (o ⊔ ℓ) (o ⊔ ℓ)
+Pointed-DCPOs-subcat o ℓ .Subcat.is-ob = is-pointed-dcpo
+Pointed-DCPOs-subcat o ℓ .Subcat.is-hom f _ _ = is-strictly-scott-continuous f
+Pointed-DCPOs-subcat o ℓ .Subcat.is-hom-prop f _ _ =
+ is-strictly-scott-is-prop f
+Pointed-DCPOs-subcat o ℓ .Subcat.is-hom-id {D} _ = strict-scott-id {D = D}
+Pointed-DCPOs-subcat o ℓ .Subcat.is-hom-∘ {f = f} {g = g} f-strict g-strict =
+ strict-scott-∘ f g f-strict g-strict
+
+Pointed-DCPOs : ∀ o ℓ → Precategory (lsuc (o ⊔ ℓ)) (lsuc o ⊔ ℓ)
+Pointed-DCPOs o ℓ = Subcategory (Pointed-DCPOs-subcat o ℓ)
+
+Pointed-DCPOs-is-category : is-category (Pointed-DCPOs o ℓ)
+Pointed-DCPOs-is-category =
+ subcat-is-category DCPOs-is-category is-pointed-dcpo-is-prop
+```
+
+# Reasoning with Pointed DCPOs
+
+The following module re-exports facts about pointed DCPOs, and also
+proves a bunch of useful lemma.s
+
+
+
+```agda
+module Pointed-dcpo {o ℓ} (D : Pointed-dcpo o ℓ) where
+```
+
+
+These proofs are all quite straightforward, so we omit them.
+
+```
+ open is-directed-family
+
+ dcpo : DCPO o ℓ
+ dcpo = D .fst
+
+ has-pointed : is-pointed-dcpo dcpo
+ has-pointed = D .snd
+
+ open DCPO dcpo public
+
+ bottom : Ob
+ bottom = Bottom.bot (D .snd)
+
+ bottom≤x : ∀ x → bottom ≤ x
+ bottom≤x = Bottom.has-bottom (D .snd)
+
+ adjoin : ∀ {Ix : Type o} → (Ix → Ob) → Maybe Ix → Ob
+ adjoin = extend-bottom dcpo has-pointed
+
+ adjoin-directed
+ : ∀ (s : Ix → Ob) → is-semidirected-family poset s
+ → is-directed-family poset (adjoin s)
+ adjoin-directed = extend-bottom-directed dcpo has-pointed
+
+ lub→adjoin-lub : ∀ {s : Ix → Ob} {x : Ob} → is-lub poset s x → is-lub poset (adjoin s) x
+ lub→adjoin-lub = lub→extend-bottom-lub dcpo has-pointed
+
+ adjoin-lub→lub : ∀ {s : Ix → Ob} {x : Ob} → is-lub poset (adjoin s) x → is-lub poset s x
+ adjoin-lub→lub = extend-bottom-lub→lub dcpo has-pointed
+
+ -- We put these behind 'opaque' to prevent blow ups in goals.
+ opaque
+ ⋃-semi : (s : Ix → Ob) → is-semidirected-family poset s → Ob
+ ⋃-semi s semidir = ⋃ (adjoin s) (adjoin-directed s semidir)
+
+ ⋃-semi-lub
+ : ∀ (s : Ix → Ob) (dir : is-semidirected-family poset s)
+ → is-lub poset s (⋃-semi s dir)
+ ⋃-semi-lub s dir = adjoin-lub→lub (⋃.has-lub (adjoin s) (adjoin-directed s dir))
+
+ ⋃-semi-le
+ : ∀ (s : Ix → Ob) (dir : is-semidirected-family poset s)
+ → ∀ i → s i ≤ ⋃-semi s dir
+ ⋃-semi-le s dir = is-lub.fam≤lub (⋃-semi-lub s dir)
+
+ ⋃-semi-least
+ : ∀ (s : Ix → Ob) (dir : is-semidirected-family poset s)
+ → ∀ x → (∀ i → s i ≤ x) → ⋃-semi s dir ≤ x
+ ⋃-semi-least s dir x le = is-lub.least (⋃-semi-lub s dir) x le
+
+ ⋃-semi-pointwise
+ : ∀ {Ix} {s s' : Ix → Ob}
+ → {fam : is-semidirected-family poset s} {fam' : is-semidirected-family poset s'}
+ → (∀ ix → s ix ≤ s' ix)
+ → ⋃-semi s fam ≤ ⋃-semi s' fam'
+ ⋃-semi-pointwise le = ⋃-pointwise λ where
+ (just i) → le i
+ nothing → bottom≤x _
+```
+
+
+However, we do call attention to one extremely useful fact: if $D$ is
+a pointed DCPO, then it has least upper bounds of families indexed by
+propositions.
+
+```agda
+ opaque
+ ⋃-prop : ∀ {Ix : Type o} → (Ix → Ob) → is-prop Ix → Ob
+ ⋃-prop s ix-prop = ⋃-semi s (prop-indexed→semidirected poset s ix-prop)
+
+ ⋃-prop-le
+ : ∀ (s : Ix → Ob) (p : is-prop Ix)
+ → ∀ i → s i ≤ ⋃-prop s p
+ ⋃-prop-le s p i = ⋃-semi-le _ _ i
+
+ ⋃-prop-least
+ : ∀ (s : Ix → Ob) (p : is-prop Ix)
+ → ∀ x → (∀ i → s i ≤ x) → ⋃-prop s p ≤ x
+ ⋃-prop-least s p = ⋃-semi-least _ _
+
+ ⋃-prop-lub
+ : ∀ (s : Ix → Ob) (p : is-prop Ix)
+ → is-lub poset s (⋃-prop s p)
+ ⋃-prop-lub s p = ⋃-semi-lub _ _
+```
+
+This allows us to reflect the truth value of a proposition into $D$.
+
+```agda
+ opaque
+ ⋃-prop-false
+ : ∀ (s : Ix → Ob) (p : is-prop Ix)
+ → ¬ Ix → ⋃-prop s p ≡ bottom
+ ⋃-prop-false s p ¬i =
+ ≤-antisym
+ (⋃-prop-least s p bottom (absurd ⊙ ¬i))
+ (bottom≤x _)
+
+ ⋃-prop-true
+ : ∀ (s : Ix → Ob) (p : is-prop Ix)
+ → (i : Ix) → ⋃-prop s p ≡ s i
+ ⋃-prop-true s p i =
+ sym $ lub-of-const-fam poset (λ i j → ap s (p i j)) (⋃-prop-lub s p) i
+```
+
+We define a similar module for strictly Scott-continuous maps.
+
+```agda
+module Strict-scott {D E : Pointed-dcpo o ℓ} (f : Pointed-DCPOs.Hom D E) where
+```
+
+
+These proofs are all quite straightforward, so we omit them.
+
+```agda
+ private
+ module D = Pointed-dcpo D
+ module E = Pointed-dcpo E
+
+ scott : DCPOs.Hom D.dcpo E.dcpo
+ scott = Subcat-hom.hom f
+
+ open Scott scott public
+
+ opaque
+ pres-bottoms : ∀ x → is-bottom D.poset x → is-bottom E.poset (hom x)
+ pres-bottoms = Subcat-hom.witness f
+
+ pres-⊥ : hom D.bottom ≡ E.bottom
+ pres-⊥ = bottom-unique E.poset (pres-bottoms D.bottom D.bottom≤x) E.bottom≤x
+
+ pres-adjoin-lub
+ : ∀ {s : Ix → D.Ob} {x : D.Ob}
+ → is-semidirected-family D.poset s
+ → is-lub D.poset (D.adjoin s) x → is-lub E.poset (E.adjoin (hom ⊙ s)) (hom x)
+ pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.fam≤lub (just i) =
+ monotone _ _ (is-lub.fam≤lub x-lub (just i))
+ pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.fam≤lub nothing =
+ E.bottom≤x (hom x)
+ pres-adjoin-lub {s = s} {x = x} sdir x-lub .is-lub.least y le =
+ is-lub.least
+ (pres-directed-lub (D.adjoin s) (D.adjoin-directed s sdir) x x-lub) y λ where
+ (just i) → le (just i)
+ nothing → pres-bottoms _ D.bottom≤x y
+
+ pres-semidirected-lub
+ : ∀ {Ix} (s : Ix → D.Ob) → is-semidirected-family D.poset s
+ → ∀ x → is-lub D.poset s x → is-lub E.poset (hom ⊙ s) (hom x)
+ pres-semidirected-lub s sdir x x-lub =
+ E.adjoin-lub→lub (pres-adjoin-lub sdir (D.lub→adjoin-lub x-lub))
+
+ pres-⋃-prop
+ : ∀ {Ix} (s : Ix → D.Ob) (p q : is-prop Ix)
+ → hom (D.⋃-prop s p) ≡ E.⋃-prop (hom ⊙ s) q
+ pres-⋃-prop s p q =
+ lub-unique E.poset
+ (pres-semidirected-lub _
+ (prop-indexed→semidirected D.poset s p) (D.⋃-prop s p) (D.⋃-prop-lub s p))
+ (E.⋃-prop-lub _ _)
+
+ bottom-bounded : ∀ {x y} → x D.≤ y → hom y ≡ E.bottom → hom x ≡ E.bottom
+ bottom-bounded {x = x} {y = y} p y-bot =
+ E.≤-antisym
+ (hom x E.≤⟨ monotone _ _ p ⟩
+ hom y E.=⟨ y-bot ⟩
+ E.bottom E.≤∎)
+ (E.bottom≤x _)
+```
+
+
+
+
+We also provide a handful of ways of constructing strictly Scott-continuous
+maps. First, we note that if $f$ is monotonic and preserves the chosen
+least upper bound of _semidirected_ families, then $f$ is strictly
+Scott-continuous.
+
+```agda
+ to-strict-scott-⋃-semi
+ : (f : D.Ob → E.Ob)
+ → (∀ x y → x D.≤ y → f x E.≤ f y)
+ → (∀ {Ix} (s : Ix → D.Ob) → (dir : is-semidirected-family D.poset s)
+ → is-lub E.poset (f ⊙ s) (f (D.⋃-semi s dir)))
+ → Pointed-DCPOs.Hom D E
+ to-strict-scott-⋃-semi f monotone pres-⋃-semi =
+ sub-hom (to-scott f monotone pres-⋃) pres-bot
+ where
+ pres-⋃
+ : ∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
+ → is-lub E.poset (f ⊙ s) (f (D.⋃ s dir))
+ pres-⋃ s dir .is-lub.fam≤lub i =
+ monotone _ _ $ D.⋃.fam≤lub _ _ i
+ pres-⋃ s dir .is-lub.least y le =
+ f (D.⋃ s dir) E.=⟨ ap f (lub-unique D.poset (D.⋃.has-lub _ _) (D.⋃-semi-lub s (dir .semidirected))) ⟩
+ f (D.⋃-semi s (dir .semidirected)) E.≤⟨ is-lub.least (pres-⋃-semi _ _) y le ⟩
+ y E.≤∎
+
+ pres-bot : ∀ x → is-bottom D.poset x → is-bottom E.poset (f x)
+ pres-bot x x-bot y =
+ f x E.≤⟨ monotone _ _ (x-bot _) ⟩
+ f (D.⋃-semi _ _) E.≤⟨ is-lub.least (pres-⋃-semi (absurd ⊙ Lift.lower) (absurd ⊙ Lift.lower)) y (absurd ⊙ Lift.lower) ⟩
+ y E.≤∎
+```
+
+Next, if $f$ is monotonic, preserves chosen least upper bounds of directed
+families, and preserves chosen bottoms, then $f$ is strictly
+Scott-continuous.
+
+```agda
+ to-strict-scott-bottom
+ : (f : D.Ob → E.Ob)
+ → (∀ x y → x D.≤ y → f x E.≤ f y)
+ → (∀ {Ix} (s : Ix → D.Ob) → (dir : is-directed-family D.poset s)
+ → is-lub E.poset (f ⊙ s) (f (D.⋃ s dir)))
+ → is-bottom E.poset (f D.bottom)
+ → Pointed-DCPOs.Hom D E
+ to-strict-scott-bottom f monotone pres-⋃ pres-bot =
+ sub-hom (to-scott f monotone pres-⋃) λ x x-bot y →
+ f x E.≤⟨ monotone _ _ (x-bot _) ⟩
+ f D.bottom E.≤⟨ pres-bot y ⟩
+ y E.≤∎
+```
+
+Finally, if $f$ preserves arbitrary least upper bounds of semidirected
+families, then $f$ must be monotonic, and thus strictly Scott-continuous.
+
+```agda
+ to-strict-scott-semidirected
+ : (f : D.Ob → E.Ob)
+ → (∀ {Ix} (s : Ix → D.Ob) → (dir : is-semidirected-family D.poset s)
+ → ∀ x → is-lub D.poset s x → is-lub E.poset (f ⊙ s) (f x))
+ → Pointed-DCPOs.Hom D E
+ to-strict-scott-semidirected f pres =
+ sub-hom
+ (to-scott-directed f
+ (λ s dir x lub → pres s (is-directed-family.semidirected dir) x lub))
+ (λ x x-bot y → is-lub.least
+ (pres _ (absurd ⊙ Lift.lower) x (lift-is-lub D.poset (is-bottom→is-lub D.poset x-bot)))
+ y
+ (absurd ⊙ Lift.lower))
+```
diff --git a/src/Order/Diagram/Fixpoint.lagda.md b/src/Order/Diagram/Fixpoint.lagda.md
new file mode 100644
index 000000000..05c84f0f2
--- /dev/null
+++ b/src/Order/Diagram/Fixpoint.lagda.md
@@ -0,0 +1,79 @@
+
+
+```agda
+module Order.Diagram.Fixpoint {o ℓ} (P : Poset o ℓ) where
+```
+
+
+
+Let $(P, \le)$ be a poset, and $f : P \to P$ be a monotone map. We say
+that $f$ has a **least fixpoint** if there exists some $x : P$ such that
+$f(x) = x$, and for every other $y$ such that $f(y) = y$, $x \le y$.
+
+```agda
+record is-least-fixpoint (f : Posets.Hom P P) (x : Ob) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ fixed : f .hom x ≡ x
+ least : ∀ (y : Ob) → f .hom y ≡ y → x ≤ y
+
+record Least-fixpoint (f : Posets.Hom P P) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ fixpoint : Ob
+ has-least-fixpoint : is-least-fixpoint f fixpoint
+ open is-least-fixpoint has-least-fixpoint public
+
+open is-least-fixpoint
+```
+
+Least fixed points are unique, so the type of least fixpoints of $f$ is
+a proposition.
+
+```agda
+least-fixpoint-unique
+ : ∀ {f : Posets.Hom P P} {x y}
+ → is-least-fixpoint f x → is-least-fixpoint f y
+ → x ≡ y
+least-fixpoint-unique x-fix y-fix =
+ ≤-antisym (x-fix .least _ (y-fix .fixed)) (y-fix .least _ (x-fix .fixed))
+
+is-least-fixpoint-is-prop
+ : ∀ {f : Posets.Hom P P} {x}
+ → is-prop (is-least-fixpoint f x)
+is-least-fixpoint-is-prop {f = f} {x = x} p q i .fixed =
+ has-is-set (f .hom x) x (p .fixed) (q .fixed) i
+is-least-fixpoint-is-prop {f = f} {x = x} p q i .least y y-fix =
+ is-prop→pathp
+ (λ i → ≤-thin)
+ (p .least y y-fix) (q .least y y-fix) i
+
+Least-fixpoint-is-prop
+ : ∀ {f : Posets.Hom P P}
+ → is-prop (Least-fixpoint f)
+Least-fixpoint-is-prop {f = f} p q = p≡q where
+ module p = Least-fixpoint p
+ module q = Least-fixpoint q
+
+ path : p.fixpoint ≡ q.fixpoint
+ path = least-fixpoint-unique p.has-least-fixpoint q.has-least-fixpoint
+
+ p≡q : p ≡ q
+ p≡q i .Least-fixpoint.fixpoint = path i
+ p≡q i .Least-fixpoint.has-least-fixpoint =
+ is-prop→pathp (λ i → is-least-fixpoint-is-prop {x = path i})
+ p.has-least-fixpoint q.has-least-fixpoint i
+```
diff --git a/src/Order/Diagram/Glb.lagda.md b/src/Order/Diagram/Glb.lagda.md
index be3b2d295..472fa6e0f 100644
--- a/src/Order/Diagram/Glb.lagda.md
+++ b/src/Order/Diagram/Glb.lagda.md
@@ -1,6 +1,7 @@
```agda
-module Order.Diagram.Glb where
+module Order.Diagram.Glb {o ℓ} (P : Poset o ℓ) where
```
+
+
# Greatest lower bounds
A **glb** $g$ (short for **greatest lower bound**) for a family of
@@ -35,85 +42,146 @@ artificial, and it's just because we can't reuse the identifier
us, a meet is a glb of two elements.
```agda
-module _ {ℓ ℓ′} (P : Poset ℓ ℓ′) where
- private module P = Poset P
-
- record is-glb {ℓᵢ} {I : Type ℓᵢ} (F : I → P.Ob) (glb : P.Ob)
- : Type (ℓ ⊔ ℓ′ ⊔ ℓᵢ) where
- field
- glb≤fam : ∀ i → glb P.≤ F i
- greatest : (lb′ : P.Ob) → (∀ i → lb′ P.≤ F i) → lb′ P.≤ glb
+record is-glb {ℓᵢ} {I : Type ℓᵢ} (F : I → Ob) (glb : Ob)
+ : Type (o ⊔ ℓ ⊔ ℓᵢ) where
+ no-eta-equality
+ field
+ glb≤fam : ∀ i → glb ≤ F i
+ greatest : (lb′ : Ob) → (∀ i → lb′ ≤ F i) → lb′ ≤ glb
+
+record Glb {ℓᵢ} {I : Type ℓᵢ} (F : I → Ob) : Type (o ⊔ ℓ ⊔ ℓᵢ) where
+ no-eta-equality
+ field
+ glb : Ob
+ has-glb : is-glb F glb
+ open is-glb has-glb public
```
+## Meets
+
As mentioned before, in the binary case, we refer to glbs as **meets**:
The meet of $a$ and $b$ is, if it exists, the greatest element
satisfying $(a \cap b) \le a$ and $(a \cap b) \le b$.
```agda
- record is-meet (a b : P.Ob) (glb : P.Ob) : Type (ℓ ⊔ ℓ′) where
- field
- meet≤l : glb P.≤ a
- meet≤r : glb P.≤ b
- greatest : (lb′ : P.Ob) → lb′ P.≤ a → lb′ P.≤ b → lb′ P.≤ glb
+record is-meet (a b : Ob) (glb : Ob) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ meet≤l : glb ≤ a
+ meet≤r : glb ≤ b
+ greatest : (lb′ : Ob) → lb′ ≤ a → lb′ ≤ b → lb′ ≤ glb
+
+record Meet (a b : Ob) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ glb : Ob
+ has-meet : is-meet a b glb
+ open is-meet has-meet public
- open is-meet
+open is-meet
```
A shuffling of terms shows that being a meet is precisely being the
greatest lower bound of a family of two elements.
```agda
- is-meet→is-glb : ∀ {a b glb} → is-meet a b glb → is-glb (if_then a else b) glb
- is-meet→is-glb meet .glb≤fam true = meet .meet≤l
- is-meet→is-glb meet .glb≤fam false = meet .meet≤r
- is-meet→is-glb meet .greatest glb′ x = meet .greatest glb′ (x true) (x false)
-
- is-glb→is-meet : ∀ {F : Bool → P.Ob} {glb} → is-glb F glb → is-meet (F true) (F false) glb
- is-glb→is-meet glb .meet≤l = glb .glb≤fam true
- is-glb→is-meet glb .meet≤r = glb .glb≤fam false
- is-glb→is-meet glb .greatest lb′ lb′
@@ -121,32 +189,107 @@ An important lemma about meets is that, if $x \le y$, then the greatest
lower bound of $x$ and $y$ is just $x$:
```agda
- le→is-meet : ∀ {a b} → a P.≤ b → is-meet a b a
- le→is-meet a≤b .meet≤l = P.≤-refl
- le→is-meet a≤b .meet≤r = a≤b
- le→is-meet a≤b .greatest lb′ lb′≤a _ = lb′≤a
+le→is-meet : ∀ {a b} → a ≤ b → is-meet a b a
+le→is-meet a≤b .meet≤l = ≤-refl
+le→is-meet a≤b .meet≤r = a≤b
+le→is-meet a≤b .greatest lb′ lb′≤a _ = lb′≤a
- le-meet : ∀ {a b l} → a P.≤ b → is-meet a b l → a ≡ l
- le-meet a≤b l = ap fst $ meet-unique (_ , le→is-meet a≤b) (_ , l)
+le-meet : ∀ {a b l} → a ≤ b → is-meet a b l → a ≡ l
+le-meet a≤b l = meet-unique (le→is-meet a≤b) l
```
-## As products
+### 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
- open Product
-
- is-meet→product : ∀ {a b glb : P.Ob} → is-meet a b glb → Product (poset→category P) a b
- is-meet→product glb .apex = _
- is-meet→product glb .π₁ = glb .is-meet.meet≤l
- is-meet→product glb .π₂ = glb .is-meet.meet≤r
- is-meet→product glb .has-is-product .⟨_,_⟩ q
+
+### As Terminal Objects
+
+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!
+
+```agda
+is-top→terminal : ∀ {x} → is-top x → is-terminal (poset→category P) x
+is-top→terminal is-top x .centre = is-top x
+is-top→terminal is-top x .paths _ = ≤-thin _ _
+
+terminal→is-top : ∀ {x} → is-terminal (poset→category P) x → is-top x
+terminal→is-top terminal x = terminal x .centre
```
diff --git a/src/Order/Diagram/Lub.lagda.md b/src/Order/Diagram/Lub.lagda.md
index 4f064ff38..3aa2962c9 100644
--- a/src/Order/Diagram/Lub.lagda.md
+++ b/src/Order/Diagram/Lub.lagda.md
@@ -1,6 +1,7 @@
```agda
-module Order.Diagram.Lub where
+module Order.Diagram.Lub {o ℓ} (P : Poset o ℓ) where
```
-# 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
@@ -31,101 +38,341 @@ lubs, with the binary name being **join**.
[glbs vs meets]: Order.Diagram.Glb.html
```agda
-module _ {ℓ ℓ′} (P : Poset ℓ ℓ′) where
- private module P = Poset P
+record is-lub
+ {ℓᵢ} {I : Type ℓᵢ} (F : I → Ob) (lub : Ob)
+ : Type (o ⊔ ℓ ⊔ ℓᵢ)
+ where
+ no-eta-equality
+ field
+ fam≤lub : ∀ i → F i ≤ lub
+ least : (ub′ : Ob) → (∀ i → F i ≤ ub′) → lub ≤ ub′
+
+record Lub {ℓᵢ} {I : Type ℓᵢ} (F : I → Ob) : Type (o ⊔ ℓ ⊔ ℓᵢ) where
+ no-eta-equality
+ field
+ lub : Ob
+ has-lub : is-lub F lub
+ open is-lub has-lub public
- record is-lub {ℓᵢ} {I : Type ℓᵢ} (F : I → P.Ob) (lub : P.Ob)
- : Type (ℓ ⊔ ℓ′ ⊔ ℓᵢ) where
- field
- fam≤lub : ∀ i → F i P.≤ lub
- least : (ub′ : P.Ob) → (∀ i → F i P.≤ ub′) → lub P.≤ ub′
+open is-lub
```
+Let $f : I \to P$ be a family. If there is some $i$ such that
+for all $j$, $f(j) < f(i)$, then $f(i)$ is the least upper bound of
+$f$.
+
+```agda
+fam-bound→is-lub
+ : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob}
+ → (i : I) → (∀ j → F j ≤ F i)
+ → is-lub F (F i)
+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.
+
+```agda
+lub-of-const-fam
+ : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob} {x}
+ → (∀ i j → F i ≡ F j)
+ → is-lub F x
+ → ∀ i → F i ≡ x
+lub-of-const-fam {F = F} is-const x-lub i =
+ ≤-antisym
+ (fam≤lub x-lub i)
+ (least x-lub (F i) λ j → path→≥ (is-const i j))
+```
+
+Furthermore, if $f : I \to A$ is a constant family and $I$ is merely
+inhabited, then $f$ has a least upper bound.
+
+```agda
+const-inhabited-fam→is-lub
+ : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob} {x}
+ → (∀ i → F i ≡ x)
+ → ∥ I ∥
+ → is-lub F x
+const-inhabited-fam→is-lub {I = I} {F = F} {x = x} is-const =
+ ∥-∥-rec is-lub-is-prop mk-is-lub where
+ mk-is-lub : I → is-lub F x
+ mk-is-lub i .is-lub.fam≤lub j = path→≤ (is-const j)
+ mk-is-lub i .is-lub.least y le =
+ x =˘⟨ is-const i ⟩
+ F i ≤⟨ le i ⟩
+ y ≤∎
+
+const-inhabited-fam→lub
+ : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob}
+ → (∀ i j → F i ≡ F j)
+ → ∥ I ∥
+ → Lub F
+const-inhabited-fam→lub {I = I} {F = F} is-const =
+ ∥-∥-rec Lub-is-prop mk-lub where
+ mk-lub : I → Lub F
+ mk-lub i .Lub.lub = F i
+ mk-lub i .Lub.has-lub =
+ 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
computation shows that being a join is _precisely_ being the lub of a
family of two elements.
```agda
- record is-join (a b : P.Ob) (lub : P.Ob) : Type (ℓ ⊔ ℓ′) where
- field
- l≤join : a P.≤ lub
- r≤join : b P.≤ lub
- least : (ub′ : P.Ob) → a P.≤ ub′ → b P.≤ ub′ → lub P.≤ ub′
+record is-join (a b : Ob) (lub : Ob) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ l≤join : a ≤ lub
+ r≤join : b ≤ lub
+ least : (ub′ : Ob) → a ≤ ub′ → b ≤ ub′ → lub ≤ ub′
- open is-join
+record Join (a b : Ob) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ lub : Ob
+ has-join : is-join a b lub
+ open is-join has-join public
- is-join→is-lub : ∀ {a b lub} → is-join a b lub → is-lub (if_then a else b) lub
- is-join→is-lub join .fam≤lub true = join .l≤join
- is-join→is-lub join .fam≤lub false = join .r≤join
- is-join→is-lub join .least ub′ x = join .least ub′ (x true) (x false)
+open is-join
- is-lub→is-join : ∀ {F : Bool → P.Ob} {lub} → is-lub F lub → is-join (F true) (F false) lub
- is-lub→is-join lub .l≤join = lub .fam≤lub true
- is-lub→is-join lub .r≤join = lub .fam≤lub false
- is-lub→is-join lub .least ub′ a
+
+An important lemma about joins is that, if $x \le y$, then the least
+upper bound of $x$ and $y$ is just $y$:
+
+```agda
+gt→is-join : ∀ {a b} → a ≤ b → is-join a b b
+gt→is-join a≤b .l≤join = a≤b
+gt→is-join a≤b .r≤join = ≤-refl
+gt→is-join a≤b .least ub′ _ b≤ub′ = b≤ub′
+
+gt-join : ∀ {a b l} → a ≤ b → is-join a b l → b ≡ l
+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.
+
+```agda
+open is-coproduct
+open Coproduct
+
+is-join→coproduct : ∀ {a b lub : Ob} → is-join a b lub → Coproduct (poset→category P) a b
+is-join→coproduct lub .coapex = _
+is-join→coproduct lub .in₀ = lub .is-join.l≤join
+is-join→coproduct lub .in₁ = lub .is-join.r≤join
+is-join→coproduct lub .has-is-coproduct .[_,_] a
-## As coproducts
+### As initial objects
-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.
+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!
```agda
- open is-coproduct
- open Coproduct
-
- is-join→coproduct : ∀ {a b lub : P.Ob} → is-join a b lub → Coproduct (poset→category P) a b
- is-join→coproduct lub .coapex = _
- is-join→coproduct lub .in₀ = lub .is-join.l≤join
- is-join→coproduct lub .in₁ = lub .is-join.r≤join
- is-join→coproduct lub .has-is-coproduct .[_,_] a
+
+```agda
+module Order.Instances.Discrete where
+```
+
+# Discrete Orders
+
+Every set $A$ can be turned into a [[poset]] by defining $x \le y$ to
+be $x = y$.
+
+```agda
+Disc : ∀ {ℓ} → Set ℓ → Poset ℓ ℓ
+Disc A = to-poset ∣ A ∣ mk-disc where
+ mk-disc : make-poset _ (A .∣_∣)
+ mk-disc .make-poset.rel = _≡_
+ mk-disc .make-poset.id = refl
+ mk-disc .make-poset.thin = A .is-tr _ _
+ mk-disc .make-poset.trans = _∙_
+ mk-disc .make-poset.antisym p _ = p
+```
+
+This extends to a functor from $\Sets$ into the category of posets.
+
+```agda
+DiscF : ∀ {ℓ} → Functor (Sets ℓ) (Posets ℓ ℓ)
+DiscF .Functor.F₀ = Disc
+DiscF .Functor.F₁ f = total-hom f (λ _ _ p → ap f p)
+DiscF .Functor.F-id = total-hom-path _ refl refl
+DiscF .Functor.F-∘ f g = total-hom-path _ refl refl
+```
+
+Furthermore, this functor is a [[left adjoint]] to the forgetful functor
+into $\Sets$.
+
+```agda
+DiscF⊣Forget : ∀ {ℓ} → DiscF {ℓ} ⊣ πᶠ _
+DiscF⊣Forget ._⊣_.unit ._=>_.η A x = x
+DiscF⊣Forget ._⊣_.unit ._=>_.is-natural _ _ _ = refl
+DiscF⊣Forget ._⊣_.counit ._=>_.η P =
+ total-hom (λ x → x) (λ _ _ → Poset.path→≤ P)
+DiscF⊣Forget ._⊣_.counit ._=>_.is-natural P Q f =
+ total-hom-path _ refl
+ (funext λ _ → funext λ _ → funext λ _ → Poset.≤-thin Q _ _)
+DiscF⊣Forget ._⊣_.zig {A = A} =
+ total-hom-path _ refl $
+ funext λ x → funext λ y → funext λ p →
+ J (λ y p → transport (λ i → p (~ i) ≡ y) refl ≡ p) (transport-refl _) p
+DiscF⊣Forget ._⊣_.zag = refl
+```
+
+## Least Upper Bounds
+
+If $f : I \to A$ has a [[least upper bound]] in the discrete poset on
+$A$, then $f$ must be a constant family.
+
+```agda
+disc-is-lub→const
+ : ∀ {ℓ iℓ} {Ix : Type iℓ} {A : Set ℓ}
+ → {f : Ix → ∣ A ∣} {x : ∣ A ∣}
+ → is-lub (Disc A) f x
+ → ∀ i → f i ≡ x
+disc-is-lub→const x-lub i = is-lub.fam≤lub x-lub i
+
+disc-lub→const
+ : ∀ {ℓ iℓ} {Ix : Type iℓ} {A : Set ℓ}
+ → {f : Ix → ∣ A ∣}
+ → Lub (Disc A) f
+ → ∀ i j → f i ≡ f j
+disc-lub→const x-lub i j =
+ Lub.fam≤lub x-lub i ∙ sym (Lub.fam≤lub x-lub j)
+```
diff --git a/src/Order/Instances/Lower/Cocompletion.lagda.md b/src/Order/Instances/Lower/Cocompletion.lagda.md
index e699e2a06..8cb4bea3d 100644
--- a/src/Order/Instances/Lower/Cocompletion.lagda.md
+++ b/src/Order/Instances/Lower/Cocompletion.lagda.md
@@ -67,9 +67,9 @@ saying that presheaves are computed as certain [coends].
```agda
lower-set-∫ : Ls ≡ Lower-sets-cocomplete P diagram .fst
- lower-set-∫ = ap fst $ lub-unique (Lower-sets P)
- (Ls , lower-set-is-lub)
- (Lower-sets-cocomplete P diagram)
+ lower-set-∫ = lub-unique (Lower-sets P)
+ (lower-set-is-lub)
+ (snd $ Lower-sets-cocomplete P diagram)
```