Tom de Jong, early January 2022.

Inspired by the paper "Continuous categories and exponentiable toposes" by Peter
Johnstone and AndrΓ© Joyal, we discuss the notions

(1) structural continuity of a dcpo;
(2) continuity of a dcpo;
(3) pseudocontinuity of a dcpo.

(1) and (2) are defined in Continuity.lagda and (3) is defined and examined here.
The notions (1)-(3) have the following shapes:

(1)   Ξ  (x : D) β   Ξ£ I : π₯ Μ  , Ξ£ Ξ± : I β D , Ξ± is-directed Γ ... Γ ...
(2) β₯ Ξ  (x : D) β   Ξ£ I : π₯ Μ  , Ξ£ Ξ± : I β D , Ξ± is-directed Γ ... Γ ... β₯
(3)   Ξ  (x : D) β β₯ Ξ£ I : π₯ Μ  , Ξ£ Ξ± : I β D , Ξ± is-directed Γ ... Γ ... β₯

So (2) and (3) are propositions, but (1) isn't. We illustrate (1)-(3) by
discussion them in terms of left adjoints. In these discussions, the
Ind-completion, as defined in IndCompletion.lagda plays an important role.

We show that (1) for a dcpo D is equivalent to asserting that the map
β : Ind(D) β D (which takes a directed family to its supremum) has a specified

It follows directly that (2) is equivalent to asking that β-map has an

Because Ind is a preorder and not a poset, the type expressing that β-map has a
specified left adjoint is not a proposition, as the supposed left adjoint can
map elements of D to bicofinal (but nonequal) directed families.

We could take the poset reflection Ind(D)/β of Ind(D) and ask that the map
β-map/ : Ind(D)/β β D induced by β : Ind(D) β D has a left adjoint to obtain a
type that is a proposition. We show that this amounts precisely to
pseudocontinuity.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan hiding (J)
open import UF.FunExt
open import UF.PropTrunc

module DomainTheory.BasesAndContinuity.ContinuityDiscussion
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(π₯ : Universe) -- where the index types for directed completeness live
where

open PropositionalTruncation pt

open import UF.Base hiding (_β_)
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Hedberg
open import UF.ImageAndSurjection pt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open import DomainTheory.Basics.Dcpo pt fe π₯
open import DomainTheory.Basics.Miscelanea pt fe π₯
open import DomainTheory.Basics.WayBelow pt fe π₯

open import DomainTheory.BasesAndContinuity.Continuity pt fe π₯
open import DomainTheory.BasesAndContinuity.IndCompletion pt fe π₯

\end{code}

Because we'll want to apply some standard equivalences later on, we first show
that our record-based definition of structural continuity is equivalent to one
using Ξ£-types.

\begin{code}

structurally-continuous-Ξ£ : (π : DCPO {π€} {π£}) β π₯ βΊ β π€ β π£ Μ
structurally-continuous-Ξ£ π =
β Ξ£ I κ π₯ Μ  , Ξ£ Ξ± κ (I β β¨ π β©) , (is-way-upperbound π x Ξ±)
Γ (Ξ£ Ξ΄ κ is-Directed π Ξ± , β π Ξ΄ οΌ x)

structurally-continuous-to-Ξ£ : (π : DCPO {π€} {π£})
β structurally-continuous π
β structurally-continuous-Ξ£ π
structurally-continuous-to-Ξ£ π C x =
index-of-approximating-family x
, approximating-family x
, approximating-family-is-way-below x
, approximating-family-is-directed x
, approximating-family-β-οΌ x
where
open structurally-continuous C

