Tom de Jong, January 2020.

December 2021: Added material on semidirected and subsingleton suprema.
June 2022: Refactored and moved some material around to/from other files.

A collection of various useful definitions and facts on directed complete posets
and Scott continuous maps between them.

Table of contents
 * Lemmas for establishing Scott continuity of maps between dcpos.
 * Continuity of basic functions (constant functions, identity, composition).
 * Definitions of isomorphisms of dcpos, continuous retracts and
   embedding-projection pairs.
 * Defining local smallness for dcpos and showing it is preserved by continuous
   retracts.
 * Lemmas involving (joins of) cofinal directed families.
 * Reindexing directed families.
 * Suprema of Ο‰-chains (added 23 June 2024).
 * Subdcpo induced by a subset/property (added 18th Feb 2024 by Martin Escardo).

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc

module DomainTheory.Basics.Miscelanea
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (π“₯ : Universe)
       where

private
 fe' : FunExt
 fe' _ _ = fe

open PropositionalTruncation pt

open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Size hiding (is-small ; is-locally-small)
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UniverseEmbedding

open import DomainTheory.Basics.Dcpo pt fe π“₯

\end{code}

Some preliminary basic lemmas.

\begin{code}

∐-is-monotone : (𝓓 : DCPO {𝓀} {𝓣}) {I : π“₯ Μ‡ } {Ξ± Ξ² : I β†’ ⟨ 𝓓 ⟩}
                (Ξ΄ : is-Directed 𝓓 Ξ±) (Ξ΅ : is-Directed 𝓓 Ξ²)
              β†’ ((i : I) β†’ Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² i)
              β†’ ∐ 𝓓 Ξ΄ βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΅
∐-is-monotone 𝓓 {I} {Ξ±} {Ξ²} Ξ΄ Ξ΅ l = ∐-is-lowerbound-of-upperbounds 𝓓 Ξ΄ (∐ 𝓓 Ξ΅) Ξ³
 where
  Ξ³ : (i : I) β†’ Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΅
  Ξ³ i = Ξ± i   βŠ‘βŸ¨ 𝓓 ⟩[ l i ]
        Ξ² i   βŠ‘βŸ¨ 𝓓 ⟩[ ∐-is-upperbound 𝓓 Ξ΅ i ]
        ∐ 𝓓 Ξ΅ ∎⟨ 𝓓 ⟩

