Tom de Jong and Ayberk Tosun, 4 & 5 October 2023


Given an algebraic dcpo ๐““, the subset K of compact elements forms a basis for ๐““.
In our predicative context, we consider *small* bases, however, and a priori
there is no reason for K to be a small type.

However, if ๐““ comes equipped with what we call a small compact basis, then set
replacementยน implies that K is small.

If we moreover assume univalence, then the relevant small condition is a
property, which means that having an unspecified small compact basis is
sufficient.

In particular, with set replacement and univalence, we can show:
  โˆฅ has-specified-small-compact-basis ๐““ โˆฅ โ†’ has-specified-small-compact-basis ๐““.
In other words, the type (has-specified-small-compact-basis ๐““) has split support.

Having a specified small compact basis is useful as we can use the small basis
to replace large quantifications by small ones for example, for example to show
that exponentials are locally small.

The split support observation is due to Ayberk Tosun (23 September 2023) and was
formalised, with the addition of many explanatory comments, by Tom de Jong.
Ayberk previously formalised the result for spectrality in the context of locale
theory in Locales.SmallBasis (truncated-spectralแดฐ-implies-spectral).

Towards the end, we also clarify how the fact that K is the unique basis (as a
subset) consisting of compact elements fits in to our framework.


ยน Set replacement says: if f : X โ†’ Y is a map from a small type to a locally
  small set, then the image of f is small.
  It is equivalent to having small set quotients, see Quotient.index.

\begin{code}

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

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

module DomainTheory.BasesAndContinuity.CompactBasis
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (๐“ฅ : Universe) -- where the index types for directed completeness live
       where

open PropositionalTruncation pt

open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ImageAndSurjection pt
open import UF.KrausLemma
open import UF.Sets
open import UF.Sets-Properties
open import UF.Size hiding (is-small ; is-locally-small)
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Univalence

open split-support-and-collapsibility pt

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.Bases pt fe ๐“ฅ
open import DomainTheory.BasesAndContinuity.Continuity pt fe ๐“ฅ

\end{code}

As announced above, we start by establishing as many as properties of K as
possible without considering that K needs to be small.

For this, we only assume, in a few places, that our dcpo is algebraic (as a
property rather than as data).

\begin{code}

module _
        (๐““ : DCPO {๐“ค} {๐“ฃ})
       where

 K : ๐“ฅ โบ โŠ” ๐“ค โŠ” ๐“ฃ ฬ‡
 K = ฮฃ x ๊ž‰ โŸจ ๐““ โŸฉ , is-compact ๐““ x

 K-inclusion : K โ†’ โŸจ ๐““ โŸฉ
 K-inclusion = prโ‚

 private
  ฮน : K โ†’ โŸจ ๐““ โŸฉ
  ฮน = prโ‚

 K-inclusion-is-compact : (c : K) โ†’ is-compact ๐““ (ฮน c)
 K-inclusion-is-compact = prโ‚‚

 โ†“แดท : โŸจ ๐““ โŸฉ โ†’ ๐“ฅ โบ โŠ” ๐“ค โŠ” ๐“ฃ ฬ‡
 โ†“แดท x = ฮฃ k ๊ž‰ K , ฮน k โŠ‘โŸจ ๐““ โŸฉ x

 โ†“แดท-inclusion : (x : โŸจ ๐““ โŸฉ) โ†’ โ†“แดท x โ†’ โŸจ ๐““ โŸฉ
 โ†“แดท-inclusion x = ฮน โˆ˜ prโ‚

\end{code}

We show that every element x of ๐““ is the *directed* supremum of the inclusion
  (ฮฃ k ๊ž‰ K , k โŠ‘โŸจ ๐““ โŸฉ x) โ†’ โŸจ ๐““ โŸฉ.

