Tom de Jong, 26 Feburary 2020
Minor updates on 28 January 2022

We construct the rounded ideal completion of an abstract basis, cf. Section
2.2.6 in Domain Theory by Abramsky and Jung.

Further properties and developments are in the file IdealCompletion-Properties.

\begin{code}

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

open import MLTT.Spartan hiding (J)

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

module DomainTheory.IdealCompletion.IdealCompletion
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (π“₯ : Universe) -- universe where the index types for directedness
                       -- completeness live
       where

open import DomainTheory.Basics.Dcpo pt fe π“₯
open import OrderedTypes.Poset fe
open import UF.Powerset
open import UF.Sets
open import UF.Sets-Properties
open import UF.SubtypeClassifier
open import UF.Subsingletons-FunExt

open PosetAxioms

open PropositionalTruncation pt

module Ideals
        {P : 𝓀 Μ‡ }
        (_β‰Ί_ : P β†’ P β†’ π“₯ βŠ” 𝓣 Μ‡ )
        (β‰Ί-prop-valued : {p q : P} β†’ is-prop (p β‰Ί q))
        (INTβ‚‚ : {qβ‚€ q₁ p : P} β†’ qβ‚€ β‰Ί p β†’ q₁ β‰Ί p
              β†’ βˆƒ r κž‰ P , qβ‚€ β‰Ί r Γ— q₁ β‰Ί r Γ— r β‰Ί p)
        (INTβ‚€ : (p : P) β†’ βˆƒ q κž‰ P , q β‰Ί p)
        (β‰Ί-trans : {p q r : P} β†’ p β‰Ί q β†’ q β‰Ί r β†’ p β‰Ί r)
       where

 is-lowerset : (P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ π“₯ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-lowerset A = (p q : P) β†’ p β‰Ί q β†’ q ∈ A β†’ p ∈ A

 being-lowerset-is-prop : (I :  P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ is-prop (is-lowerset I)
 being-lowerset-is-prop I = Ξ β‚„-is-prop fe (Ξ» p q l i β†’ ∈-is-prop I p)

 is-inhabited-set : (P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓣 Μ‡
 is-inhabited-set A = βˆƒ p κž‰ P , p ∈ A

 being-inhabited-set-is-prop : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                             β†’ is-prop (is-inhabited-set I)
 being-inhabited-set-is-prop I = βˆ₯βˆ₯-is-prop

 is-semidirected-set : (P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ π“₯ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-semidirected-set A = (p q : P) β†’ p ∈ A β†’ q ∈ A
                          β†’ βˆƒ r κž‰ P , r ∈ A
                          Γ— p β‰Ί r Γ— q β‰Ί r

 being-semidirected-set-is-prop : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                                β†’ is-prop (is-semidirected-set I)
 being-semidirected-set-is-prop I = Ξ β‚„-is-prop fe (Ξ» p q i j β†’ βˆƒ-is-prop)

 is-directed-set : (P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ π“₯ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-directed-set A = is-inhabited-set A Γ— is-semidirected-set A

 being-directed-set-is-prop : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                            β†’ is-prop (is-directed-set I)
 being-directed-set-is-prop I =
  Γ—-is-prop
   (being-inhabited-set-is-prop I)
   (being-semidirected-set-is-prop I)

 directed-sets-are-inhabited : (A : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                             β†’ is-directed-set A β†’ is-inhabited-set A
 directed-sets-are-inhabited A = pr₁

 directed-sets-are-semidirected : (A : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                                β†’ is-directed-set A
                                β†’ is-semidirected-set A
 directed-sets-are-semidirected A = prβ‚‚

 is-ideal : (P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ π“₯ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 is-ideal I = is-lowerset I Γ— is-directed-set I

 being-ideal-is-prop : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ is-prop (is-ideal I)
 being-ideal-is-prop I =
  Γ—-is-prop
   (being-lowerset-is-prop I)
   (being-directed-set-is-prop I)

 ideals-are-lowersets : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣)) β†’ is-ideal I β†’ is-lowerset I
 ideals-are-lowersets I = pr₁

 ideals-are-directed-sets : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                          β†’ is-ideal I β†’ is-directed-set I
 ideals-are-directed-sets I = prβ‚‚

 ideals-are-inhabited : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                      β†’ is-ideal I β†’ is-inhabited-set I
 ideals-are-inhabited I ΞΉ =
  directed-sets-are-inhabited I (ideals-are-directed-sets I ΞΉ)

 ideals-are-semidirected : (I : P β†’ Ξ© (π“₯ βŠ” 𝓣))
                         β†’ is-ideal I β†’ is-semidirected-set I
 ideals-are-semidirected I ΞΉ =
  directed-sets-are-semidirected I (ideals-are-directed-sets I ΞΉ)

 Idl : π“₯ ⁺ βŠ” 𝓣 ⁺ βŠ” 𝓀 Μ‡
 Idl = Ξ£ I κž‰ (P β†’ Ξ© (π“₯ βŠ” 𝓣)) , is-ideal I

 carrier : Idl β†’ P β†’ Ξ© (π“₯ βŠ” 𝓣)
 carrier = pr₁

 ideality : (I : Idl) β†’ is-ideal (carrier I)
 ideality = prβ‚‚

 _∈ᡒ_ : P β†’ Idl β†’ π“₯ βŠ” 𝓣 Μ‡
 p ∈ᡒ I = p ∈ carrier I

 _βŠ‘_ : Idl β†’ Idl β†’ π“₯ βŠ” 𝓀 βŠ” 𝓣 Μ‡
 I βŠ‘ J = carrier I βŠ† carrier J

 Idl-∐ : {𝓐 : π“₯ Μ‡ } (Ξ± : 𝓐 β†’ Idl) β†’ is-directed _βŠ‘_ Ξ± β†’ Idl
 Idl-∐ {𝓐} Ξ± Ξ΄ = (∐α , ls , inh , Ξ΅)
  where
   open unions-of-small-families pt π“₯ 𝓣 P
   ∐α : P β†’ Ξ© (π“₯ βŠ” 𝓣)
   ∐α = ⋃ (carrier ∘ Ξ±)
   ls : is-lowerset ∐α
   ls p q l = βˆ₯βˆ₯-functor Ξ³
    where
     Ξ³ : (Ξ£ a κž‰ 𝓐 , q ∈ᡒ Ξ± a) β†’ (Ξ£ a κž‰ 𝓐 , p ∈ᡒ Ξ± a)
     Ξ³ (a , u) = a , ideals-are-lowersets (carrier (Ξ± a)) (ideality (Ξ± a))
                     p q l u
   inh : βˆƒ p κž‰ P , p ∈ ∐α
   inh = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop Ξ³ (inhabited-if-directed _βŠ‘_ Ξ± Ξ΄)
    where
     Ξ³ : 𝓐 β†’ βˆƒ p κž‰ P , p ∈ ∐α
     Ξ³ a = βˆ₯βˆ₯-functor h inh'
      where
       inh' : is-inhabited-set (carrier (Ξ± a))
       inh' = directed-sets-are-inhabited (carrier (Ξ± a))
              (ideals-are-directed-sets (carrier (Ξ± a)) (ideality (Ξ± a)))
       h : (Ξ£ p κž‰ P , p ∈ᡒ Ξ± a) β†’ (Ξ£ p κž‰ P , p ∈ ∐α)
       h (p , u) = p , ∣ a , u ∣
   Ρ : is-semidirected-set ∐α
   Ξ΅ p q i j = βˆ₯βˆ₯-recβ‚‚ βˆ₯βˆ₯-is-prop Ξ³ i j
    where
     Ξ³ : (Ξ£ a κž‰ 𝓐 , p ∈ᡒ Ξ± a)
       β†’ (Ξ£ b κž‰ 𝓐 , q ∈ᡒ Ξ± b)
       β†’ βˆƒ r κž‰ P , r ∈ ∐α Γ— p β‰Ί r Γ— q β‰Ί r
     Ξ³ (a , ia) (b , jb) =
      βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop g (semidirected-if-directed _βŠ‘_ Ξ± Ξ΄ a b)
       where
        g : (Ξ£ c κž‰ 𝓐 , Ξ± a βŠ‘ Ξ± c Γ— Ξ± b βŠ‘ Ξ± c)
          β†’ βˆƒ r κž‰ P , r ∈ ∐α Γ— p β‰Ί r Γ— q β‰Ί r
        g (c , l , m) = do
         (r , k , u , v) ← directed-sets-are-semidirected (carrier (Ξ± c))
                           (ideals-are-directed-sets (carrier (Ξ± c))
                            (ideality (Ξ± c)))
                           p q ic jc
         ∣ r , ∣ c , k ∣ , u , v ∣
         where
         ic : p ∈ᡒ α c
         ic = l p ia
         jc : q ∈ᡒ α c
         jc = m q jb

 Idl-DCPO : DCPO {π“₯ ⁺ βŠ” 𝓣 ⁺ βŠ” 𝓀} {π“₯ βŠ” 𝓀 βŠ” 𝓣}
 Idl-DCPO = Idl , _βŠ‘_ , Ξ³
  where
   Ξ³ : dcpo-axioms _βŠ‘_
   Ξ³ = pa , dc
    where
     pa : poset-axioms _βŠ‘_
     pa = s , pv , r , t , a
      where
       s : is-set Idl
       s = subtypes-of-sets-are-sets' carrier
            (pr₁-lc Ξ» {I} β†’ being-ideal-is-prop I)
            (powersets-are-sets'' fe fe pe)
       pv : is-prop-valued _βŠ‘_
       pv I J = βŠ†-is-prop' fe fe (carrier I) (carrier J)
       r : (I : Idl) β†’ I βŠ‘ I
       r I = βŠ†-refl' (carrier I)
       t : is-transitive _βŠ‘_
       t I J K = βŠ†-trans' (carrier I) (carrier J) (carrier K)
       a : is-antisymmetric _βŠ‘_
       a I J u v = to-subtype-＝
                    (Ξ» K β†’ being-ideal-is-prop K)
                    (subset-extensionality'' pe fe fe u v)
     dc : is-directed-complete _βŠ‘_
     dc 𝓐 Ξ± Ξ΄ = (Idl-∐ Ξ± Ξ΄) , ub , lb
      where
       ub : (a : 𝓐) β†’ Ξ± a βŠ‘ Idl-∐ Ξ± Ξ΄
       ub a p p-in-a = ∣ a , p-in-a ∣
       lb : is-lowerbound-of-upperbounds _βŠ‘_ (Idl-∐ Ξ± Ξ΄) Ξ±
       lb I ub p p-in-∐α = βˆ₯βˆ₯-rec (∈-is-prop (carrier I) p) h p-in-∐α
        where
         h : (Ξ£ a κž‰ 𝓐 , p ∈ᡒ Ξ± a) β†’ p ∈ᡒ I
         h (a , q) = ub a p q

\end{code}