structurally-continuous-from-Ξ£ : (π : DCPO {π€} {π£})
β structurally-continuous-Ξ£ π
β structurally-continuous π
structurally-continuous-from-Ξ£ π C' =
record
{ index-of-approximating-family     = Ξ» x β prβ (C' x)
; approximating-family              = Ξ» x β prβ (prβ (C' x))
; approximating-family-is-directed  = Ξ» x β prβ (prβ (prβ (prβ (C' x))))
; approximating-family-is-way-below = Ξ» x β prβ (prβ (prβ (C' x)))
; approximating-family-β-οΌ          = Ξ» x β prβ (prβ (prβ (prβ (C' x))))
}

structurally-continuous-β : (π : DCPO {π€} {π£})
β structurally-continuous π
β structurally-continuous-Ξ£ π
structurally-continuous-β π = qinveq (structurally-continuous-to-Ξ£ π)
((structurally-continuous-from-Ξ£ π) ,
((Ξ» x β refl) , (Ξ» x β refl)))

\end{code}

In "Continuous categories and exponentiable toposes", Peter Johnstone and AndrΓ©
Joyal show in Lemma 2.1 that a dcpo D is continuous if and only if the map
β : Ind(D) β D that takes a directed family in the Ind-completion of D to its
supremum has a (specified) left adjoint.

We show that the type expressing that the β-map has a left adjoint is equivalent
to the type expressing structural continuity of D.

The proof below is fairly short, but only because we already characterized when
β-map has a left adjoint in IndCompletion.lagda.

\begin{code}

module _
(π : DCPO {π€} {π£})
where

open Ind-completion π

β structurally-continuous π
record
{ index-of-approximating-family     = Ξ» x β prβ (L x)
; approximating-family              = Ξ» x β prβ (prβ (L x))
; approximating-family-is-directed  = Ξ» x β prβ (prβ (L x))
; approximating-family-is-way-below = Ξ» x β prβ (L-is-approximating x)
; approximating-family-β-οΌ          = Ξ» x β prβ (L-is-approximating x)
}
where
L-is-approximating : is-approximating L

structurally-continuous π
where
open structurally-continuous C
L : β¨ π β© β Ind
L x = index-of-approximating-family x
, approximating-family x
, approximating-family-is-directed x
L-is-left-adjoint x Ο@(I , Ξ± , Ξ΄) = β¦1β¦ , β¦2β¦
where
β¦1β¦ : L x β² (I , Ξ± , Ξ΄) β x ββ¨ π β© β π Ξ΄
β¦1β¦ Lx-cofinal-in-Ξ± = transport (Ξ» - β - ββ¨ π β© β π Ξ΄)
(approximating-family-β-οΌ x)
(β²-to-β-of-β (approximating-family-is-directed x)
Ξ΄ Lx-cofinal-in-Ξ±)
β¦2β¦ : x ββ¨ π β© β π Ξ΄ β L x β² (I , Ξ± , Ξ΄)
β¦2β¦ x-below-βΞ± j = approximating-family-is-way-below x j I Ξ± Ξ΄ x-below-βΞ±

specified-left-adjoint-structurally-continuous-β = qinveq f (g , Ο , Ο)
where
Ο : g β f βΌ id
Ο : f β g βΌ id
Ο C = f (g C)         οΌβ¨ refl β©
Ο (Ο (f (g C))) οΌβ¨ h    β©
Ο (Ο C)         οΌβ¨ refl β©
C               β
where
Ο : structurally-continuous-Ξ£ π β structurally-continuous π
Ο = structurally-continuous-from-Ξ£ π
Ο : structurally-continuous π β structurally-continuous-Ξ£ π
Ο = structurally-continuous-to-Ξ£ π
h = ap Ο (dfunext fe
(Ξ» x β to-Ξ£-οΌ (refl , (to-Ξ£-οΌ (refl ,
(to-Γ-οΌ refl  (to-Ξ£-οΌ (refl , (sethood π _ _)))))))))

\end{code}

It follows immediately that a dcpo is continuous if and only if β-map has an

\begin{code}

module _
(π : DCPO {π€} {π£})
where

open Ind-completion π

β-map-has-unspecified-left-adjoint : π₯ βΊ β π€ β π£ Μ

\end{code}

Finall, we consider pseudocontinuity. It is similar to structural continuity,
but instead of asking that for every x : D, we have a specified directed family
approximating x, we merely ask there exists an unspecified directed family
approximating x.

On first sight, pseudocontinuity is arguably how one would expect us to define
contuinity of a dcpo while ensuring the notion is property as opposed to
structure. It is however weaker than continuity (as defined in
Continuity.lagda) and structural continuity. More importantly, with
pseudocontinuity we would need some instances of the axiom of choice when
proving the interpolation properties for the way-below relation, at least when
trying to mimick the proof in Continuity.lagda.

\begin{code}

is-pseudocontinuous-dcpo : (π : DCPO {π€} {π£}) β π₯ βΊ β π€ β π£ Μ
is-pseudocontinuous-dcpo π =
β β₯ Ξ£ I κ π₯ Μ  , Ξ£ Ξ± κ (I β β¨ π β©) , (is-way-upperbound π x Ξ±)
Γ (Ξ£ Ξ΄ κ is-Directed π Ξ± , β π Ξ΄ οΌ x) β₯

being-pseudocontinuous-dcpo-is-prop : (π : DCPO {π€} {π£})
β is-prop (is-pseudocontinuous-dcpo π)
being-pseudocontinuous-dcpo-is-prop π = Ξ -is-prop fe (Ξ» x β β₯β₯-is-prop)

continuous-dcpo-hierarchyβ : (π : DCPO {π€} {π£})
β structurally-continuous π
β is-continuous-dcpo π
continuous-dcpo-hierarchyβ π = β£_β£

continuous-dcpo-hierarchyβ : (π : DCPO {π€} {π£})
β is-continuous-dcpo π
β is-pseudocontinuous-dcpo π
continuous-dcpo-hierarchyβ π c x =
β₯β₯-functor (Ξ» C β structurally-continuous-to-Ξ£ π C x) c

\end{code}

Of course, one way to obtain a propositional-valued definition of continuity is
to ensure that we're asking for left adjoints between posets. That is, we take
the poset reflection Ind/β of Ind and ask that β-map/ : Ind/β β D has a left

We show that this is exactly the same as pseudocontinuity. This also illustrates
the discussion above on the need for the axiom of choice, as it boils down to
choosing representatives of equivalence classes.

\begin{code}

module _
(pe : Prop-Ext)
(π : DCPO {π€} {π£})
where

open import Quotient.Type
open import Quotient.Large pt fe pe
open general-set-quotients-exist large-set-quotients

open Ind-completion π
open Ind-completion-poset-reflection pe π

β-β-map/-lemma : {x : β¨ π β©} {Ο : Ind}
β (x ββ¨ π β© β-map Ο) β (x ββ¨ π β© β-map/ (Ξ· Ο))
β-β-map/-lemma {x} {Ο} = transport (Ξ» - β x ββ¨ π β© -) ((β-map/-triangle Ο) β»ΒΉ)
, transport (Ξ» - β x ββ¨ π β© -) (β-map/-triangle Ο)

where
module construction (x : β¨ π β©) where
str-cont : π₯ βΊ β π€ β π£ Μ
str-cont = (Ξ£ I κ π₯ Μ  , Ξ£ Ξ± κ (I β β¨ π β©)
, is-way-upperbound π x Ξ±
Γ (Ξ£ Ξ΄ κ is-Directed π Ξ± , β π Ξ΄ οΌ x))
ΞΊ : str-cont β Ind
ΞΊ (I , Ξ± , _ , (Ξ΄ , _)) = I , Ξ± , Ξ΄
ΞΊ-gives-approximating-family : (Ο : str-cont) β ΞΊ Ο approximates x
ΞΊ-gives-approximating-family (I , Ξ± , Ξ±-wb-x , (Ξ΄ , βΞ±-is-x)) =
βΞ±-is-x , Ξ±-wb-x

ladj : (Ο : str-cont) (Ο : Ind) β (ΞΊ Ο β² Ο) β (x ββ¨ π β© β-map Ο)
(ΞΊ Ο) x (ΞΊ-gives-approximating-family Ο) Ο

ΞΊ/ : str-cont β Ind/β
ΞΊ/ = Ξ· β ΞΊ
ΞΊ/-wconstant : wconstant ΞΊ/
ΞΊ/-wconstant Ο@(I , Ξ± , Ξ±-way-below-x , (Ξ΄ , x-sup-of-Ξ±))
Ο@(J , Ξ² , Ξ²-way-below-x , (Ξ΅ , x-sup-of-Ξ²)) =
β€-is-antisymmetric (ΞΊ/ Ο) (ΞΊ/ Ο)
(Ξ·-preserves-order (Ξ» i β Ξ±-way-below-x i J Ξ² Ξ΅ (οΌ-to-β π x-sup-of-Ξ²)))
(Ξ·-preserves-order (Ξ» j β Ξ²-way-below-x j I Ξ± Ξ΄ (οΌ-to-β π x-sup-of-Ξ±)))

Ο : Ξ£ Ο κ (β₯ str-cont β₯ β Ind/β) , ΞΊ/ βΌ Ο β β£_β£
Ο = wconstant-map-to-set-factors-through-truncation-of-domain
Ind/β-is-set ΞΊ/ ΞΊ/-wconstant

L : β¨ π β© β Ind/β
L x = prβ Ο (pc x)
where
open construction x

where
open construction x
β is-prop ((L x β€ Ο') β (x ββ¨ π β© β-map/ Ο'))
(Γ-is-prop (Ξ -is-prop fe (Ξ» _ β prop-valuedness π x (β-map/ Ο')))
(Ξ -is-prop fe (Ξ» _ β β€-is-prop-valued (L x) Ο')))
lemma : (Ο : str-cont) (Ο' : Ind/β) β ((L x β€ Ο') β (x ββ¨ π β© β-map/ Ο'))
where
β (L x β€ Ξ· Ο) β (x ββ¨ π β© β-map/ (Ξ· Ο))
L-is-ladj' Ο = β-trans β¦1β¦ β¦2β¦
where
β¦2β¦ : (ΞΊ Ο β² Ο) β (x ββ¨ π β© β-map/ (Ξ· Ο))
β¦2β¦ = β-trans (ladj Ο Ο) (β-β-map/-lemma)
β¦1β¦ : (L x β€ Ξ· Ο) β (ΞΊ Ο β² Ο)
β¦1β¦ = β-trans s (β-sym Ξ·-β-order)
where
s : (L x β€ Ξ· Ο) β (Ξ· (ΞΊ Ο) β€ Ξ· Ο)
s = transport (_β€ Ξ· Ο) e , transport (_β€ Ξ· Ο) (e β»ΒΉ)
where
e : L x οΌ Ξ· (ΞΊ Ο)
e = L x          οΌβ¨ refl                                 β©
prβ Ο (pc x) οΌβ¨ ap (prβ Ο) (β₯β₯-is-prop (pc x) β£ Ο β£) β©
prβ Ο β£ Ο β£  οΌβ¨ (prβ Ο Ο) β»ΒΉ                         β©
Ξ· (ΞΊ Ο)      β

β is-pseudocontinuous-dcpo π
β₯β₯-functor lemma (Ξ·-is-surjection (L x))
where
lemma : (Ξ£ Ο κ Ind , Ξ· Ο οΌ L x)
β Ξ£ I κ π₯ Μ  , Ξ£ Ξ± κ (I β β¨ π β©) , is-way-upperbound π x Ξ±
Γ (Ξ£ Ξ΄ κ is-Directed π Ξ± , β π Ξ΄ οΌ x)
lemma (Ο@(I , Ξ± , Ξ΄) , e) = I , Ξ± , prβ approx , (Ξ΄ , prβ approx)
where
ladj : (Ο : Ind) β (Ο β² Ο) β (x ββ¨ π β© β-map Ο)
where
ladj' : (Ξ· Ο β€ Ξ· Ο) β xΒ ββ¨ π β© β-map/ (Ξ· Ο)
ladj' = transport (Ξ» - β (- β€ Ξ· Ο) β x ββ¨ π β© β-map/ (Ξ· Ο)) (e β»ΒΉ)
approx : (β π Ξ΄ οΌ x) Γ is-way-upperbound π x Ξ±