\begin{code}

 โ†“แดท-is-inhabited : is-algebraic-dcpo ๐““ โ†’ (x : โŸจ ๐““ โŸฉ) โ†’ โˆฅ โ†“แดท x โˆฅ
 โ†“แดท-is-inhabited is-alg x = โˆฅโˆฅ-rec โˆฅโˆฅ-is-prop ฮณ is-alg
  where
   ฮณ : structurally-algebraic ๐““
     โ†’ โˆฅ โ†“แดท x โˆฅ
   ฮณ str-alg = โˆฅโˆฅ-functor f inh
    where
     open structurally-algebraic str-alg
     inh : โˆฅ index-of-compact-family x โˆฅ
     inh = inhabited-if-Directed ๐““ (compact-family x)
                                   (compact-family-is-directed x)
     f : index-of-compact-family x โ†’ โ†“แดท x
     f i = (compact-family x i , compact-family-is-compact x i)
           , compact-family-is-upperbound x i

 โ†“แดท-is-semidirected : is-algebraic-dcpo ๐““
                    โ†’ (x : โŸจ ๐““ โŸฉ) โ†’ is-Semidirected ๐““ (โ†“แดท-inclusion x)
 โ†“แดท-is-semidirected is-alg x =
  โˆฅโˆฅ-rec (being-semidirected-is-prop (underlying-order ๐““) (โ†“แดท-inclusion x))
         ฮณ is-alg
   where
    ฮณ : structurally-algebraic ๐““
      โ†’ is-Semidirected ๐““ (โ†“แดท-inclusion x)
    ฮณ str-alg ((cโ‚ , cโ‚-compact) , cโ‚-below-x)
              ((cโ‚‚ , cโ‚‚-compact) , cโ‚‚-below-x) =
     โˆฅโˆฅ-recโ‚‚ โˆƒ-is-prop sd โฆ…1โฆ† โฆ…2โฆ†
      where
       open structurally-algebraic str-alg
       I = index-of-compact-family x
       ฮบ = compact-family x
       ฮด = compact-family-is-directed x
       โฆ…1โฆ† : โˆƒ iโ‚ ๊ž‰ I , cโ‚ โŠ‘โŸจ ๐““ โŸฉ compact-family x iโ‚
       โฆ…1โฆ† = cโ‚-compact I ฮบ ฮด
                        (cโ‚     โŠ‘โŸจ ๐““ โŸฉ[ cโ‚-below-x ]
                         x      โŠ‘โŸจ ๐““ โŸฉ[ ๏ผ-to-โŠ’ ๐““ (compact-family-โˆ-๏ผ x) ]
                         โˆ ๐““ ฮด โˆŽโŸจ ๐““ โŸฉ)
       โฆ…2โฆ† : โˆƒ iโ‚‚ ๊ž‰ I , cโ‚‚ โŠ‘โŸจ ๐““ โŸฉ compact-family x iโ‚‚
       โฆ…2โฆ† = cโ‚‚-compact I ฮบ ฮด
                        (cโ‚‚     โŠ‘โŸจ ๐““ โŸฉ[ cโ‚‚-below-x ]
                         x      โŠ‘โŸจ ๐““ โŸฉ[ ๏ผ-to-โŠ’ ๐““ (compact-family-โˆ-๏ผ x) ]
                         โˆ ๐““ ฮด โˆŽโŸจ ๐““ โŸฉ)
       sd : (ฮฃ iโ‚ ๊ž‰ I , cโ‚ โŠ‘โŸจ ๐““ โŸฉ ฮบ iโ‚)
          โ†’ (ฮฃ iโ‚‚ ๊ž‰ I , cโ‚‚ โŠ‘โŸจ ๐““ โŸฉ ฮบ iโ‚‚)
          โ†’ โˆƒ c ๊ž‰ โ†“แดท x , (cโ‚ โŠ‘โŸจ ๐““ โŸฉ โ†“แดท-inclusion x c)
                       ร— (cโ‚‚ โŠ‘โŸจ ๐““ โŸฉ โ†“แดท-inclusion x c)
       sd (iโ‚ , cโ‚-below-iโ‚) (iโ‚‚ , cโ‚‚-below-iโ‚‚) = โˆฅโˆฅ-functor f semidir
        where
         semidir : โˆƒ i ๊ž‰ I , (ฮบ iโ‚ โŠ‘โŸจ ๐““ โŸฉ ฮบ i) ร— (ฮบ iโ‚‚ โŠ‘โŸจ ๐““ โŸฉ ฮบ i)
         semidir = semidirected-if-Directed ๐““ ฮบ ฮด iโ‚ iโ‚‚
         f : (ฮฃ i ๊ž‰ I , (ฮบ iโ‚ โŠ‘โŸจ ๐““ โŸฉ ฮบ i) ร— (ฮบ iโ‚‚ โŠ‘โŸจ ๐““ โŸฉ ฮบ i))
           โ†’ ฮฃ c ๊ž‰ โ†“แดท x , (cโ‚ โŠ‘โŸจ ๐““ โŸฉ โ†“แดท-inclusion x c)
                        ร— (cโ‚‚ โŠ‘โŸจ ๐““ โŸฉ โ†“แดท-inclusion x c)
         f (i , iโ‚-below-i , iโ‚‚-below-i) = ((ฮบ i , compact-family-is-compact x i)
                                           , compact-family-is-upperbound x i)
                                           , (cโ‚   โŠ‘โŸจ ๐““ โŸฉ[ cโ‚-below-iโ‚ ]
                                              ฮบ iโ‚ โŠ‘โŸจ ๐““ โŸฉ[ iโ‚-below-i ]
                                              ฮบ i  โˆŽโŸจ ๐““ โŸฉ)
                                           , (cโ‚‚   โŠ‘โŸจ ๐““ โŸฉ[ cโ‚‚-below-iโ‚‚ ]
                                              ฮบ iโ‚‚ โŠ‘โŸจ ๐““ โŸฉ[ iโ‚‚-below-i ]
                                              ฮบ i  โˆŽโŸจ ๐““ โŸฉ)

 โ†“แดท-is-directed : is-algebraic-dcpo ๐““
                โ†’ (x : โŸจ ๐““ โŸฉ) โ†’ is-Directed ๐““ (โ†“แดท-inclusion x)
 โ†“แดท-is-directed is-alg x = โ†“แดท-is-inhabited is-alg x , โ†“แดท-is-semidirected is-alg x

 โ†“แดท-is-upperbound : (x : โŸจ ๐““ โŸฉ)
                  โ†’ is-upperbound (underlying-order ๐““) x (โ†“แดท-inclusion x)
 โ†“แดท-is-upperbound x c = prโ‚‚ c

 โ†“แดท-is-sup : is-algebraic-dcpo ๐““
           โ†’ (x : โŸจ ๐““ โŸฉ) โ†’ is-sup (underlying-order ๐““) x (โ†“แดท-inclusion x)
 โ†“แดท-is-sup is-alg x =
  โˆฅโˆฅ-rec (is-sup-is-prop (underlying-order ๐““) (prโ‚ (axioms-of-dcpo ๐““))
                         x (โ†“แดท-inclusion x))
         ฮณ is-alg
   where
    ฮณ : structurally-algebraic ๐““
      โ†’ is-sup (underlying-order ๐““) x (โ†“แดท-inclusion x)
    ฮณ str-alg = โ†“แดท-is-upperbound x , lb-of-ubs
     where
      open structurally-algebraic str-alg
      lb-of-ubs : is-lowerbound-of-upperbounds (underlying-order ๐““) x
                                               (โ†“แดท-inclusion x)
      lb-of-ubs y y-is-ub =
       transport (ฮป - โ†’ - โŠ‘โŸจ ๐““ โŸฉ y)
                 (compact-family-โˆ-๏ผ x)
                 (โˆ-is-lowerbound-of-upperbounds ๐““
                   (compact-family-is-directed x) y lb-of-ubs')
        where
         lb-of-ubs' : (i : index-of-compact-family x)
                    โ†’ compact-family x i โŠ‘โŸจ ๐““ โŸฉ y
         lb-of-ubs' i = y-is-ub ((compact-family x i
                                , compact-family-is-compact x i)
                                , compact-family-is-upperbound x i)

