Tom de Jong, 3 June 2024.

We consider the lifting of a proposition P as a locally small algebraic dcpo
which does not have a small basis unless the proposition P can be resized.

\begin{code}

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

open import MLTT.Spartan

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

module DomainTheory.Examples.LiftingLargeProposition
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (๐“ฅ ๐“ค : Universe)
        (P : ๐“ค ฬ‡  )
        (P-is-prop : is-prop P)
       where

open PropositionalTruncation pt

open import UF.Equiv
open import UF.Sets
open import UF.Size hiding (is-locally-small)
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties

private
 P-is-set : is-set P
 P-is-set = props-are-sets (P-is-prop)

open import DomainTheory.Basics.Dcpo pt fe ๐“ฅ
open import DomainTheory.Basics.Miscelanea pt fe ๐“ฅ
open import DomainTheory.Basics.Pointed pt fe ๐“ฅ
open import DomainTheory.Basics.SupComplete pt fe ๐“ฅ
open import DomainTheory.Basics.WayBelow pt fe ๐“ฅ
open import DomainTheory.BasesAndContinuity.Bases pt fe ๐“ฅ
open import DomainTheory.BasesAndContinuity.Continuity pt fe ๐“ฅ
open import DomainTheory.Lifting.LiftingSet pt fe ๐“ฅ pe
open import DomainTheory.Lifting.LiftingSetAlgebraic pt pe fe ๐“ฅ hiding (ฮบ)

open import Lifting.Construction ๐“ฅ
open import Lifting.Miscelanea ๐“ฅ
open import Lifting.Miscelanea-PropExt-FunExt ๐“ฅ pe fe
open import Lifting.UnivalentPrecategory ๐“ฅ P hiding (_โŠ‘_)

open import OrderedTypes.Poset
open PosetAxioms fe

\end{code}

The lifting of a set with respect to the propositions in a universe ๐“ฅ always
produces a ๐“ฅ-directed complete poset. Here, we obtain a ๐“ฅ-dcpo with carrier in
๐“ฅ โบ โŠ” ๐“ค where P : ๐“ค.

\begin{code}

๐“›P : DCPOโŠฅ {๐“ฅ โบ โŠ” ๐“ค} {๐“ฅ โบ โŠ” ๐“ค}
๐“›P = ๐“›-DCPOโŠฅ {๐“ค} {P} (props-are-sets P-is-prop)

\end{code}

Because P is a proposition, the order on ๐“›P is equivalent to the simpler partial
order defined below. This also shows that ๐“›P is locally small, despite P being
(potentially) large.

\begin{code}