∐-independent-of-directedness-witness : (𝓓 : DCPO {𝓀} {𝓣})
                                        {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                                        (Ξ΄ Ξ΅ : is-Directed 𝓓 Ξ±)
                                      β†’ ∐ 𝓓 Ξ΄ = ∐ 𝓓 Ξ΅
∐-independent-of-directedness-witness 𝓓 {I} {Ξ±} Ξ΄ Ξ΅ = ap (∐ 𝓓) p
 where
  p : δ = Ρ
  p = being-directed-is-prop (underlying-order 𝓓) Ξ± Ξ΄ Ξ΅

∐-family-= : (𝓓 : DCPO {𝓀} {𝓣}) {I : π“₯ Μ‡ } {Ξ± Ξ² : I β†’ ⟨ 𝓓 ⟩}
             (p : Ξ± = Ξ²) (Ξ΄ : is-Directed 𝓓 Ξ±)
           β†’ ∐ 𝓓 {I} {Ξ±} Ξ΄ = ∐ 𝓓 {I} {Ξ²} (transport (is-Directed 𝓓) p Ξ΄)
∐-family-= 𝓓 {I} {Ξ±} {Ξ±} refl Ξ΄ = refl

∐-family-=' : (𝓓 : DCPO {𝓀} {𝓣}) {I : π“₯ Μ‡ } {Ξ± Ξ² : I β†’ ⟨ 𝓓 ⟩}
              (h : Ξ± ∼ Ξ²) (Ξ΄ : is-Directed 𝓓 Ξ±) (Ξ΅ : is-Directed 𝓓 Ξ²)
            β†’ ∐ 𝓓 {I} {Ξ±} Ξ΄ = ∐ 𝓓 {I} {Ξ²} Ξ΅
∐-family-=' 𝓓 {I} {Ξ±} {Ξ²} h Ξ΄ Ξ΅ =
 ∐-family-= 𝓓 (dfunext fe h) Ξ΄ βˆ™ ∐-independent-of-directedness-witness 𝓓 _ Ξ΅

to-continuous-function-= : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                           {f g : DCPO[ 𝓓 , 𝓔 ]}
                         β†’ [ 𝓓 , 𝓔 ]⟨ f ⟩ ∼ [ 𝓓 , 𝓔 ]⟨ g ⟩
                         β†’ f = g
to-continuous-function-= 𝓓 𝓔 h =
 to-subtype-= (being-continuous-is-prop 𝓓 𝓔) (dfunext fe h)

=-to-βŠ‘ : (𝓓 : DCPO {𝓀} {𝓣}) {x y : ⟨ 𝓓 ⟩} β†’ x = y β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
=-to-βŠ‘ 𝓓 {x} {x} refl = reflexivity 𝓓 x

=-to-βŠ’ : (𝓓 : DCPO {𝓀} {𝓣}) {x y : ⟨ 𝓓 ⟩} β†’ y = x β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
=-to-βŠ’ 𝓓 p = =-to-βŠ‘ 𝓓 (p ⁻¹)

is-monotone : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
            β†’ (⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩) β†’ 𝓀 βŠ” 𝓣 βŠ” 𝓣' Μ‡
is-monotone 𝓓 𝓔 f = (x y : ⟨ 𝓓 ⟩) β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y β†’ f x βŠ‘βŸ¨ 𝓔 ⟩ f y

is-inflationary : (𝓓 : DCPO {𝓀} {𝓣})
                β†’ (⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩) β†’ 𝓀 βŠ” 𝓣 Μ‡
is-inflationary 𝓓 f = (x : ⟨ 𝓓 ⟩) β†’ x βŠ‘βŸ¨ 𝓓 ⟩ f x

\end{code}

Lemmas for establishing Scott continuity of maps between dcpos.

\begin{code}

image-is-directed : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                    {f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩}
                  β†’ is-monotone 𝓓 𝓔 f
                  β†’ {I : π“₯ Μ‡ }
                  β†’ {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                  β†’ is-Directed 𝓓 Ξ±
                  β†’ is-Directed 𝓔 (f ∘ Ξ±)
image-is-directed 𝓓 𝓔 {f} m {I} {Ξ±} Ξ΄ =
 inhabited-if-Directed 𝓓 Ξ± Ξ΄ , Ξ³
  where
   Ξ³ : is-semidirected (underlying-order 𝓔) (f ∘ Ξ±)
   Ξ³ i j = βˆ₯βˆ₯-functor (Ξ» (k , u , v) β†’ k , m (Ξ± i) (Ξ± k) u , m (Ξ± j) (Ξ± k) v)
                      (semidirected-if-Directed 𝓓 Ξ± Ξ΄ i j)

continuity-criterion : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                       (f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩)
                     β†’ (m : is-monotone 𝓓 𝓔 f)
                     β†’ ((I : π“₯ Μ‡ )
                        (Ξ± : I β†’ ⟨ 𝓓 ⟩)
                        (Ξ΄ : is-Directed 𝓓 Ξ±)
                     β†’ f (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ ∐ 𝓔 (image-is-directed 𝓓 𝓔 m Ξ΄))
                     β†’ is-continuous 𝓓 𝓔 f
continuity-criterion 𝓓 𝓔 f m e I Ξ± Ξ΄ = ub , lb-of-ubs
 where
  ub : (i : I) β†’ f (Ξ± i) βŠ‘βŸ¨ 𝓔 ⟩ f (∐ 𝓓 Ξ΄)
  ub i = m (Ξ± i) (∐ 𝓓 Ξ΄) (∐-is-upperbound 𝓓 Ξ΄ i)
  Ξ΅ : is-Directed 𝓔 (f ∘ Ξ±)
  Ξ΅ = image-is-directed 𝓓 𝓔 m Ξ΄
  lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order 𝓔)
              (f (∐ 𝓓 Ξ΄)) (f ∘ Ξ±)
  lb-of-ubs y u = f (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩[ e I Ξ± Ξ΄  ]
                  ∐ 𝓔 Ξ΅     βŠ‘βŸ¨ 𝓔 ⟩[ ∐-is-lowerbound-of-upperbounds 𝓔 Ξ΅ y u ]
                  y         ∎⟨ 𝓔 ⟩

continuity-criterion' : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                        (f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩)
                      β†’ (m : is-monotone 𝓓 𝓔 f)
                      β†’ ((I : π“₯ Μ‡ )
                         (Ξ± : I β†’ ⟨ 𝓓 ⟩)
                         (Ξ΄ : is-Directed 𝓓 Ξ±)
                      β†’ is-lowerbound-of-upperbounds (underlying-order 𝓔)
                                                     (f (∐ 𝓓 Ξ΄)) (f ∘ Ξ±))
                      β†’ is-continuous 𝓓 𝓔 f
continuity-criterion' 𝓓 𝓔 f m lb I Ξ± Ξ΄ = ub , lb I Ξ± Ξ΄
 where
  ub : (i : I) β†’ f (Ξ± i) βŠ‘βŸ¨ 𝓔 ⟩ f (∐ 𝓓 Ξ΄)
  ub i = m (Ξ± i) (∐ 𝓓 Ξ΄) (∐-is-upperbound 𝓓 Ξ΄ i)

monotone-if-continuous : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                         (f : DCPO[ 𝓓 , 𝓔 ])
                       β†’ is-monotone 𝓓 𝓔 [ 𝓓 , 𝓔 ]⟨ f ⟩
monotone-if-continuous 𝓓 𝓔 (f , cts) x y l = Ξ³
  where
   Ξ± : πŸ™ {π“₯} + πŸ™ {π“₯} β†’ ⟨ 𝓓 ⟩
   Ξ± (inl *) = x
   Ξ± (inr *) = y
   Ξ΄ : is-Directed 𝓓 Ξ±
   Ξ΄ = (∣ inl ⋆ ∣ , Ξ΅)
    where
     Ξ΅ : (i j : πŸ™ + πŸ™) β†’ βˆƒ k κž‰ πŸ™ + πŸ™ , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k Γ— Ξ± j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± k
     Ξ΅ (inl ⋆) (inl ⋆) = ∣ inr ⋆ , l , l ∣
     Ξ΅ (inl ⋆) (inr ⋆) = ∣ inr ⋆ , l , reflexivity 𝓓 y ∣
     Ξ΅ (inr ⋆) (inl ⋆) = ∣ inr ⋆ , reflexivity 𝓓 y , l ∣
     Ξ΅ (inr ⋆) (inr ⋆) = ∣ inr ⋆ , reflexivity 𝓓 y , reflexivity 𝓓 y ∣
   a : y = ∐ 𝓓 Ξ΄
   a = antisymmetry 𝓓 y (∐ 𝓓 Ξ΄)
           (∐-is-upperbound 𝓓 Ξ΄ (inr ⋆))
           (∐-is-lowerbound-of-upperbounds 𝓓 Ξ΄ y h)
    where
     h : (i : πŸ™ + πŸ™) β†’ Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ y
     h (inl ⋆) = l
     h (inr ⋆) = reflexivity 𝓓 y
   b : is-sup (underlying-order 𝓔) (f y) (f ∘ Ξ±)
   b = transport (Ξ» - β†’ is-sup (underlying-order 𝓔) - (f ∘ Ξ±)) (ap f (a ⁻¹))
       (cts (πŸ™ + πŸ™) Ξ± Ξ΄)
   Ξ³ : f x βŠ‘βŸ¨ 𝓔 ⟩ f y
   Ξ³ = sup-is-upperbound (underlying-order 𝓔) b (inl ⋆)

image-is-directed' : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                     (f : DCPO[ 𝓓 , 𝓔 ]) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                   β†’ is-Directed 𝓓 Ξ±
                   β†’ is-Directed 𝓔 ([ 𝓓 , 𝓔 ]⟨ f ⟩ ∘ Ξ±)
image-is-directed' 𝓓 𝓔 f {I} {Ξ±} Ξ΄ = image-is-directed 𝓓 𝓔 m Ξ΄
 where
  m : is-monotone 𝓓 𝓔 [ 𝓓 , 𝓔 ]⟨ f ⟩
  m = monotone-if-continuous 𝓓 𝓔 f

continuous-∐-βŠ‘ : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                 (f : DCPO[ 𝓓 , 𝓔 ]) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                 (Ξ΄ : is-Directed 𝓓 Ξ±)
               β†’ [ 𝓓 , 𝓔 ]⟨ f ⟩ (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ ∐ 𝓔 (image-is-directed' 𝓓 𝓔 f Ξ΄)
continuous-∐-βŠ‘ 𝓓 𝓔 (f , c) {I} {Ξ±} Ξ΄ =
 sup-is-lowerbound-of-upperbounds (underlying-order 𝓔) (c I Ξ± Ξ΄) (∐ 𝓔 Ξ΅) u
  where
   Ξ΅ : is-Directed 𝓔 (f ∘ Ξ±)
   Ξ΅ = image-is-directed' 𝓓 𝓔 (f , c) Ξ΄
   u : is-upperbound (underlying-order 𝓔) (∐ 𝓔 Ξ΅) (f ∘ Ξ±)
   u = ∐-is-upperbound 𝓔 Ξ΅

continuous-∐-βŠ’ : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                 (f : DCPO[ 𝓓 , 𝓔 ]) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                 (Ξ΄ : is-Directed 𝓓 Ξ±)
               β†’ ∐ 𝓔 (image-is-directed' 𝓓 𝓔 f Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ [ 𝓓 , 𝓔 ]⟨ f ⟩ (∐ 𝓓 Ξ΄)
continuous-∐-βŠ’ 𝓓 𝓔 (f , c) {I} {Ξ±} Ξ΄ =
 ∐-is-lowerbound-of-upperbounds 𝓔 Ξ΅ (f (∐ 𝓓 Ξ΄)) u
  where
   Ξ΅ : is-Directed 𝓔 (f ∘ Ξ±)
   Ξ΅ = image-is-directed' 𝓓 𝓔 (f , c) Ξ΄
   u : (i : I) β†’ f (Ξ± i) βŠ‘βŸ¨ 𝓔 ⟩ f (∐ 𝓓 Ξ΄)
   u i = sup-is-upperbound (underlying-order 𝓔) (c I Ξ± Ξ΄) i

continuous-∐-= : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                 (f : DCPO[ 𝓓 , 𝓔 ]) {I : π“₯ Μ‡ } {Ξ± : I β†’ ⟨ 𝓓 ⟩}
                 (Ξ΄ : is-Directed 𝓓 Ξ±)
               β†’ [ 𝓓 , 𝓔 ]⟨ f ⟩ (∐ 𝓓 Ξ΄) = ∐ 𝓔 (image-is-directed' 𝓓 𝓔 f Ξ΄)
continuous-∐-= 𝓓 𝓔 (f , c) {I} {Ξ±} Ξ΄ =
 antisymmetry 𝓔 (f (∐ 𝓓 Ξ΄)) (∐ 𝓔 Ξ΅) a b
  where
   Ξ΅ : is-Directed 𝓔 (f ∘ Ξ±)
   Ξ΅ = image-is-directed' 𝓓 𝓔 (f , c) Ξ΄
   a : f (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ ∐ 𝓔 Ξ΅
   a = continuous-∐-βŠ‘ 𝓓 𝓔 (f , c) Ξ΄
   b : ∐ 𝓔 Ξ΅ βŠ‘βŸ¨ 𝓔 ⟩ f (∐ 𝓓 Ξ΄)
   b = continuous-∐-βŠ’ 𝓓 𝓔 (f , c) Ξ΄

\end{code}

Continuity of basic functions (constant functions, identity, composition).

\begin{code}

constant-functions-are-continuous : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                                    {e : ⟨ 𝓔 ⟩} β†’ is-continuous 𝓓 𝓔 (Ξ» d β†’ e)
constant-functions-are-continuous 𝓓 𝓔 {e} I Ξ± Ξ΄ = u , v
 where
  u : (i : I) β†’ e βŠ‘βŸ¨ 𝓔 ⟩ e
  u i = reflexivity 𝓔 e
  v : (y : ⟨ 𝓔 ⟩) β†’ ((i : I) β†’ e βŠ‘βŸ¨ 𝓔 ⟩ y) β†’ e βŠ‘βŸ¨ 𝓔 ⟩ y
  v y l  = βˆ₯βˆ₯-rec (prop-valuedness 𝓔 e y) l (inhabited-if-Directed 𝓓 Ξ± Ξ΄)

id-is-monotone : (𝓓 : DCPO {𝓀} {𝓣}) β†’ is-monotone 𝓓 𝓓 id
id-is-monotone 𝓓 x y l = l

id-is-inflationary : (𝓓 : DCPO {𝓀} {𝓣}) β†’ is-inflationary 𝓓 id
id-is-inflationary = reflexivity

id-is-continuous : (𝓓 : DCPO {𝓀} {𝓣}) β†’ is-continuous 𝓓 𝓓 id
id-is-continuous 𝓓 = continuity-criterion 𝓓 𝓓 id (id-is-monotone 𝓓) Ξ³
 where
  Ξ³ : (I : π“₯ Μ‡ )(Ξ± : I β†’ ⟨ 𝓓 ⟩) (Ξ΄ : is-Directed 𝓓 Ξ±)
    β†’ ∐ 𝓓 Ξ΄ βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 (image-is-directed 𝓓 𝓓 (Ξ» x y l β†’ l) Ξ΄)
  Ξ³ I Ξ± Ξ΄ = =-to-βŠ‘ 𝓓 (∐-independent-of-directedness-witness 𝓓
             Ξ΄ (image-is-directed 𝓓 𝓓 (Ξ» x y l β†’ l) Ξ΄))

∘-is-monotone : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'}) (𝓔' : DCPO {𝓦} {𝓦'})
                  (f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩) (g : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓔' ⟩)
                β†’ is-monotone 𝓓 𝓔 f
                β†’ is-monotone 𝓔 𝓔' g
                β†’ is-monotone 𝓓 𝓔' (g ∘ f)
∘-is-monotone 𝓓 𝓔 𝓔' f g mf mg x y l = mg (f x) (f y) (mf x y l)

∘-is-inflationary : (𝓓 : DCPO {𝓀} {𝓣})
                  (f g : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩)
                β†’ is-inflationary 𝓓 f
                β†’ is-inflationary 𝓓 g
                β†’ is-inflationary 𝓓 (g ∘ f)
∘-is-inflationary 𝓓 f g if ig x = transitivity 𝓓 x (f x) (g (f x)) (if x) (ig (f x))

∘-is-continuous : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'}) (𝓔' : DCPO {𝓦} {𝓦'})
                  (f : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩) (g : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓔' ⟩)
                β†’ is-continuous 𝓓 𝓔 f
                β†’ is-continuous 𝓔 𝓔' g
                β†’ is-continuous 𝓓 𝓔' (g ∘ f)
∘-is-continuous 𝓓 𝓔 𝓔' f g cf cg = continuity-criterion 𝓓 𝓔' (g ∘ f) m ψ
 where
  mf : is-monotone 𝓓 𝓔 f
  mf = monotone-if-continuous 𝓓 𝓔 (f , cf)
  mg : is-monotone 𝓔 𝓔' g
  mg = monotone-if-continuous 𝓔 𝓔' (g , cg)
  m : is-monotone 𝓓 𝓔' (g ∘ f)
  m = ∘-is-monotone 𝓓 𝓔 𝓔' f g mf mg
  ψ : (I : π“₯ Μ‡ )(Ξ± : I β†’ ⟨ 𝓓 ⟩) (Ξ΄ : is-Directed 𝓓 Ξ±)
    β†’ g (f (∐ 𝓓 Ξ΄)) βŠ‘βŸ¨ 𝓔' ⟩ ∐ 𝓔' (image-is-directed 𝓓 𝓔' m Ξ΄)
  ψ I Ξ± Ξ΄ = g (f (∐ 𝓓 Ξ΄)) βŠ‘βŸ¨ 𝓔' ⟩[ l₁ ]
            g (∐ 𝓔 Ξ΅f)    βŠ‘βŸ¨ 𝓔' ⟩[ lβ‚‚ ]
            ∐ 𝓔' Ξ΅g       βŠ‘βŸ¨ 𝓔' ⟩[ l₃ ]
            ∐ 𝓔' Ξ΅        ∎⟨ 𝓔' ⟩
   where
    Ξ΅ : is-Directed 𝓔' (g ∘ f ∘ Ξ±)
    Ξ΅ = image-is-directed 𝓓 𝓔' m Ξ΄
    Ξ΅f : is-Directed 𝓔 (f ∘ Ξ±)
    Ξ΅f = image-is-directed' 𝓓 𝓔 (f , cf) Ξ΄
    Ξ΅g : is-Directed 𝓔' (g ∘ f ∘ Ξ±)
    Ξ΅g = image-is-directed' 𝓔 𝓔' (g , cg) Ξ΅f
    l₁ = mg (f (∐ 𝓓 Ξ΄)) (∐ 𝓔 Ξ΅f) h
     where
      h : f (∐ 𝓓 Ξ΄) βŠ‘βŸ¨ 𝓔 ⟩ ∐ 𝓔 Ξ΅f
      h = continuous-∐-βŠ‘ 𝓓 𝓔 (f , cf) Ξ΄
    lβ‚‚ = continuous-∐-βŠ‘ 𝓔 𝓔' (g , cg) Ξ΅f
    l₃ = =-to-βŠ‘ 𝓔' (∐-independent-of-directedness-witness 𝓔' Ξ΅g Ξ΅)

∘-is-continuous₃ : {𝓦₁ 𝓣₁ 𝓦₂ 𝓣₂ 𝓦₃ 𝓣₃ 𝓦₄ 𝓣₄ : Universe}
                   (𝓓₁ : DCPO {𝓦₁} {𝓣₁}) (𝓓₂ : DCPO {𝓦₂} {𝓣₂})
                   (𝓓₃ : DCPO {𝓦₃} {𝓣₃}) (𝓓₄ : DCPO {𝓦₄} {𝓣₄})
                   (f : ⟨ 𝓓₁ ⟩ β†’ ⟨ 𝓓₂ ⟩) (g : ⟨ 𝓓₂ ⟩ β†’ ⟨ 𝓓₃ ⟩)
                   (h : ⟨ 𝓓₃ ⟩ β†’ ⟨ 𝓓₄ ⟩)
                 β†’ is-continuous 𝓓₁ 𝓓₂ f
                 β†’ is-continuous 𝓓₂ 𝓓₃ g
                 β†’ is-continuous 𝓓₃ 𝓓₄ h
                 β†’ is-continuous 𝓓₁ 𝓓₄ (h ∘ g ∘ f)
∘-is-continuous₃ 𝓓₁ 𝓓₂ 𝓓₃ 𝓓₄ f g h cf cg ch =
 ∘-is-continuous 𝓓₁ 𝓓₂ 𝓓₄ f (h ∘ g) cf
                 (∘-is-continuous 𝓓₂ 𝓓₃ 𝓓₄ g h cg ch)

DCPO-∘ : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'}) (𝓔' : DCPO {𝓦} {𝓦'})
       β†’ DCPO[ 𝓓 , 𝓔 ] β†’ DCPO[ 𝓔 , 𝓔' ] β†’ DCPO[ 𝓓 , 𝓔' ]
DCPO-∘ 𝓓 𝓔 𝓔' (f , cf) (g , cg) = (g ∘ f) , (∘-is-continuous 𝓓 𝓔 𝓔' f g cf cg)

DCPO-βˆ˜β‚ƒ : {𝓦₁ 𝓣₁ 𝓦₂ 𝓣₂ 𝓦₃ 𝓣₃ 𝓦₄ 𝓣₄ : Universe}
          (𝓓₁ : DCPO {𝓦₁} {𝓣₁}) (𝓓₂ : DCPO {𝓦₂} {𝓣₂})
          (𝓓₃ : DCPO {𝓦₃} {𝓣₃}) (𝓓₄ : DCPO {𝓦₄} {𝓣₄})
          (f : DCPO[ 𝓓₁ , 𝓓₂ ]) (g : DCPO[ 𝓓₂ , 𝓓₃ ]) (h : DCPO[ 𝓓₃ , 𝓓₄ ])
        β†’ DCPO[ 𝓓₁ , 𝓓₄ ]
DCPO-βˆ˜β‚ƒ 𝓓₁ 𝓓₂ 𝓓₃ 𝓓₄ f g h = DCPO-∘ 𝓓₁ 𝓓₂ 𝓓₄ f (DCPO-∘ 𝓓₂ 𝓓₃ 𝓓₄ g h)

\end{code}

Defining isomorphisms of (pointed) dcpos.

\begin{code}

_β‰ƒα΅ˆαΆœα΅–α΅’_ : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'}) β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣' Μ‡
𝓓 β‰ƒα΅ˆαΆœα΅–α΅’ 𝓔 = Ξ£ f κž‰ (⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩) , Ξ£ g κž‰ (⟨ 𝓔 ⟩ β†’ ⟨ 𝓓 ⟩) ,
                ((d : ⟨ 𝓓 ⟩) β†’ g (f d) = d)
              Γ— ((e : ⟨ 𝓔 ⟩) β†’ f (g e) = e)
              Γ— is-continuous 𝓓 𝓔 f
              Γ— is-continuous 𝓔 𝓓 g

β‰ƒα΅ˆαΆœα΅–α΅’-inv : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
          β†’ 𝓓 β‰ƒα΅ˆαΆœα΅–α΅’ 𝓔
          β†’ 𝓔 β‰ƒα΅ˆαΆœα΅–α΅’ 𝓓
β‰ƒα΅ˆαΆœα΅–α΅’-inv 𝓓 𝓔 (f , g , s , r , cf , cg) = (g , f , r , s , cg , cf)

is-deflation : (𝓓 : DCPO {𝓀} {𝓣}) β†’ DCPO[ 𝓓 , 𝓓 ] β†’ 𝓀 βŠ” 𝓣 Μ‡
is-deflation 𝓓 f = (x : ⟨ 𝓓 ⟩) β†’ [ 𝓓 , 𝓓 ]⟨ f ⟩ x βŠ‘βŸ¨ 𝓓 ⟩ x

is-continuous-retract : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                      β†’ DCPO[ 𝓓 , 𝓔 ]
                      β†’ DCPO[ 𝓔 , 𝓓 ]
                      β†’ 𝓀 Μ‡
is-continuous-retract 𝓓 𝓔 (Οƒ , _) (ρ , _) = (x : ⟨ 𝓓 ⟩) β†’ ρ (Οƒ x) = x

is-embedding-projection-pair : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                             β†’ DCPO[ 𝓓 , 𝓔 ]
                             β†’ DCPO[ 𝓔 , 𝓓 ]
                             β†’ 𝓀 βŠ” 𝓀' βŠ” 𝓣' Μ‡
is-embedding-projection-pair 𝓓 𝓔 𝕀@(s , cs) 𝕣@(r , cr) =
   is-continuous-retract 𝓓 𝓔 𝕀 𝕣
 Γ— is-deflation 𝓔 (s ∘ r , ∘-is-continuous 𝓔 𝓓 𝓔 r s cr cs)

record _continuous-retract-of_
        (𝓓 : DCPO {𝓀} {𝓣})
        (𝓔 : DCPO {𝓀'} {𝓣'}) : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣' Μ‡  where
  field
   s : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩
   r : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓓 ⟩
   s-section-of-r : r ∘ s ∼ id
   s-is-continuous : is-continuous 𝓓 𝓔 s
   r-is-continuous : is-continuous 𝓔 𝓓 r

  𝕀 : DCPO[ 𝓓 , 𝓔 ]
  𝕀 = s , s-is-continuous

  𝕣 : DCPO[ 𝓔 , 𝓓 ]
  𝕣 = r , r-is-continuous

β‰ƒα΅ˆαΆœα΅–α΅’-to-continuous-retract : (𝓓 : DCPO {𝓀} {𝓣})
                              (𝓔 : DCPO {𝓀'} {𝓣'})
                            β†’ 𝓓 β‰ƒα΅ˆαΆœα΅–α΅’ 𝓔
                            β†’ 𝓓 continuous-retract-of 𝓔
β‰ƒα΅ˆαΆœα΅–α΅’-to-continuous-retract 𝓓 𝓔 (f , g , s , r , cf , cg) =
 record
  { s = f
  ; r = g
  ; s-section-of-r = s
  ; s-is-continuous = cf
  ; r-is-continuous = cg
  }

is-embedding-projection : (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
                        β†’ DCPO[ 𝓓 , 𝓔 ]
                        β†’ DCPO[ 𝓔 , 𝓓 ]
                        β†’ 𝓀 βŠ” 𝓀' βŠ” 𝓣' Μ‡
is-embedding-projection 𝓓 𝓔 Ξ΅ Ο€ =
 is-continuous-retract 𝓓 𝓔 Ξ΅ Ο€ Γ— is-deflation 𝓔 (DCPO-∘ 𝓔 𝓓 𝓔 Ο€ Ξ΅)

record embedding-projection-pair-between
        (𝓓 : DCPO {𝓀} {𝓣})
        (𝓔 : DCPO {𝓀'} {𝓣'}) : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓀' βŠ” 𝓣' Μ‡  where
  field
   e : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓔 ⟩
   p : ⟨ 𝓔 ⟩ β†’ ⟨ 𝓓 ⟩
   e-section-of-p : p ∘ e ∼ id
   e-p-deflation : (y : ⟨ 𝓔 ⟩) β†’ e (p y) βŠ‘βŸ¨ 𝓔 ⟩ y
   e-is-continuous : is-continuous 𝓓 𝓔 e
   p-is-continuous : is-continuous 𝓔 𝓓 p

  𝕖 : DCPO[ 𝓓 , 𝓔 ]
  𝕖 = e , e-is-continuous

  𝕑 : DCPO[ 𝓔 , 𝓓 ]
  𝕑 = p , p-is-continuous

β‰ƒα΅ˆαΆœα΅–α΅’-to-embedding-projection-pair : (𝓓 : DCPO {𝓀} {𝓣})
                                     (𝓔 : DCPO {𝓀'} {𝓣'})
                                   β†’ 𝓓 β‰ƒα΅ˆαΆœα΅–α΅’ 𝓔
                                   β†’ embedding-projection-pair-between 𝓓 𝓔
β‰ƒα΅ˆαΆœα΅–α΅’-to-embedding-projection-pair 𝓓 𝓔 (f , g , s , r , cf , cg) =
 record
  { e = f
  ; p = g
  ; e-section-of-p = s
  ; e-p-deflation = Ξ» y β†’ =-to-βŠ‘ 𝓔 (r y)
  ; e-is-continuous = cf
  ; p-is-continuous = cg
  }

\end{code}

Many examples of dcpos conveniently happen to be locally small.

We present and prove the equivalence of three definitions:
- our main one, is-locally-small, which uses a record so that we have convenient
  helper functions;
- a second one, is-locally-small-Ξ£, which is like the above but uses a Ξ£-type
  rather than a record;
- a third one, is-locally-small', which arguably looks more like the familiar
  categorical notion of a locally small category.

To prove their equivalence, we prove a general lemma on small-valued binary
relations.

\begin{code}

is-small : (X : 𝓀 Μ‡ ) β†’ π“₯ ⁺ βŠ” 𝓀 Μ‡
is-small X = X is π“₯ small

small-binary-relation-equivalence : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {R : X β†’ Y β†’ 𝓣 Μ‡ }
                                  β†’ ((x : X) (y : Y) β†’ is-small (R x y))
                                  ≃ (Ξ£ Rβ‚› κž‰ (X β†’ Y β†’ π“₯ Μ‡ ) ,
                                      ((x : X) (y : Y) β†’ Rβ‚› x y ≃ R x y))
small-binary-relation-equivalence {𝓀} {𝓦} {𝓣} {X} {Y} {R} =
 ((x : X) (y : Y)    β†’ is-small (R x y))                            β‰ƒβŸ¨ I   ⟩
 ((((x , y) : X Γ— Y) β†’ is-small (R x y)))                           β‰ƒβŸ¨ II  ⟩
 (Ξ£ R' κž‰ (X Γ— Y β†’ π“₯ Μ‡ ) , (((x , y) : X Γ— Y) β†’ R' (x , y) ≃ R x y)) β‰ƒβŸ¨ III ⟩
 (Ξ£ R' κž‰ (X Γ— Y β†’ π“₯ Μ‡ ) , ((x : X) (y : Y) β†’ R' (x , y) ≃ R x y))   β‰ƒβŸ¨ IV  ⟩
 (Ξ£ Rβ‚› κž‰ (X β†’ Y β†’ π“₯ Μ‡ ) , ((x : X) (y : Y) β†’ Rβ‚› x y ≃ R x y))       β– 
  where
   Ο† : {𝓀 π“₯ 𝓦 : Universe}
       {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Z : (Ξ£ x κž‰ X , Y x) β†’ 𝓦 Μ‡ }
     β†’ Ξ  Z ≃ (Ξ  x κž‰ X , Ξ  y κž‰ Y x , Z (x , y))
   Ο† = curry-uncurry fe'
   I   = ≃-sym Ο†
   II  = Ξ Ξ£-distr-≃
   III = Ξ£-cong (Ξ» R β†’ Ο†)
   IV  = Ξ£-change-of-variable (Ξ» R' β†’ (x : X) (y : Y) β†’ R' x y ≃ R x y)
          ⌜ Ο† ⌝ (⌜⌝-is-equiv Ο†)

module _
        (𝓓 : DCPO {𝓀} {𝓣})
       where

 record is-locally-small : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡  where
  field
   _βŠ‘β‚›_ : ⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡
   βŠ‘β‚›-≃-βŠ‘ : {x y : ⟨ 𝓓 ⟩} β†’ x βŠ‘β‚› y ≃ x βŠ‘βŸ¨ 𝓓 ⟩ y

  βŠ‘β‚›-to-βŠ‘ : {x y : ⟨ 𝓓 ⟩} β†’ x βŠ‘β‚› y β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y
  βŠ‘β‚›-to-βŠ‘ = ⌜ βŠ‘β‚›-≃-βŠ‘ ⌝

  βŠ‘-to-βŠ‘β‚› : {x y : ⟨ 𝓓 ⟩} β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y β†’ x βŠ‘β‚› y
  βŠ‘-to-βŠ‘β‚› = ⌜ βŠ‘β‚›-≃-βŠ‘ ⌝⁻¹

  βŠ‘β‚›-is-prop-valued : (x y : ⟨ 𝓓 ⟩) β†’ is-prop (x βŠ‘β‚› y)
  βŠ‘β‚›-is-prop-valued x y = equiv-to-prop βŠ‘β‚›-≃-βŠ‘ (prop-valuedness 𝓓 x y)

  transitivityβ‚› : (x : ⟨ 𝓓 ⟩) {y z : ⟨ 𝓓 ⟩}
                β†’ x βŠ‘β‚› y β†’ y βŠ‘β‚› z β†’ x βŠ‘β‚› z
  transitivityβ‚› x {y} {z} u v = ⌜ βŠ‘β‚›-≃-βŠ‘ ⌝⁻¹
                                 (transitivity 𝓓 x y z
                                               (⌜ βŠ‘β‚›-≃-βŠ‘ ⌝ u)
                                               (⌜ βŠ‘β‚›-≃-βŠ‘ ⌝ v))

  syntax transitivityβ‚› x u v = x βŠ‘β‚›[ u ] v
  infixr 0 transitivityβ‚›

  reflexivityβ‚› : (x : ⟨ 𝓓 ⟩) β†’ x βŠ‘β‚› x
  reflexivityβ‚› x = ⌜ βŠ‘β‚›-≃-βŠ‘ ⌝⁻¹ (reflexivity 𝓓 x)

  syntax reflexivityβ‚› x = x βˆŽβ‚›
  infix 1 reflexivityβ‚›

\end{code}

This ends our helper function for the record and we proceed by giving the
alternative definitions of local smallness and proving their equivalence.

\begin{code}

 is-locally-small-Ξ£ : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-locally-small-Ξ£ =
   Ξ£ _βŠ‘β‚›_ κž‰ (⟨ 𝓓 ⟩ β†’ ⟨ 𝓓 ⟩ β†’ π“₯ Μ‡ ) , ((x y : ⟨ 𝓓 ⟩) β†’ (x βŠ‘β‚› y) ≃ (x βŠ‘βŸ¨ 𝓓 ⟩ y))

 is-locally-small-record-equivalence : is-locally-small ≃ is-locally-small-Ξ£
 is-locally-small-record-equivalence = qinveq f (g , (Ξ» _ β†’ refl) , (Ξ» _ β†’ refl))
  where
   f : is-locally-small β†’ is-locally-small-Ξ£
   f ls = _βŠ‘β‚›_ , (Ξ» x y β†’ βŠ‘β‚›-≃-βŠ‘)
    where
     open is-locally-small ls
   g : is-locally-small-Ξ£ β†’ is-locally-small
   g ls = record { _βŠ‘β‚›_ = pr₁ ls ; βŠ‘β‚›-≃-βŠ‘ = (Ξ» {x} {y} β†’ prβ‚‚ ls x y) }

 is-locally-small' : π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-locally-small' = (x y : ⟨ 𝓓 ⟩) β†’ is-small (x βŠ‘βŸ¨ 𝓓 ⟩ y)

 local-smallness-equivalent-definitions : is-locally-small ≃ is-locally-small'
 local-smallness-equivalent-definitions =
  is-locally-small-record-equivalence ● ≃-sym (small-binary-relation-equivalence)

 being-locally-small'-is-prop : PropExt β†’ is-prop is-locally-small'
 being-locally-small'-is-prop pe =
  Ξ β‚‚-is-prop fe (Ξ» x y β†’ prop-being-small-is-prop pe fe'
                          (x βŠ‘βŸ¨ 𝓓 ⟩ y) (prop-valuedness 𝓓 x y))

 being-locally-small-is-prop : PropExt β†’ is-prop is-locally-small
 being-locally-small-is-prop pe =
  equiv-to-prop local-smallness-equivalent-definitions
                (being-locally-small'-is-prop pe)

\end{code}

Being locally small is preserved by continuous retracts.

\begin{code}

local-smallness-preserved-by-continuous-retract :
   (𝓓 : DCPO {𝓀} {𝓣}) (𝓔 : DCPO {𝓀'} {𝓣'})
 β†’ 𝓓 continuous-retract-of 𝓔
 β†’ is-locally-small 𝓔
 β†’ is-locally-small 𝓓
local-smallness-preserved-by-continuous-retract 𝓓 𝓔 ρ ls =
 ⌜ local-smallness-equivalent-definitions 𝓓 ⌝⁻¹ Ξ³
  where
   open _continuous-retract-of_ ρ
   open is-locally-small ls
   Ξ³ : is-locally-small' 𝓓
   Ξ³ x y = (s x βŠ‘β‚› s y , g)
    where
     g : (s x βŠ‘β‚› s y) ≃ (x βŠ‘βŸ¨ 𝓓 ⟩ y)
     g = logically-equivalent-props-are-equivalent
          (equiv-to-prop βŠ‘β‚›-≃-βŠ‘
            (prop-valuedness 𝓔 (s x) (s y)))
          (prop-valuedness 𝓓 x y)
          ⦅⇒⦆ ⦅⇐⦆
      where
       ⦅⇒⦆ : (s x βŠ‘β‚› s y) β†’ (x βŠ‘βŸ¨ 𝓓 ⟩ y)
       ⦅⇒⦆ l = x      βŠ‘βŸ¨ 𝓓 ⟩[ β¦…1⦆ ]
              r (s x) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…2⦆ ]
              r (s y) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…3⦆ ]
              y       ∎⟨ 𝓓 ⟩
        where
         β¦…1⦆ = =-to-βŠ’ 𝓓 (s-section-of-r x)
         β¦…2⦆ = monotone-if-continuous 𝓔 𝓓 𝕣 (s x) (s y) (βŠ‘β‚›-to-βŠ‘ l)
         β¦…3⦆ = =-to-βŠ‘ 𝓓 (s-section-of-r y)
       ⦅⇐⦆ : (x βŠ‘βŸ¨ 𝓓 ⟩ y) β†’ (s x βŠ‘β‚› s y)
       ⦅⇐⦆ l = βŠ‘-to-βŠ‘β‚› (monotone-if-continuous 𝓓 𝓔 𝕀 x y l)

\end{code}

Moving on from local smallness, we present a few useful lemmas on cofinality and
(joins of) directed families.

\begin{code}

semidirected-if-bicofinal : (𝓓 : DCPO {𝓀} {𝓣}) {I J : 𝓦 Μ‡ }
                            (Ξ± : I β†’ ⟨ 𝓓 ⟩) (Ξ² : J β†’ ⟨ 𝓓 ⟩)
                          β†’ ((i : I) β†’ βˆƒ j κž‰ J , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
                          β†’ ((j : J) β†’ βˆƒ i κž‰ I , Ξ² j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
                          β†’ is-semidirected (underlying-order 𝓓) Ξ±
                          β†’ is-semidirected (underlying-order 𝓓) Ξ²
semidirected-if-bicofinal 𝓓 {I} {J} Ξ± Ξ² Ξ±-cofinal-in-Ξ² Ξ²-cofinal-in-Ξ± Οƒ j₁ jβ‚‚ =
 βˆ₯βˆ₯-recβ‚‚ βˆƒ-is-prop f (Ξ²-cofinal-in-Ξ± j₁) (Ξ²-cofinal-in-Ξ± jβ‚‚)
  where
   f : (Ξ£ i₁ κž‰ I , Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i₁)
     β†’ (Ξ£ iβ‚‚ κž‰ I , Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ± iβ‚‚)
     β†’ βˆƒ j κž‰ J , (Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j) Γ— (Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
   f (i₁ , u₁) (iβ‚‚ , uβ‚‚) = βˆ₯βˆ₯-rec βˆƒ-is-prop g (Οƒ i₁ iβ‚‚)
    where
     g : (Ξ£ i κž‰ I , (Ξ± i₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i) Γ— (Ξ± iβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i))
       β†’ (βˆƒ j κž‰ J , (Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j) Γ— (Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j))
     g (i , v₁ , vβ‚‚) = βˆ₯βˆ₯-functor h (Ξ±-cofinal-in-Ξ² i)
      where
       h : (Ξ£ j κž‰ J , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
         β†’ (Ξ£ j κž‰ J , (Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j) Γ— (Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j))
       h (j , w) = (j , (Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩[ u₁ ]
                         Ξ± i₁ βŠ‘βŸ¨ 𝓓 ⟩[ v₁ ]
                         Ξ± i  βŠ‘βŸ¨ 𝓓 ⟩[ w ]
                         Ξ² j  ∎⟨ 𝓓 ⟩)
                      , (Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩[ uβ‚‚ ]
                         Ξ± iβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩[ vβ‚‚ ]
                         Ξ± i  βŠ‘βŸ¨ 𝓓 ⟩[ w ]
                         Ξ² j  ∎⟨ 𝓓 ⟩))

directed-if-bicofinal : (𝓓 : DCPO {𝓀} {𝓣}) {I J : 𝓦 Μ‡ }
                        {Ξ± : I β†’ ⟨ 𝓓 ⟩} {Ξ² : J β†’ ⟨ 𝓓 ⟩}
                      β†’ ((i : I) β†’ βˆƒ j κž‰ J , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
                      β†’ ((j : J) β†’ βˆƒ i κž‰ I , Ξ² j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
                      β†’ is-Directed 𝓓 Ξ±
                      β†’ is-Directed 𝓓 Ξ²
directed-if-bicofinal 𝓓 {I} {J} {Ξ±} {Ξ²} κ₁ ΞΊβ‚‚ Ξ΄ =
 (Ξ³ , semidirected-if-bicofinal 𝓓 Ξ± Ξ² κ₁ ΞΊβ‚‚ (semidirected-if-Directed 𝓓 Ξ± Ξ΄))
  where
   Ξ³ : βˆ₯ J βˆ₯
   Ξ³ = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop Ο• (inhabited-if-Directed 𝓓 Ξ± Ξ΄)
    where
     Ο• : I β†’ βˆ₯ J βˆ₯
     Ο• i = βˆ₯βˆ₯-functor pr₁ (κ₁ i)

∐-βŠ‘-if-cofinal : (𝓓 : DCPO {𝓀} {𝓣}) {I J : π“₯ Μ‡ }
                 {Ξ± : I β†’ ⟨ 𝓓 ⟩} {Ξ² : J β†’ ⟨ 𝓓 ⟩}
               β†’ ((i : I) β†’ βˆƒ j κž‰ J , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
               β†’ (Ξ΄ : is-Directed 𝓓 Ξ±)
               β†’ (Ξ΅ : is-Directed 𝓓 Ξ²)
               β†’ ∐ 𝓓 Ξ΄ βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΅
∐-βŠ‘-if-cofinal 𝓓 {I} {J} {Ξ±} {Ξ²} Ξ±-cofinal-in-Ξ² Ξ΄ Ξ΅ =
 ∐-is-lowerbound-of-upperbounds 𝓓 Ξ΄ (∐ 𝓓 Ξ΅) Ξ³
  where
   Ξ³ : (i : I) β†’ Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΅
   Ξ³ i = βˆ₯βˆ₯-rec (prop-valuedness 𝓓 (Ξ± i) (∐ 𝓓 Ξ΅)) Ο• (Ξ±-cofinal-in-Ξ² i)
    where
     Ο• : (Ξ£ j κž‰ J , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
       β†’ Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ ∐ 𝓓 Ξ΅
     Ο• (j , u) = Ξ± i   βŠ‘βŸ¨ 𝓓 ⟩[ u ]
                 Ξ² j   βŠ‘βŸ¨ 𝓓 ⟩[ ∐-is-upperbound 𝓓 Ξ΅ j ]
                 ∐ 𝓓 Ξ΅ ∎⟨ 𝓓 ⟩

∐-=-if-bicofinal : (𝓓 : DCPO {𝓀} {𝓣}) {I J : π“₯ Μ‡ }
                   {Ξ± : I β†’ ⟨ 𝓓 ⟩} {Ξ² : J β†’ ⟨ 𝓓 ⟩}
                 β†’ ((i : I) β†’ βˆƒ j κž‰ J , Ξ± i βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j)
                 β†’ ((j : J) β†’ βˆƒ i κž‰ I , Ξ² j βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i)
                 β†’ (Ξ΄ : is-Directed 𝓓 Ξ±)
                 β†’ (Ξ΅ : is-Directed 𝓓 Ξ²)
                 β†’ ∐ 𝓓 Ξ΄ = ∐ 𝓓 Ξ΅
∐-=-if-bicofinal 𝓓 κ₁ ΞΊβ‚‚ Ξ΄ Ξ΅ =
 antisymmetry 𝓓 (∐ 𝓓 Ξ΄) (∐ 𝓓 Ξ΅) (∐-βŠ‘-if-cofinal 𝓓 κ₁ Ξ΄ Ξ΅)
                                (∐-βŠ‘-if-cofinal 𝓓 ΞΊβ‚‚ Ξ΅ Ξ΄)

\end{code}

Finally, we sometimes wish to reindex a directed family by another equivalent
type. The resulting family is of course directed again and has the same
supremum, which is what we prove here.

\begin{code}

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        {I : 𝓦 Μ‡ } {J : 𝓦' Μ‡ }
        (ρ : I ≃ J)
        (Ξ± : I β†’ ⟨ 𝓓 ⟩)
       where

 reindexed-family : J β†’ ⟨ 𝓓 ⟩
 reindexed-family = α ∘ ⌜ ρ ⌝⁻¹

 reindexed-family-is-directed : is-Directed 𝓓 Ξ±
                              β†’ is-Directed 𝓓 reindexed-family
 reindexed-family-is-directed Ξ΄ = J-inh , Ξ²-semidirected
  where
   J-inh : βˆ₯ J βˆ₯
   J-inh = βˆ₯βˆ₯-functor ⌜ ρ ⌝ (inhabited-if-Directed 𝓓 Ξ± Ξ΄)
   Ξ² : J β†’ ⟨ 𝓓 ⟩
   Ξ² = reindexed-family
   Ξ²-semidirected : is-semidirected (underlying-order 𝓓) Ξ²
   Ξ²-semidirected j₁ jβ‚‚ =
    βˆ₯βˆ₯-functor r (semidirected-if-Directed 𝓓 Ξ± Ξ΄ (⌜ ρ ⌝⁻¹ j₁) (⌜ ρ ⌝⁻¹ jβ‚‚))
     where
      r : (Ξ£ i κž‰ I , (Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i) Γ— (Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ± i))
        β†’ (Ξ£ j κž‰ J , (Ξ² j₁ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j) Γ— (Ξ² jβ‚‚ βŠ‘βŸ¨ 𝓓 ⟩ Ξ² j))
      r (i , l₁ , lβ‚‚) = (⌜ ρ ⌝ i
                        , (Ξ² j₁                    βŠ‘βŸ¨ 𝓓 ⟩[ l₁ ]
                           Ξ± i                     βŠ‘βŸ¨ 𝓓 ⟩[ k ]
                           (Ξ± ∘ ⌜ ρ ⌝⁻¹ ∘ ⌜ ρ ⌝) i ∎⟨ 𝓓 ⟩)
                        , (Ξ² jβ‚‚                    βŠ‘βŸ¨ 𝓓 ⟩[ lβ‚‚ ]
                           Ξ± i                     βŠ‘βŸ¨ 𝓓 ⟩[ k ]
                           (Ξ± ∘ ⌜ ρ ⌝⁻¹ ∘ ⌜ ρ ⌝) i ∎⟨ 𝓓 ⟩))
       where
        k = =-to-βŠ’ 𝓓
             (ap α (inverses-are-retractions ⌜ ρ ⌝ (⌜⌝-is-equiv ρ) i))

 reindexed-family-sup : (x : ⟨ 𝓓 ⟩)
                      β†’ is-sup (underlying-order 𝓓) x Ξ±
                      β†’ is-sup (underlying-order 𝓓) x (reindexed-family)
 reindexed-family-sup x x-is-sup = ub , lb-of-ubs
  where
   Ξ² : J β†’ ⟨ 𝓓 ⟩
   Ξ² = reindexed-family
   ub : is-upperbound (underlying-order 𝓓) x Ξ²
   ub i = sup-is-upperbound (underlying-order 𝓓) x-is-sup (⌜ ρ ⌝⁻¹ i)
   lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order 𝓓) x Ξ²
   lb-of-ubs y y-is-ub = sup-is-lowerbound-of-upperbounds (underlying-order 𝓓)
                          x-is-sup y lemma
    where
     lemma : is-upperbound (underlying-order 𝓓) y Ξ±
     lemma i = Ξ± i         βŠ‘βŸ¨ 𝓓 ⟩[ β¦…1⦆ ]
               Ξ² (⌜ ρ ⌝ i) βŠ‘βŸ¨ 𝓓 ⟩[ β¦…2⦆ ]
               y           ∎⟨ 𝓓 ⟩
      where
       β¦…1⦆ = =-to-βŠ’ 𝓓
             (ap α (inverses-are-retractions ⌜ ρ ⌝ (⌜⌝-is-equiv ρ) i))
       β¦…2⦆ = y-is-ub (⌜ ρ ⌝ i)

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        {I : 𝓦 Μ‡ } {J : 𝓦' Μ‡ }
        (ρ : I ≃ J)
        (Ξ± : I β†’ ⟨ 𝓓 ⟩)
       where

 sup-reindexed-family : (x : ⟨ 𝓓 ⟩)
                      β†’ is-sup (underlying-order 𝓓) x (reindexed-family 𝓓 ρ Ξ±)
                      β†’ is-sup (underlying-order 𝓓) x Ξ±
 sup-reindexed-family x x-is-sup =
  transport (is-sup (underlying-order 𝓓) x) (dfunext fe h)
            (reindexed-family-sup 𝓓 (≃-sym ρ) Ξ² x x-is-sup)
   where
    Ξ² = reindexed-family 𝓓 ρ Ξ±
    h : reindexed-family 𝓓 (≃-sym ρ) Ξ² ∼ Ξ±
    h i = (Ξ± ∘ ⌜ ρ ⌝⁻¹ ∘ ⌜ ≃-sym ρ ⌝⁻¹) i =⟨ e₁ ⟩
          (Ξ± ∘ ⌜ ρ ⌝⁻¹ ∘ ⌜ ρ ⌝) i         =⟨ eβ‚‚ ⟩
          α i                             ∎
     where
      e₁ = ap (Ξ» - β†’ (Ξ± ∘ ⌜ ρ ⌝⁻¹ ∘ -) i)
              (inversion-involutive ⌜ ρ ⌝ (⌜⌝-is-equiv ρ))
      eβ‚‚ = ap Ξ± (inverses-are-retractions' ρ i)

\end{code}

Added 23 June 2024.
All dcpos (regardless of the universe level for index families) are Ο‰-complete.

\begin{code}

dcpos-are-Ο‰-complete : (𝓓 : DCPO {𝓀} {𝓣})
                     β†’ is-Ο‰-complete (underlying-order 𝓓)
dcpos-are-Ο‰-complete 𝓓 Ξ± Ξ±-is-Ο‰-chain = s , s-is-sup
 where
  β„•' : π“₯ Μ‡
  β„•' = Lift π“₯ β„•
  ρ : β„• ≃ Lift π“₯ β„•
  ρ = ≃-Lift π“₯ β„•
  Ξ΄ : is-Directed 𝓓 (reindexed-family 𝓓 (≃-Lift π“₯ β„•) Ξ±)
  Ξ΄ = reindexed-family-is-directed 𝓓 ρ Ξ± (Ο‰-chains-are-Directed 𝓓 Ξ± Ξ±-is-Ο‰-chain)
  s : ⟨ 𝓓 ⟩
  s = ∐ 𝓓 Ξ΄
  s-is-sup : is-sup (underlying-order 𝓓) s Ξ±
  s-is-sup = sup-reindexed-family 𝓓 ρ Ξ± s (∐-is-sup 𝓓 Ξ΄)

\end{code}

Added 18th Feb 2024 by Martin Escardo. Subdcpo induced by a subset /
property.

\begin{code}

is-closed-under-directed-sups : (𝓓 : DCPO {𝓀} {𝓣})
                              β†’ (⟨ 𝓓 ⟩ β†’ 𝓦 Μ‡)
                              β†’ π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓦 Μ‡
is-closed-under-directed-sups {𝓀} {𝓣} 𝓓 P =
    {I : π“₯ Μ‡ } (Ξ± : I β†’ ⟨ 𝓓 ⟩) (Ξ΄ : is-Directed 𝓓 Ξ±)
  β†’ ((i : I) β†’ P (Ξ± i))
  β†’ P (∐ 𝓓 Ξ΄)

open import UF.Sets-Properties

module _
         (𝓓 : DCPO {𝓀} {𝓣})
         (P : ⟨ 𝓓 ⟩ β†’ 𝓦 Μ‡)
         (P-is-prop-valued : (x : ⟨ 𝓓 ⟩) β†’ is-prop (P x))
         (P-is-closed-under-directed-sups : is-closed-under-directed-sups 𝓓 P)
       where

 subdcpo : DCPO {𝓀 βŠ” 𝓦} {𝓣}
 subdcpo =
  (Ξ£ x κž‰ ⟨ 𝓓 ⟩ , P x) ,
  (Ξ» (x , _) (y , _) β†’ x βŠ‘βŸ¨ 𝓓 ⟩ y) ,
  (subsets-of-sets-are-sets ⟨ 𝓓 ⟩ P (sethood 𝓓) (P-is-prop-valued _) ,
   (Ξ» _ _ β†’ prop-valuedness 𝓓 _ _) ,
   (Ξ» _ β†’ reflexivity 𝓓 _) ,
   (Ξ» (x , _) (y , _) (z , _) β†’ transitivity 𝓓 x y z) ,
   (Ξ» (x , _) (y , _) l m β†’ to-subtype-=
                             P-is-prop-valued
                             (antisymmetry 𝓓 x y l m))) ,
  (Ξ» I Ξ± Ξ΄ β†’ (∐ 𝓓 {I} {pr₁ ∘ Ξ±} Ξ΄ ,
              P-is-closed-under-directed-sups (pr₁ ∘ Ξ±) Ξ΄ (prβ‚‚ ∘ Ξ±)) ,
             ∐-is-upperbound 𝓓 Ξ΄ ,
             (Ξ» (x , _) β†’ ∐-is-lowerbound-of-upperbounds 𝓓 Ξ΄ x))

 subdcpo-inclusion : ⟨ subdcpo ⟩ β†’ ⟨ 𝓓 ⟩
 subdcpo-inclusion = pr₁

 subdcpo-satisfies-property : (Οƒ : ⟨ subdcpo ⟩) β†’ P (subdcpo-inclusion Οƒ)
 subdcpo-satisfies-property = prβ‚‚

open import UF.SubtypeClassifier

is-closed-under-directed-supsβ‚š : (𝓓 : DCPO {𝓀} {𝓣})
                               β†’ (⟨ 𝓓 ⟩ β†’ Ξ© 𝓦)
                               β†’ Ξ© (π“₯ ⁺ βŠ” 𝓀 βŠ” 𝓣 βŠ” 𝓦)
is-closed-under-directed-supsβ‚š {𝓀} {𝓣} 𝓓 P =
 is-closed-under-directed-sups 𝓓 (Ξ» x β†’ P x holds) ,
 Ξ -is-prop' fe (Ξ» I β†’ Π₃-is-prop fe (Ξ» Ξ± Ξ΄ c β†’ holds-is-prop (P (∐ 𝓓 Ξ΄))))

module _
        (𝓓 : DCPO {𝓀} {𝓣})
        (P : ⟨ 𝓓 ⟩ β†’ Ξ© 𝓦)
        (P-is-closed-under-directed-supsβ‚š : is-closed-under-directed-supsβ‚š 𝓓 P holds)
       where

 subdcpoβ‚š : DCPO {𝓀 βŠ” 𝓦} {𝓣}
 subdcpoβ‚š = subdcpo 𝓓
            (Ξ» x β†’ P x holds)
            (Ξ» x β†’ holds-is-prop (P x))
            P-is-closed-under-directed-supsβ‚š

\end{code}