\end{code}

Assuming set replacement and a *specified* small compact basis, we deduce that K
is a small type.

\begin{code}

 module _
         (sr : Set-Replacement pt)
         ((B , ฮฒ , scb) : has-specified-small-compact-basis ๐““)
        where

  open is-small-compact-basis scb
  open is-locally-small (locally-small-if-small-compact-basis ๐““ ฮฒ scb)

  K-is-small' : is-small K
  K-is-small' = โ‰ƒ-size-contravariance K-is-image image-is-small
   where
    ฮฒ' : B โ†’ K
    ฮฒ' b = ฮฒ b , basis-is-compact b
    ฮฒ'-is-surjection : is-surjection ฮฒ'
    ฮฒ'-is-surjection (x , x-compact) =
     โˆฅโˆฅ-functor
      (ฮป {(b , refl) โ†’ b , to-subtype-๏ผ (being-compact-is-prop ๐““) refl})
      (small-compact-basis-contains-all-compact-elements
       ๐““ ฮฒ scb x x-compact)
    K-is-image : K โ‰ƒ image ฮฒ'
    K-is-image = โ‰ƒ-sym (surjection-โ‰ƒ-image ฮฒ' ฮฒ'-is-surjection)
    K-is-set : is-set K
    K-is-set = subtypes-of-sets-are-sets' ฮน
                (prโ‚-lc (ฮป {x} โ†’ being-compact-is-prop ๐““ x)) (sethood ๐““)
    K-is-locally-small : K is-locally ๐“ฅ small
    K-is-locally-small (x , x-compact) (y , y-compact) =
       ((x โŠ‘โ‚› y) ร— (y โŠ‘โ‚› x))
     , logically-equivalent-props-are-equivalent
        (ร—-is-prop (โŠ‘โ‚›-is-prop-valued x y) (โŠ‘โ‚›-is-prop-valued y x))
        K-is-set
        (ฮป (l , k) โ†’ to-subtype-๏ผ (being-compact-is-prop ๐““)
                                   (antisymmetry ๐““ x y (โŠ‘โ‚›-to-โŠ‘ l)
                                                       (โŠ‘โ‚›-to-โŠ‘ k)))
        ฮป {refl โ†’ reflexivityโ‚› x , reflexivityโ‚› x}
    image-is-small : is-small (image ฮฒ')
    image-is-small = sr ฮฒ' (B , โ‰ƒ-refl B) K-is-locally-small K-is-set

  ฮน-โŠ‘-is-small' : (x : โŸจ ๐““ โŸฉ) (c : K) โ†’ is-small (ฮน c โŠ‘โŸจ ๐““ โŸฉ x)
  ฮน-โŠ‘-is-small' x c =
   โŒœ local-smallness-equivalent-definitions ๐““ โŒ loc-small (ฮน c) x
    where
     loc-small : is-locally-small ๐““
     loc-small = locally-small-if-small-compact-basis ๐““ ฮฒ scb

\end{code}

If we additionally assume univalence, then we can prove that K is small from
assuming an *unspecified* small compact basis.

The need for univalence lies in the fact that it implies that smallness is a
property (being-small-is-prop).
(In fact, univalence is equivalent to this, in some precise sense, see UF.Size.)

\begin{code}

 module _
         (ua : Univalence)
         (sr : Set-Replacement pt)
         (uscb : has-unspecified-small-compact-basis ๐““)
        where

  private
   is-alg : is-algebraic-dcpo ๐““
   is-alg = is-algebraic-dcpo-if-unspecified-small-compact-basis ๐““ uscb

  K-is-small : is-small K
  K-is-small = โˆฅโˆฅ-rec (being-small-is-prop ua K ๐“ฅ) ฮณ uscb
   where
    ฮณ : has-specified-small-compact-basis ๐““
      โ†’ is-small K
    ฮณ scb = K-is-small' sr scb

  ฮน-โŠ‘-is-small : (x : โŸจ ๐““ โŸฉ) (c : K) โ†’ is-small (ฮน c โŠ‘โŸจ ๐““ โŸฉ x)
  ฮน-โŠ‘-is-small = โˆฅโˆฅ-rec (ฮ โ‚‚-is-prop fe (ฮป x c โ†’ being-small-is-prop
                                                 ua (ฮน c โŠ‘โŸจ ๐““ โŸฉ x) ๐“ฅ))
                        ฮณ uscb
   where
    ฮณ : has-specified-small-compact-basis ๐““
      โ†’ (x : โŸจ ๐““ โŸฉ) (c : K) โ†’ is-small (ฮน c โŠ‘โŸจ ๐““ โŸฉ x)
    ฮณ scb = ฮน-โŠ‘-is-small' sr scb

\end{code}

We now package things up, using the small copy Kโ‚› of K and a reindexing along
the equivalence Kโ‚› โ‰ƒ K, to produce a small compact basis.

\begin{code}

  Kโ‚› : ๐“ฅ ฬ‡
  Kโ‚› = resized K K-is-small

  Kโ‚›-inclusion : Kโ‚› โ†’ โŸจ ๐““ โŸฉ
  Kโ‚›-inclusion = ฮน โˆ˜ โŒœ resizing-condition K-is-small โŒ

  private
   ฮนโ‚› : Kโ‚› โ†’ โŸจ ๐““ โŸฉ
   ฮนโ‚› = Kโ‚›-inclusion

  โ†“-resizing : (x : โŸจ ๐““ โŸฉ) โ†’ โ†“แดท x โ‰ƒ โ†“แดฎ ๐““ ฮนโ‚› x
  โ†“-resizing x =
   โ‰ƒ-sym (ฮฃ-change-of-variable _ โŒœ resizing-condition K-is-small โŒ
                               (โŒœโŒ-is-equiv (resizing-condition K-is-small)))

  โ†“แดทโ‚›-is-directed : (x : โŸจ ๐““ โŸฉ) โ†’ is-Directed ๐““ (โ†“-inclusion ๐““ ฮนโ‚› x)
  โ†“แดทโ‚›-is-directed x =
   reindexed-family-is-directed ๐““ (โ†“-resizing x)
                                  (โ†“แดท-inclusion x)
                                  (โ†“แดท-is-directed is-alg x)

  Kโ‚›-is-small-compact-basis : is-small-compact-basis ๐““ ฮนโ‚›
  Kโ‚›-is-small-compact-basis =
   record
    { basis-is-compact = ฮป k โ†’ K-inclusion-is-compact (โŒœ resizing-condition K-is-small โŒ k)
    ; โŠ‘แดฎ-is-small = ฮป x k โ†’ ฮน-โŠ‘-is-small x (โŒœ resizing-condition K-is-small โŒ k)
    ; โ†“แดฎ-is-directed = โ†“แดทโ‚›-is-directed
    ; โ†“แดฎ-is-sup = ฮป x โ†’ reindexed-family-sup ๐““ (โ†“-resizing x)
                                               (โ†“แดท-inclusion x) x
                                               (โ†“แดท-is-sup is-alg x)
    }

\end{code}

Finally, we arrive at the result announced at the top of this file: the type
(has-specified-small-compact-basis ๐““) has split support.

\begin{code}

module _
        (ua : Univalence)
        (sr : Set-Replacement pt)
        (๐““ : DCPO {๐“ค} {๐“ฃ})
       where

 specified-small-compact-basis-has-split-support :
  has-split-support (has-specified-small-compact-basis ๐““)
 specified-small-compact-basis-has-split-support uscb =
  Kโ‚› ๐““ ua sr uscb , Kโ‚›-inclusion ๐““ ua sr uscb ,
  Kโ‚›-is-small-compact-basis ๐““ ua sr uscb

\end{code}

In particular, we can extract algebraicity structure from an unspecified small
compact basis.

\begin{code}

 structurally-algebraic-if-unspecified-small-compact-basis :
    has-unspecified-small-compact-basis ๐““
  โ†’ structurally-algebraic ๐““
 structurally-algebraic-if-unspecified-small-compact-basis =
  structurally-algebraic-if-specified-small-compact-basis ๐““
   โˆ˜ specified-small-compact-basis-has-split-support

\end{code}

Another formulation is that we have the following logical equivalence:

\begin{code}

 specified-unspecified-equivalence :
  has-specified-small-compact-basis ๐““ โ†” has-unspecified-small-compact-basis ๐““
 specified-unspecified-equivalence =
    โˆฃ_โˆฃ
  , specified-small-compact-basis-has-split-support

\end{code}

We note that the above cannot be promoted to an equivalence of types, because
the left-hand side, the type (has-specified-small-compact-basis ๐““), is not a
proposition. This may seem puzzling, especially to domain theorists, as there is
a unique basis (as a subset) which consists of compact elements, so we stop to
explain this here.

Recall that
  has-specified-small-compact-basis ๐““ :=
    ฮฃ B ๊ž‰ ๐“ฅ ฬ‡ , ฮฃ ฮฒ ๊ž‰ (B โ†’ โŸจ ๐““ โŸฉ) , (1) ร— (2) ร— (3)
with (1)โ”€(3) expressing that:
  (1) all elements ฮฒ b are compact,
  (2) (ฮฒ b โŠ‘โŸจ ๐““ โŸฉ x) is a small type for all elements x, and
  (3) the family (ฮฃ b ๊ž‰ B , ฮฒ b โŠ‘โŸจ ๐““ โŸฉ) โ†’ โŸจ ๐““ โŸฉ is directed with sup x.

If we drop smallness condition (2) and allow for B to live in larger universes
than ๐“ฅ, then K, the subset of compact elements with its inclusion K โ†’ โŸจ ๐““ โŸฉ,
will fit the specification.

If we now add the condition that ฮฒ is an embedding (as it is for K), then we get
the type
    ฮฃ B ๊ž‰ _ ฬ‡ฬ‡ , ฮฃ ฮฒ ๊ž‰ (B โ†’ โŸจ ๐““ โŸฉ) , (1) ร— (3) ร— (ฮฒ is an embedding)
which *is* a proposition: it has a unique element in case ๐““ is algebraic, given
by the *subset* of compact elements of ๐““. (This is true because any basis must
contain all compact elements.)

This raises a question: why don't we require ฮฒ to be an embedding in our
definition of a small compact basis to obtain a property instead of truncating
the type has-specified-small-compact-basis?

The reason is that it could be useful, as we illustrate now:

  The canonical map from lists into the powerset of a set X,
    ฮฒ : List X โ†’ ๐“Ÿ X
  is a small compact basis for the algebraic dcpo ๐“Ÿ X. This map is not an
  embedding, as any permutation of a list will give rise to the same subset.

  If we insisted on having an embedding, we would instead have to use the
  inclusion of the Kuratowski finite subsets ๐“š X into ๐“Ÿ X.  However, ๐“š X is not
  a small type without additional assumptions, such as HITs or more specifically,
  set replacement (as ๐“š X is precisely the image of the map ฮฒ : List X โ†’ ๐“Ÿ X).

Returning to the main line of thought, we conclude that, in the presence of set
replacement and univalence, if there is some unspecified small compact basis,
then the subset K of compact elements is suitably small.