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.