private
 _โŠ‘_ : โŸช ๐“›P โŸซ โ†’ โŸช ๐“›P โŸซ โ†’ ๐“ฅ ฬ‡
 (Q , _) โŠ‘ (R , _) = Q โ†’ R

 โŠ‘-is-prop-valued : (Q R : โŸช ๐“›P โŸซ) โ†’ is-prop (Q โŠ‘ R)
 โŠ‘-is-prop-valued Q (R , _ , i) = ฮ -is-prop fe (ฮป _ โ†’ i)

 โŠ‘-to-๐“›-โŠ‘ : (Q R : โŸช ๐“›P โŸซ) โ†’ (Q โŠ‘ R โ†’ Q โŠ‘โŸช ๐“›P โŸซ R)
 โŠ‘-to-๐“›-โŠ‘ (Q , _ , i) (R , _ , j) l h =
  to-subtype-๏ผ
   (ฮป _ โ†’ ร—-is-prop (ฮ -is-prop fe (ฮป _ โ†’ P-is-prop))
   (being-prop-is-prop fe))
   (pe i j l (ฮป r โ†’ h))

 ๐“›-โŠ‘-to-โŠ‘ : (Q R : โŸช ๐“›P โŸซ) โ†’ (Q โŠ‘โŸช ๐“›P โŸซ R โ†’ Q โŠ‘ R)
 ๐“›-โŠ‘-to-โŠ‘ Q R l = def-pr Q R (โŠ‘'-to-โŠ‘ l)

๐“›P-is-locally-small : is-locally-small (๐“›P โป)
๐“›P-is-locally-small =
 record
  { _โŠ‘โ‚›_ = _โŠ‘_ ;
    โŠ‘โ‚›-โ‰ƒ-โŠ‘ = ฮป {Q} {R} โ†’ logically-equivalent-props-are-equivalent
              (โŠ‘-is-prop-valued Q R)
              (prop-valuedness (๐“›P โป) Q R)
              (โŠ‘-to-๐“›-โŠ‘ Q R)
              (๐“›-โŠ‘-to-โŠ‘ Q R)
  }

\end{code}

We now work towards showing that ๐“›P is algebraic. The idea is that an element
Q : ๐“›P is the supremum of the directed family
  ๐Ÿ™ + Q โ†’ ๐“›P
  *     โ†ฆ ๐Ÿ˜
      q โ†ฆ ๐Ÿ™
whose elements are compact.

\begin{code}

private
 module _
   (โ„š@(Q , Q-implies-P , Q-is-prop) : โŸช ๐“›P โŸซ)
  where

  family : Q โ†’ โŸช ๐“›P โŸซ
  family q = ๐Ÿ™ , (ฮป _ โ†’ Q-implies-P q) , ๐Ÿ™-is-prop

  family-members-are-compact : (q : Q) โ†’ is-compact (๐“›P โป) (family q)
  family-members-are-compact q I ฮฑ ฮด l = โˆฅโˆฅ-functor โฆ…2โฆ† โฆ…1โฆ†
   where
    โฆ…1โฆ† : โˆƒ i ๊ž‰ I , is-defined (ฮฑ i)
    โฆ…1โฆ† = ๏ผ-to-is-defined (l โ‹†) โ‹†
    โฆ…2โฆ† : (ฮฃ i ๊ž‰ I , is-defined (ฮฑ i))
        โ†’ ฮฃ i ๊ž‰ I , family q โŠ‘โŸช ๐“›P โŸซ ฮฑ i
    โฆ…2โฆ† (i , d) = i , ๏ผ-to-โŠ‘ (๐“›P โป) (family q   ๏ผโŸจ l โ‹† โŸฉ
                                      โˆ (๐“›P โป) ฮด ๏ผโŸจ e โปยน โŸฉ
                                      ฮฑ i        โˆŽ)
     where
      e = family-defined-somewhere-sup-๏ผ P-is-set ฮด i d

  upperbound-of-family : is-upperbound _โŠ‘_ โ„š family
  upperbound-of-family q _ = q

  lowerbound-of-upperbounds-of-family : is-lowerbound-of-upperbounds _โŠ‘_ โ„š family
  lowerbound-of-upperbounds-of-family R R-is-ub q = R-is-ub q โ‹†

  family-is-sup : is-sup _โŠ‘_ โ„š family
  family-is-sup = upperbound-of-family , lowerbound-of-upperbounds-of-family

  family-is-sup' : is-sup (underlying-order (๐“›P โป)) โ„š family
  family-is-sup' = (ฮป q โ†’ โŠ‘-to-๐“›-โŠ‘ (family q) โ„š (upperbound-of-family q)) ,
                   (ฮป โ„ โ„-is-ub โ†’ โŠ‘-to-๐“›-โŠ‘ โ„š โ„
                                   (lowerbound-of-upperbounds-of-family โ„
                                     (ฮป q โ†’ ๐“›-โŠ‘-to-โŠ‘ (family q) โ„ (โ„-is-ub q))))

  โˆหขหข-๏ผ : โˆหขหข ๐“›P family Q-is-prop ๏ผ โ„š
  โˆหขหข-๏ผ = sups-are-unique (underlying-order (๐“›P โป))
                           (poset-axioms-of-dcpo (๐“›P โป))
                           family
                           (โˆหขหข-is-sup ๐“›P family Q-is-prop)
                           family-is-sup'

๐“›P-is-algebraic' : structurally-algebraic (๐“›P โป)
๐“›P-is-algebraic' =
 record
  { index-of-compact-family = ฮป (Q , _) โ†’ ๐Ÿ™ + Q
  ; compact-family = ฮป Q โ†’ add-โŠฅ ๐“›P (family Q)
  ; compact-family-is-directed = ฮด
  ; compact-family-is-compact = ฮบ
  ; compact-family-โˆ-๏ผ = โˆหขหข-๏ผ
  }
   where
    ฮบ : (Q : โŸช ๐“›P โŸซ) (i : ๐Ÿ™ + is-defined Q)
      โ†’ is-compact (๐“›P โป) (add-โŠฅ ๐“›P (family Q) i)
    ฮบ Q (inl _) = โŠฅ-is-compact ๐“›P
    ฮบ Q (inr q) = family-members-are-compact Q q
    ฮด : (Q : โŸจ ๐“›P โป โŸฉ) โ†’ is-Directed (๐“›P โป) (add-โŠฅ ๐“›P (family Q))
    ฮด Q = add-โŠฅ-is-directed ๐“›P
           (subsingleton-indexed-is-semidirected (๐“›P โป)
           (family Q)
           (being-defined-is-prop Q))

๐“›P-is-algebraic : is-algebraic-dcpo (๐“›P โป)
๐“›P-is-algebraic = โˆฃ ๐“›P-is-algebraic' โˆฃ

\end{code}

Since P is a proposition, the lifting of P is not just a dcpo but actually a
sup-lattice. However, it has a greatest element if and only if P is ๐“ฅ small.

\begin{code}

๐“›P-is-sup-complete : is-sup-complete (๐“›P โป)
๐“›P-is-sup-complete = lifting-of-prop-is-sup-complete P-is-prop

greatest-element-gives-resizing : (โŠค : โŸช ๐“›P โŸซ)
                                โ†’ is-greatest _โŠ‘_ โŠค
                                โ†’ P is ๐“ฅ small
greatest-element-gives-resizing (Q , Q-implies-P , Q-is-prop) grt = Q , e
 where
  e : Q โ‰ƒ P
  e = logically-equivalent-props-are-equivalent
       Q-is-prop
       P-is-prop
       Q-implies-P
       (ฮป p โ†’ grt (๐Ÿ™ , (ฮป _ โ†’ p) , ๐Ÿ™-is-prop) โ‹†)

resizing-gives-greatest-element : P is ๐“ฅ small
                                โ†’ ฮฃ โŠค ๊ž‰ โŸช ๐“›P โŸซ , is-greatest _โŠ‘_ โŠค
resizing-gives-greatest-element (Pโ‚€ , e) = โ„™โ‚€ , โ„™โ‚€-is-greatest
 where
  โ„™โ‚€ : โŸช ๐“›P โŸซ
  โ„™โ‚€ = Pโ‚€ , โŒœ e โŒ , equiv-to-prop e P-is-prop
  โ„™โ‚€-is-greatest : is-greatest _โŠ‘_ โ„™โ‚€
  โ„™โ‚€-is-greatest (Q , Q-implies-P , Q-is-prop) q = โŒœ e โŒโปยน (Q-implies-P q)

\end{code}

Since ๐“›P is sup-complete, taking the sup of all elements of a small basis would
produce a greatest element and hence result in the resizing of P.

\begin{code}

๐“›P-has-unspecified-small-basis-resizes : has-unspecified-small-basis (๐“›P โป)
                                       โ†’ P is ๐“ฅ small
๐“›P-has-unspecified-small-basis-resizes scb =
 greatest-element-gives-resizing โŠค โŠค-is-greatest
  where
   grt : ฮฃ โŠค ๊ž‰ โŸช ๐“›P โŸซ , ((Q : โŸช ๐“›P โŸซ) โ†’ Q โŠ‘โŸช ๐“›P โŸซ โŠค)
   grt = greatest-element-if-sup-complete-with-small-basis
          (๐“›P โป) ๐“›P-is-sup-complete scb
   โŠค : โŸช ๐“›P โŸซ
   โŠค = prโ‚ grt
   โŠค-is-greatest : (Q : โŸช ๐“›P โŸซ) โ†’ Q โŠ‘ โŠค
   โŠค-is-greatest Q = ๐“›-โŠ‘-to-โŠ‘ Q โŠค (prโ‚‚ grt Q)

๐“›P-has-unspecified-small-compact-basis-resizes :
   has-unspecified-small-compact-basis (๐“›P โป)
 โ†’ P is ๐“ฅ small
๐“›P-has-unspecified-small-compact-basis-resizes h =
 ๐“›P-has-unspecified-small-basis-resizes
  (โˆฅโˆฅ-functor (ฮป (B , ฮฒ , scb) โ†’ B , ฮฒ , compact-basis-is-basis _ ฮฒ scb) h)

\end{code}

Conversely, if P is ๐“ฅ small, then ๐“›P has a small compact basis.

This is because ๐“› X always has a small compact basis when X : ๐“ฅ. Therefore, if
P โ‰ƒ Pโ‚€ with Pโ‚€ : ๐“ฅ, then we can use the induced isomorphism of dcpos between ๐“› P
and ๐“› Pโ‚€ to equip ๐“› P with a small compact basis.

\begin{code}

resizing-gives-small-compact-basis : P is ๐“ฅ small
                                   โ†’ has-specified-small-compact-basis (๐“›P โป)
resizing-gives-small-compact-basis (Pโ‚€ , e) =
 small-compact-basis-from-โ‰ƒแตˆแถœแต–แต’ pe
  (๐“›-DCPO Pโ‚€-is-set) (๐“›P โป)
  (๐“›ฬ‡-โ‰ƒแตˆแถœแต–แต’ Pโ‚€-is-set P-is-set e)
  scb
  where
   Pโ‚€-is-set : is-set Pโ‚€
   Pโ‚€-is-set = props-are-sets (equiv-to-prop e P-is-prop)
   scb : has-specified-small-compact-basis (๐“›-DCPO Pโ‚€-is-set)
   scb = ๐“›-has-specified-small-compact-basis Pโ‚€-is-set

\end{code}