Martin Escardo, January 2018

Two weak notions of compactness: βˆƒ-compactness and Ξ -compactness. See
the module CompactTypes for the strong notion.

\begin{code}

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

open import MLTT.Spartan

open import CoNaturals.Type
open import MLTT.Two-Properties
open import Notation.Order
open import Taboos.WLPO
open import TypeTopology.CompactTypes
open import TypeTopology.DisconnectedTypes
open import TypeTopology.TotallySeparated
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.Retracts
open import UF.Retracts-FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

module TypeTopology.WeaklyCompactTypes
        (fe : FunExt)
        (pt : propositional-truncations-exist)
       where

private
 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

open PropositionalTruncation pt
open import NotionsOfDecidability.Complemented

is-βˆƒ-compact : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-βˆƒ-compact X = (p : X β†’ 𝟚) β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)

βˆƒ-compactness-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (is-βˆƒ-compact X)
βˆƒ-compactness-is-prop {𝓀} {X} = Ξ -is-prop fe'
                                  (Ξ» _ β†’ decidability-of-prop-is-prop fe'
                                          βˆ₯βˆ₯-is-prop)

βˆƒ-compactness-gives-Markov : {X : 𝓀 Μ‡ }
                           β†’ is-βˆƒ-compact X
                           β†’ (p : X β†’ 𝟚)
                           β†’ ¬¬ (βˆƒ x κž‰ X , p x ＝ β‚€)
                           β†’ βˆƒ x κž‰ X , p x ＝ β‚€
βˆƒ-compactness-gives-Markov {𝓀} {X} c p Ο† = g (c p)
 where
  g : is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€) β†’ βˆƒ x κž‰ X , p x ＝ β‚€
  g (inl e) = e
  g (inr u) = 𝟘-elim (Ο† u)

\end{code}

The relation of βˆƒ-compactness with compactness is the same as that of
LPO with WLPO.

\begin{code}

is-Ξ -compact : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-Ξ -compact X = (p : X β†’ 𝟚) β†’ is-decidable ((x : X) β†’ p x ＝ ₁)

Ξ -compactness-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (is-Ξ -compact X)
Ξ -compactness-is-prop {𝓀} = Ξ -is-prop fe'
                              (Ξ» _ β†’ decidability-of-prop-is-prop fe'
                                       (Ξ -is-prop fe' (Ξ» _ β†’ 𝟚-is-set)))

βˆƒ-compact-types-are-Ξ -compact : {X : 𝓀 Μ‡ } β†’ is-βˆƒ-compact X β†’ is-Ξ -compact X
βˆƒ-compact-types-are-Ξ -compact {𝓀} {X} c p = f (c p)
 where
  f : is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€) β†’ is-decidable (Ξ  x κž‰ X , p x ＝ ₁)
  f (inl s) = inr (Ξ» Ξ± β†’ βˆ₯βˆ₯-rec 𝟘-is-prop (g Ξ±) s)
   where
    g : ((x : X) β†’ p x ＝ ₁) β†’ Β¬ (Ξ£ x κž‰ X , p x ＝ β‚€)
    g Ξ± (x , r) = zero-is-not-one (r ⁻¹ βˆ™ Ξ± x)
  f (inr u) = inl (not-existsβ‚€-implies-forall₁ p u)

empty-types-are-βˆƒ-compact : {X : 𝓀 Μ‡ } β†’ is-empty X β†’ is-βˆƒ-compact X
empty-types-are-βˆƒ-compact u p = inr (βˆ₯βˆ₯-rec 𝟘-is-prop Ξ» Οƒ β†’ u (pr₁ Οƒ))

empty-types-are-Ξ -compact : {X : 𝓀 Μ‡ } β†’ is-empty X β†’ is-Ξ -compact X
empty-types-are-Ξ -compact u p = inl (Ξ» x β†’ 𝟘-elim (u x))

\end{code}

The βˆƒ-compactness, and hence Ξ -compactness, of compact sets (and hence
of β„•βˆž, for example):

\begin{code}

compact-types-are-βˆƒ-compact : {X : 𝓀 Μ‡ } β†’ is-compact X β†’ is-βˆƒ-compact X
compact-types-are-βˆƒ-compact {𝓀} {X} Ο† p = g (Ο† p)
 where
  g : ((Ξ£ x κž‰ X , p x ＝ β‚€) + ((x : X) β†’ p x ＝ ₁))
    β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
  g (inl (x , r)) = inl ∣ x , r ∣
  g (inr Ξ±)       = inr (forall₁-implies-not-existsβ‚€ p Ξ±)

βˆ₯Compactβˆ₯-types-are-βˆƒ-compact : {X : 𝓀 Μ‡ } β†’ βˆ₯ is-Compact X βˆ₯ β†’ is-βˆƒ-compact X
βˆ₯Compactβˆ₯-types-are-βˆƒ-compact {𝓀} {X} =
 βˆ₯βˆ₯-rec
   βˆƒ-compactness-is-prop
   (compact-types-are-βˆƒ-compact ∘ Compact-types-are-compact)

\end{code}

But notice that the Ξ -compactness of β„• is WLPO and its βˆƒ-compactness
is amounts to LPO.

The Ξ -compactness of X is equivalent to the isolatedness of the boolean
predicate Ξ» x β†’ ₁:

\begin{code}

is-Ξ -compact' : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-Ξ -compact' X = is-isolated' (Ξ» (x : X) β†’ ₁)

being-Ξ -compact'-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (is-Ξ -compact' X)
being-Ξ -compact'-is-prop {𝓀} = being-isolated'-is-prop fe (Ξ» x β†’ ₁)

Ξ -compact'-types-are-Ξ -compact : {X : 𝓀 Μ‡ } β†’ is-Ξ -compact' X β†’ is-Ξ -compact X
Ξ -compact'-types-are-Ξ -compact {𝓀} {X} c' p = g (c' p)
 where
  g : is-decidable (p ＝ Ξ» x β†’ ₁) β†’ is-decidable ((x : X) β†’ p x ＝ ₁)
  g (inl r) = inl (happly r)
  g (inr u) = inr (contrapositive (dfunext fe') u)

Ξ -compact-types-are-Ξ -compact' : {X : 𝓀 Μ‡ } β†’ is-Ξ -compact X β†’ is-Ξ -compact' X
Ξ -compact-types-are-Ξ -compact' {𝓀} {X} c p = g (c p)
 where
  g : is-decidable ((x : X) β†’ p x ＝ ₁) β†’ is-decidable (p ＝ Ξ» x β†’ ₁)
  g (inl Ξ±) = inl (dfunext fe' Ξ±)
  g (inr u) = inr (contrapositive happly u)

\end{code}

In classical topology, the Tychonoff Theorem gives that compact to the
power discrete is compact (where we read the function type X β†’ Y as "Y
to the power X", with Y the base and X the exponent, and call it an
exponential). Here we don't have the Tychonoff Theorem (in the absence
of anti-classical intuitionistic assumptions).

It is less well-known that in classical topology we also have that
discrete to the power compact is discrete. This we do have here,
without the need of any assumption:

\begin{code}

discrete-to-power-Ξ -compact-is-discrete : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                        β†’ is-Ξ -compact X
                                        β†’ is-discrete Y
                                        β†’ is-discrete (X β†’ Y)
discrete-to-power-Ξ -compact-is-discrete {𝓀} {π“₯} {X} {Y} c d f g = Ξ΄
 where
  p : X β†’ 𝟚
  p = pr₁ (co-characteristic-function (Ξ» x β†’ d (f x) (g x)))

  r : (x : X) β†’ (p x ＝ β‚€ β†’ Β¬ (f x ＝ g x)) Γ— (p x ＝ ₁ β†’ f x ＝ g x)
  r = prβ‚‚ (co-characteristic-function Ξ» x β†’ d (f x) (g x))

  Ο† : ((x : X) β†’ p x ＝ ₁) β†’ f ＝ g
  Ο† Ξ± = dfunext fe' (Ξ» x β†’ prβ‚‚ (r x) (Ξ± x))

  Ξ³ : f ＝ g β†’ (x : X) β†’ p x ＝ ₁
  Ξ³ t x = different-from-β‚€-equal-₁ (Ξ» u β†’ pr₁ (r x) u (happly t x))

  h : is-decidable ((x : X) β†’ p x ＝ ₁) β†’ is-decidable (f ＝ g)
  h (inl Ξ±) = inl (Ο† Ξ±)
  h (inr u) = inr (contrapositive Ξ³ u)

  δ : is-decidable (f ＝ g)
  Ξ΄ = h (c p)

\end{code}

If an exponential with discrete base is discrete, then its exponent is
compact, provided the base has at least two points.

First, to decide Ξ  (p : X β†’ 𝟚), p x ＝ 1, decide p ＝ Ξ» x β†’ ₁:

\begin{code}

power-of-two-discrete-gives-compact-exponent : {X : 𝓀 Μ‡ }
                                             β†’ is-discrete (X β†’ 𝟚)
                                             β†’ is-Ξ -compact X
power-of-two-discrete-gives-compact-exponent d =
 Ξ -compact'-types-are-Ξ -compact (Ξ» p β†’ d p (Ξ» x β†’ ₁))

discrete-power-of-disconnected-gives-compact-exponent : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                                      β†’ is-disconnected Y
                                                      β†’ is-discrete (X β†’ Y)
                                                      β†’ is-Ξ -compact X
discrete-power-of-disconnected-gives-compact-exponent {𝓀} {π“₯} {X} {Y} ρ d = Ξ³
 where
  a : retract (X β†’ 𝟚) of (X β†’ Y)
  a = retract-contravariance fe' ρ

  b : is-discrete (X β†’ 𝟚)
  b = retract-is-discrete a d

  Ξ³ : is-Ξ -compact X
  Ξ³ = power-of-two-discrete-gives-compact-exponent b

discrete-power-of-non-trivial-discrete-gives-compact-exponent' :

    {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
  β†’ (Ξ£ yβ‚€ κž‰ Y , Ξ£ y₁ κž‰ Y , yβ‚€ β‰  y₁)
  β†’ is-discrete Y
  β†’ is-discrete (X β†’ Y)
  β†’ is-Ξ -compact X

discrete-power-of-non-trivial-discrete-gives-compact-exponent' w d =
  discrete-power-of-disconnected-gives-compact-exponent
   (discrete-types-with-two-different-points-are-disconnected w d)

\end{code}

So, in summary, if Y is a non-trivial discrete type, then X is
Ξ -compact iff (X β†’ Y) is discrete.

Compactness of images:

\begin{code}

open import UF.ImageAndSurjection pt

codomain-of-surjection-is-βˆƒ-compact : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                    β†’ is-surjection f
                                    β†’ is-βˆƒ-compact X
                                    β†’ is-βˆƒ-compact Y
codomain-of-surjection-is-βˆƒ-compact {𝓀} {π“₯} {X} {Y} f su c q = g (c (q ∘ f))
 where
  h : (Ξ£ x κž‰ X , q (f x) ＝ β‚€) β†’ Ξ£ y κž‰ Y , q y ＝ β‚€
  h (x , r) = (f x , r)

  l : (y : Y) β†’ q y ＝ β‚€ β†’ (Ξ£ x κž‰ X , f x ＝ y) β†’ Ξ£ x κž‰ X , q (f x) ＝ β‚€
  l y r (x , s) = (x , (ap q s βˆ™ r))

  k : (Ξ£ y κž‰ Y , q y ＝ β‚€) β†’ βˆƒ x κž‰ X , q (f x) ＝ β‚€
  k (y , r) = βˆ₯βˆ₯-functor (l y r) (su y)

  g : is-decidable (βˆƒ x κž‰ X , q (f x) ＝ β‚€)Β β†’ is-decidable (βˆƒ y κž‰ Y , q y ＝ β‚€)
  g (inl s) = inl (βˆ₯βˆ₯-functor h s)
  g (inr u) = inr (contrapositive (βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop k) u)

image-is-βˆƒ-compact : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                   β†’ is-βˆƒ-compact X
                   β†’ is-βˆƒ-compact (image f)
image-is-βˆƒ-compact f = codomain-of-surjection-is-βˆƒ-compact (corestriction f) (corestrictions-are-surjections f)

codomain-of-surjection-is-Ξ -compact : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                    β†’ is-surjection f
                                    β†’ is-Ξ -compact X
                                    β†’ is-Ξ -compact Y
codomain-of-surjection-is-Ξ -compact {𝓀} {π“₯} {X} {Y} f su c q = g (c (q ∘ f))
 where
  g : is-decidable ((x : X) β†’ q (f x) ＝ ₁) β†’ is-decidable ((x : Y) β†’ q x ＝ ₁)
  g (inl s) = inl (surjection-induction f su (Ξ» y β†’ q y ＝ ₁) (Ξ» _ β†’ 𝟚-is-set) s)
  g (inr u) = inr (contrapositive (Ξ» Ο† x β†’ Ο† (f x)) u)

retract-βˆƒ-compact : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                  β†’ retract Y of X
                  β†’ is-βˆƒ-compact X
                  β†’ is-βˆƒ-compact Y
retract-βˆƒ-compact (f , hass) = codomain-of-surjection-is-βˆƒ-compact f
                                (retractions-are-surjections f hass)

retract-is-βˆƒ-compact' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                      β†’ βˆ₯ retract Y of X βˆ₯
                      β†’ is-βˆƒ-compact X
                      β†’ is-βˆƒ-compact Y
retract-is-βˆƒ-compact' t c = βˆ₯βˆ₯-rec
                             βˆƒ-compactness-is-prop
                              (Ξ» r β†’ retract-βˆƒ-compact r c) t

image-is-Ξ -compact : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                   β†’ is-Ξ -compact X
                  β†’ is-Ξ -compact (image f)
image-is-Ξ -compact f = codomain-of-surjection-is-Ξ -compact
                        (corestriction f)
                        (corestrictions-are-surjections f)

retract-is-Ξ -compact : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     β†’ retract Y of X
                     β†’ is-Ξ -compact X
                     β†’ is-Ξ -compact Y
retract-is-Ξ -compact (f , hass) = codomain-of-surjection-is-Ξ -compact f
                                   (retractions-are-surjections f hass)

retract-is-Ξ -compact' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                      β†’ βˆ₯ retract Y of X βˆ₯
                      β†’ is-Ξ -compact X
                      β†’ is-Ξ -compact Y
retract-is-Ξ -compact' t c = βˆ₯βˆ₯-rec
                             Ξ -compactness-is-prop
                             (Ξ» r β†’ retract-is-Ξ -compact r c) t

Ξ -compact-exponential-with-pointed-domain-has-Ξ -compact-domain :

    {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
  β†’ X
  β†’ is-Ξ -compact (X β†’ Y)
  β†’ is-Ξ -compact Y

Ξ -compact-exponential-with-pointed-domain-has-Ξ -compact-domain x =
 retract-is-Ξ -compact (codomain-is-retract-of-function-space-with-pointed-domain x)

\end{code}

A main reason to consider the notion of total separatedness is that
the totally separated reflection 𝕋 X of X has the same supply of
boolean-valued predicates as X, and hence X is βˆƒ-compact (respectively
Ξ -compact) iff 𝕋 X is, as we show now.

\begin{code}

module _ (X : 𝓀 Μ‡ ) where

 open totally-separated-reflection fe pt

 private
  EP : (p : X β†’ 𝟚) β†’ βˆƒ! p' κž‰ (𝕋 X β†’ 𝟚) , p' ∘ Ξ· ＝ p
  EP = totally-separated-reflection 𝟚-is-totally-separated

  extension : (X β†’ 𝟚) β†’ (𝕋 X β†’ 𝟚)
  extension p = βˆƒ!-witness (EP p)

  extension-property : (p : X β†’ 𝟚) (x : X) β†’ extension p (Ξ· x) ＝ p x
  extension-property p = happly (βˆƒ!-is-witness (EP p))

 βˆƒ-compact-types-are-βˆƒ-compact-𝕋 : is-βˆƒ-compact X β†’ is-βˆƒ-compact (𝕋 X)
 βˆƒ-compact-types-are-βˆƒ-compact-𝕋 = codomain-of-surjection-is-βˆƒ-compact
                                    Ξ· Ξ·-is-surjection

 βˆƒ-compact-𝕋-types-are-βˆƒ-compact : is-βˆƒ-compact (𝕋 X) β†’ is-βˆƒ-compact X
 βˆƒ-compact-𝕋-types-are-βˆƒ-compact c p = h (c (extension p))
  where
   f : (Ξ£ x' κž‰ 𝕋 X , extension p x' ＝ β‚€) β†’ βˆƒ x κž‰ X , p x ＝ β‚€
   f (x' , r) = βˆ₯βˆ₯-functor f' (Ξ·-is-surjection x')
    where
     f' : (Ξ£ x κž‰ X , Ξ· x ＝ x') β†’ Ξ£ x κž‰ X , p x ＝ β‚€
     f' (x , s) = x , ((extension-property p x) ⁻¹ βˆ™ ap (extension p) s βˆ™ r)

   g : (Ξ£ x κž‰ X , p x ＝ β‚€)
     β†’ Ξ£ x' κž‰ 𝕋 X , extension p x' ＝ β‚€
   g (x , r) = Ξ· x , (extension-property p x βˆ™ r)

   h : is-decidable (βˆƒ x' κž‰ 𝕋 X , extension p x' ＝ β‚€)
     β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
   h (inl x) = inl (βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop f x)
   h (inr u) = inr (contrapositive (βˆ₯βˆ₯-functor g) u)

 Ξ -compact-types-are-Ξ -compact-𝕋 : is-Ξ -compact X β†’ is-Ξ -compact (𝕋 X)
 Ξ -compact-types-are-Ξ -compact-𝕋 = codomain-of-surjection-is-Ξ -compact
                                    Ξ· (Ξ·-is-surjection)

 Ξ -compact-𝕋-types-are-Ξ -compact : is-Ξ -compact (𝕋 X) β†’ is-Ξ -compact X
 Ξ -compact-𝕋-types-are-Ξ -compact c p = h (c (extension p))
  where
   f : ((x' : 𝕋 X) β†’ extension p x' ＝ ₁) β†’ ((x : X) β†’ p x ＝ ₁)
   f Ξ± x = (extension-property p x)⁻¹ βˆ™ Ξ± (Ξ· x)

   g : (Ξ± : (x : X) β†’ p x ＝ ₁)
     β†’ ((x' : 𝕋 X) β†’ extension p x' ＝ ₁)
   g Ξ± = Ξ·-induction (Ξ» x' β†’ extension p x' ＝ ₁) (Ξ» _ β†’ 𝟚-is-set) g'
     where
      g' : (x : X) β†’ extension p (Ξ· x) ＝ ₁
      g' x = extension-property p x βˆ™ Ξ± x

   h : is-decidable ((x' : 𝕋 X) β†’ extension p x' ＝ ₁)
     β†’ is-decidable ((x : X) β†’ p x ＝ ₁)
   h (inl Ξ±) = inl (f Ξ±)
   h (inr u) = inr (contrapositive g u)

\end{code}

If X is totally separated, and (X β†’ 𝟚) is compact, then X is
discrete. More generally, if 𝟚 is a retract of Y and (X β†’ Y) is
compact, then X is discrete if it is totally separated. This is a new
result as far as I know. I didn't know it before 12th January 2018.

The following proof works as follows. For any given x,y:X, define
q:(Xβ†’πŸš)β†’πŸš such that q(p)=1 ↔ p(x) = p(y), which is possible because 𝟚
has decidable equality (it is discrete). By the Ξ -compactness of Xβ†’πŸš,
the condition (p:Xβ†’πŸš) β†’ q(p)=1 is decidable, which amounts to saying
that (p:Xβ†’πŸš) β†’ p (x)=p (y) is decidable. But because X is totally
separated, the latter is equivalent to x=y, which shows that X is
discrete.

\begin{code}

tscd : {X : 𝓀 Μ‡ }
     β†’ is-totally-separated X
     β†’ is-Ξ -compact (X β†’ 𝟚)
     β†’ is-discrete X
tscd {𝓀} {X} ts c x y = g (a s)
 where
  q : (X β†’ 𝟚) β†’ 𝟚
  q = pr₁ (co-characteristic-function (Ξ» p β†’ 𝟚-is-discrete (p x) (p y)))

  r : (p : X β†’ 𝟚) β†’ (q p ＝ β‚€ β†’ p x β‰  p y) Γ— (q p ＝ ₁ β†’ p x ＝ p y)
  r = prβ‚‚ (co-characteristic-function (Ξ» p β†’ 𝟚-is-discrete (p x) (p y)))

  s : is-decidable ((p : X β†’ 𝟚) β†’ q p ＝ ₁)
  s = c q

  b : (p : X β†’ 𝟚) β†’ p x ＝ p y β†’ q p ＝ ₁
  b p u = different-from-β‚€-equal-₁ (Ξ» v β†’ pr₁ (r p) v u)

  a : is-decidable ((p : X β†’ 𝟚) β†’ q p ＝ ₁)
    β†’ is-decidable ((p : X β†’ 𝟚) β†’ p x ＝ p y)
  a (inl f) = inl (Ξ» p β†’ prβ‚‚ (r p) (f p))
  a (inr Ο†) = inr h
   where
    h : Β¬ ((p : X β†’ 𝟚) β†’ p x ＝ p y)
    h Ξ± = Ο† (Ξ» p β†’ b p (Ξ± p))

  g : is-decidable ((p : X β†’ 𝟚) β†’ p x ＝ p y) β†’ is-decidable (x ＝ y)
  g (inl Ξ±) = inl (ts Ξ±)
  g (inr u) = inr (contrapositive (Ξ» e p β†’ ap p e) u)

\end{code}

We are interested in the following two generalizations, which arise as
corollaries:

\begin{code}

tscdβ‚€ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ is-totally-separated X
      β†’ is-disconnected Y
      β†’ is-Ξ -compact (X β†’ Y)
      β†’ is-discrete X
tscdβ‚€ {𝓀} {π“₯} {X} {Y} ts r c =
 tscd ts (retract-is-Ξ -compact (retract-contravariance fe' r) c)

open totally-separated-reflection fe pt

tscd₁ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
      β†’ is-disconnected Y
      β†’ is-Ξ -compact (X β†’ Y)
      β†’ is-discrete (𝕋 X)
tscd₁ {𝓀} {π“₯} {X} {Y} r c = f
 where
  z : retract (X β†’ 𝟚) of (X β†’ Y)
  z = retract-contravariance fe' r

  a : (𝕋 X β†’ 𝟚) ≃ (X β†’ 𝟚)
  a = totally-separated-reflection'' 𝟚-is-totally-separated

  b : retract (𝕋 X β†’ 𝟚) of (X β†’ 𝟚)
  b = ≃-gives-◁ a

  d : retract (𝕋 X β†’ 𝟚) of (X β†’ Y)
  d = retracts-compose z b

  e : is-Ξ -compact (𝕋 X β†’ 𝟚)
  e = retract-is-Ξ -compact d c

  f : is-discrete (𝕋 X)
  f = tscd Ο„ e

\end{code}

In topological models, Ξ -compactness is the same as topological
compactess in the presence of total separatedness, at least for some
spaces, including the Kleene-Kreisel spaces, which model the simple
types (see the module SimpleTypes). Hence, for example, the
topological space (β„•βˆžβ†’πŸš) is not Ξ -compact because it is countably
discrete, as it is a theorem of topology that discrete to the power
compact is again discrete, which is compact iff it is finite. This
argument is both classical and external. But here we have that the
type (β„•βˆžβ†’πŸš) is "not" Ξ -compact, internally and constructively.

\begin{code}

[β„•βˆžβ†’πŸš]-compact-implies-WLPO : is-Ξ -compact (β„•βˆž β†’ 𝟚) β†’ WLPO
[β„•βˆžβ†’πŸš]-compact-implies-WLPO c = β„•βˆž-discrete-gives-WLPO
                                  (tscd (β„•βˆž-is-totally-separated fe') c)

\end{code}

Closure of compactness under sums (and hence binary products):

\begin{code}

Ξ -compact-closed-under-Ξ£ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
                         β†’ is-Ξ -compact X
                         β†’ ((x : X) β†’ is-Ξ -compact (Y x))
                         β†’ is-Ξ -compact (Ξ£ Y)
Ξ -compact-closed-under-Ξ£ {𝓀} {π“₯} {X} {Y} c d p = g e
 where
  f : βˆ€ x β†’ is-decidable (βˆ€ y β†’ p (x , y) ＝ ₁)
  f x = d x (Ξ» y β†’ p (x , y))

  q : X β†’ 𝟚
  q = pr₁ (co-characteristic-function f)

  qβ‚€ : (x : X) β†’ q x ＝ β‚€ β†’ Β¬ ((y : Y x) β†’ p (x , y) ＝ ₁)
  qβ‚€ x = pr₁ (prβ‚‚ (co-characteristic-function f) x)

  q₁ : (x : X) β†’ q x ＝ ₁ β†’ (y : Y x) β†’ p (x , y) ＝ ₁
  q₁ x = prβ‚‚ (prβ‚‚ (co-characteristic-function f) x)

  e : is-decidable (βˆ€ x β†’ q x ＝ ₁)
  e = c q

  g : is-decidable (βˆ€ x β†’ q x ＝ ₁) β†’ is-decidable (βˆ€ Οƒ β†’ p Οƒ ＝ ₁)
  g (inl Ξ±) = inl h
   where
    h : (Οƒ : Ξ£ Y) β†’ p Οƒ ＝ ₁
    h (x , y) = q₁ x (Ξ± x) y
  g (inr u) = inr (contrapositive h u)
   where
    h : ((Οƒ : Ξ£ Y) β†’ p Οƒ ＝ ₁) β†’ (x : X) β†’ q x ＝ ₁
    h Ξ² x = different-from-β‚€-equal-₁ (Ξ» r β†’ qβ‚€ x r (Ξ» y β†’ Ξ² (x , y)))

\end{code}

TODO. Consider also other possible closure properties, and
βˆƒ-compactness.

We now turn to propositions. A proposition is βˆƒ-compact iff it is
decidable. Regarding the compactness of propositions, we have partial
information for the moment.

\begin{code}

βˆƒ-compact-propositions-are-decidable : (X : 𝓀 Μ‡ )
                                     β†’ is-prop X
                                     β†’ is-βˆƒ-compact X
                                     β†’ is-decidable X
βˆƒ-compact-propositions-are-decidable X isp c = f a
 where
  a : is-decidable βˆ₯ X Γ— (β‚€ ＝ β‚€) βˆ₯
  a = c (Ξ» x β†’ β‚€)

  f : is-decidable βˆ₯ X Γ— (β‚€ ＝ β‚€) βˆ₯ β†’ is-decidable X
  f (inl s) = inl (βˆ₯βˆ₯-rec isp pr₁ s)
  f (inr u) = inr (Ξ» x β†’ u ∣ x , refl ∣)

βˆƒ-compact-types-have-decidable-support : {X : 𝓀 Μ‡ }
                                       β†’ is-βˆƒ-compact X
                                       β†’ is-decidable βˆ₯ X βˆ₯
βˆƒ-compact-types-have-decidable-support {𝓀} {X} c =
 βˆƒ-compact-propositions-are-decidable βˆ₯ X βˆ₯ βˆ₯βˆ₯-is-prop
  (codomain-of-surjection-is-βˆƒ-compact ∣_∣ pt-is-surjection c)

βˆƒ-compact-non-empty-types-are-inhabited : {X : 𝓀 Μ‡ }
                                        β†’ is-βˆƒ-compact X
                                        β†’ ¬¬ X
                                        β†’ βˆ₯ X βˆ₯
βˆƒ-compact-non-empty-types-are-inhabited {𝓀} {X} c Ο† = g (βˆƒ-compact-types-have-decidable-support c)
 where
  g : is-decidable βˆ₯ X βˆ₯ β†’ βˆ₯ X βˆ₯
  g (inl s) = s
  g (inr u) = 𝟘-elim (Ο† (Ξ» x β†’ u ∣ x ∣))

decidable-propositions-are-βˆƒ-compact : (X : 𝓀 Μ‡ )
                                     β†’ is-prop X
                                     β†’ is-decidable X
                                     β†’ is-βˆƒ-compact X
decidable-propositions-are-βˆƒ-compact X isp d p = g d
 where
  g : is-decidable X β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
  g (inl x) = 𝟚-equality-cases b c
   where
    b : p x ＝ β‚€ β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
    b r = inl ∣ x , r ∣

    c : p x ＝ ₁ β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
    c r = inr (βˆ₯βˆ₯-rec (𝟘-is-prop) f)
     where
      f : Β¬ (Ξ£ y κž‰ X , p y ＝ β‚€)
      f (y , q) = zero-is-not-one (transport (Ξ» - β†’ p - ＝ β‚€) (isp y x) q ⁻¹ βˆ™ r)

  g (inr u) = inr (βˆ₯βˆ₯-rec 𝟘-is-prop (Ξ» Οƒ β†’ u (pr₁ Οƒ)))

negations-of-Ξ -compact-propositions-are-decidable : (X : 𝓀 Μ‡ )
                                                  β†’ is-prop X
                                                  β†’ is-Ξ -compact X
                                                  β†’ is-decidable (Β¬ X)
negations-of-Ξ -compact-propositions-are-decidable X isp c = f a
 where
  a : is-decidable (X β†’ β‚€ ＝ ₁)
  a = c (Ξ» x β†’ β‚€)

  f : is-decidable (X β†’ β‚€ ＝ ₁) β†’ is-decidable (Β¬ X)
  f (inl u) = inl (zero-is-not-one  ∘ u)
  f (inr Ο†) = inr (Ξ» u β†’ Ο† (Ξ» x β†’ 𝟘-elim (u x)))

negations-of-propositions-whose-decidability-is-Ξ -compact-are-decidable :

    (X : 𝓀 Μ‡ )
  β†’ is-prop X
  β†’ is-Ξ -compact (is-decidable X)
  β†’ is-decidable (Β¬ X)

negations-of-propositions-whose-decidability-is-Ξ -compact-are-decidable X isp c = Cases a l m
 where
  p : X + Β¬ X β†’ 𝟚
  p (inl x) = β‚€
  p (inr u) = ₁

  a : is-decidable ((z : X + Β¬ X) β†’ p z ＝ ₁)
  a = c p

  l : ((z : X + Β¬ X) β†’ p z ＝ ₁) β†’ Β¬ X + ¬¬ X
  l Ξ± = inl (Ξ» x β†’ 𝟘-elim (zero-is-not-one (Ξ± (inl x))))

  Ξ± : (u : X β†’ 𝟘) (z : X + Β¬ X) β†’ p z ＝ ₁
  α u (inl x) = 𝟘-elim (u x)
  Ξ± u (inr v) = refl

  m : Β¬ ((z : X + Β¬ X) β†’ p z ＝ ₁) β†’ Β¬ X + ¬¬ X
  m Ο† = inr (Ξ» u β†’ Ο† (Ξ± u))

\end{code}

8th Feb 2018: A pointed detachable subset of any type is a
retract. Hence any detachable (pointed or not) subset of a βˆƒ-compact
type is compact. The first construction should probably go to another
module.

\begin{code}

detachable-subset-retract : {X : 𝓀 Μ‡ } {A : X β†’ 𝟚}
                          β†’ (Ξ£ x κž‰ X , A x ＝ β‚€)
                          β†’ retract (Ξ£ x κž‰ X , A x ＝ β‚€) of X
detachable-subset-retract {𝓀} {X} {A} (xβ‚€ , eβ‚€) = r , pr₁ , rs
 where
  r : X β†’ Ξ£ x κž‰ X , A x ＝ β‚€
  r x = 𝟚-equality-cases
         (Ξ» (e : A x ＝ β‚€) β†’ (x , e))
         (Ξ» (e : A x ＝ ₁) β†’ (xβ‚€ , eβ‚€))

  rs : (Οƒ : Ξ£ x κž‰ X , A x ＝ β‚€) β†’ r (pr₁ Οƒ) ＝ Οƒ
  rs (x , e) = w
   where
    s : (b : 𝟚) β†’ b ＝ β‚€ β†’ 𝟚-equality-cases
                           (Ξ» (_ : b ＝ β‚€) β†’ (x , e))
                           (Ξ» (_ : b ＝ ₁) β†’ (xβ‚€ , eβ‚€)) ＝ (x , e)
    s β‚€ refl = refl
    s ₁ r = 𝟘-elim (one-is-not-zero r)

    t : 𝟚-equality-cases
         (Ξ» (_ : A x ＝ β‚€) β†’ x , e)
         (Ξ» (_ : A x ＝ ₁) β†’ xβ‚€ , eβ‚€)
      ＝ (x , e)
    t = s (A x) e

    u : (Ξ» e' β†’ x , e') ＝ (Ξ» _ β†’ x , e)
    u = dfunext fe' Ξ» e' β†’ ap (Ξ» - β†’ (x , -)) (𝟚-is-set e' e)

    v : r x ＝ 𝟚-equality-cases
               (Ξ» (_ : A x ＝ β‚€) β†’ x , e)
               (Ξ» (_ : A x ＝ ₁) β†’ xβ‚€ , eβ‚€)
    v = ap (Ξ» - β†’ 𝟚-equality-cases - (Ξ» (_ : A x ＝ ₁) β†’ xβ‚€ , eβ‚€)) u

    w : r x ＝ x , e
    w = v βˆ™ t

\end{code}

Notice that in the above lemma we need to assume that the detachable
set is pointed. But its use below doesn't, because βˆƒ-compactness
allows us to decide inhabitedness, and βˆƒ-compactness is a proposition.

\begin{code}

detachable-subset-βˆƒ-compact : {X : 𝓀 Μ‡ } (A : X β†’ 𝟚)
                            β†’ is-βˆƒ-compact X
                            β†’ is-βˆƒ-compact (Ξ£ x κž‰ X , A x ＝ β‚€)
detachable-subset-βˆƒ-compact {𝓀} {X} A c = g (c A)
 where
  g : is-decidable (βˆƒ x κž‰ X , A x ＝ β‚€) β†’ is-βˆƒ-compact (Ξ£ x κž‰ X , A (x) ＝ β‚€)
  g (inl e) = retract-is-βˆƒ-compact' (βˆ₯βˆ₯-functor detachable-subset-retract e) c
  g (inr u) = empty-types-are-βˆƒ-compact (contrapositive ∣_∣ u)

\end{code}

For the compact case, the retraction method to prove the last theorem
is not available, but the conclusion holds, with some of the same
ingredients (and with a longer proof (is there a shorter one?)).

\begin{code}

complemented-subtype-is-Ξ -compact : {X : 𝓀 Μ‡ } (A : X β†’ 𝟚)
                                  β†’ is-Ξ -compact X
                                  β†’ is-Ξ -compact (Ξ£ x κž‰ X , A x ＝ ₁)
complemented-subtype-is-Ξ -compact {𝓀} {X} A c q = g (c p)
 where
  pβ‚€ : (x : X) β†’ A x ＝ β‚€ β†’ 𝟚
  pβ‚€ x e = ₁

  p₁ : (x : X) β†’ A x ＝ ₁ β†’ 𝟚
  p₁ x e = q (x , e)

  p : X β†’ 𝟚
  p x = 𝟚-equality-cases (pβ‚€ x) (p₁ x)

  p-specβ‚€ : (x : X) β†’ A x ＝ β‚€ β†’ p x ＝ ₁
  p-specβ‚€ x e = s (A x) e (p₁ x)
   where
    s : (b : 𝟚) β†’ b ＝ β‚€ β†’ (f₁ : b ＝ ₁ β†’ 𝟚)
      β†’ 𝟚-equality-cases (Ξ» (_ : b ＝ β‚€) β†’ ₁) f₁ ＝ ₁
    s β‚€ refl = Ξ» f₁ β†’ refl
    s ₁ r = 𝟘-elim (one-is-not-zero r)

  p-spec₁ : (x : X) (e : A x ＝ ₁) β†’ p x ＝ q (x , e)
  p-spec₁ x e = u βˆ™ t
   where
    y : A x ＝ ₁ β†’ 𝟚
    y _ = q (x , e)

    r : p₁ x ＝ y
    r = dfunext fe' (Ξ» e' β†’ ap (p₁ x) (𝟚-is-set e' e))

    s : (b : 𝟚)
      β†’ b ＝ ₁
      β†’ 𝟚-equality-cases
         (Ξ» (_ : b ＝ β‚€) β†’ ₁)
         (Ξ» (_ : b ＝ ₁) β†’ q (x , e))
      ＝ q (x , e)
    s β‚€ r = 𝟘-elim (zero-is-not-one r)
    s ₁ refl = refl

    t : 𝟚-equality-cases (pβ‚€ x) y ＝ q (x , e)
    t = s (A x) e

    u : p x ＝ 𝟚-equality-cases (pβ‚€ x) y
    u = ap (𝟚-equality-cases (pβ‚€ x)) r

  g : is-decidable ((x : X) β†’ p x ＝ ₁)
    β†’ is-decidable ((Οƒ : Ξ£ x κž‰ X , A x ＝ ₁) β†’ q Οƒ ＝ ₁)
  g (inl Ξ±) = inl h
   where
    h : (Οƒ : Ξ£ x κž‰ X , A x ＝ ₁) β†’ q Οƒ ＝ ₁
    h (x , e) = (p-spec₁ x e) ⁻¹ βˆ™ Ξ± x
  g (inr u) = inr (contrapositive h u)
   where
    h : ((Οƒ : Ξ£ x κž‰ X , A x ＝ ₁) β†’ q Οƒ ＝ ₁) β†’ (x : X) β†’ p x ＝ ₁
    h Ξ² x = 𝟚-equality-cases (p-specβ‚€ x) (Ξ» e β†’ p-spec₁ x e βˆ™ Ξ² (x , e))

\end{code}

20 Jan 2018.

We now consider a truncated version of pointed compactness (see the
module CompactTypes).

\begin{code}

is-βˆƒ-compactβˆ™ : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-βˆƒ-compactβˆ™ X = (p : X β†’ 𝟚) β†’ βˆƒ xβ‚€ κž‰ X , (p xβ‚€ ＝ ₁ β†’ (x : X) β†’ p x ＝ ₁)

βˆƒ-compactnessβˆ™-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (is-βˆƒ-compactβˆ™ X)
βˆƒ-compactnessβˆ™-is-prop {𝓀} = Ξ -is-prop fe' (Ξ» _ β†’ βˆ₯βˆ₯-is-prop)

\end{code}

Notice that, in view of the above results, inhabitedness can be
replaced by non-emptiness in the following results:

\begin{code}

βˆƒ-compactβˆ™-types-are-inhabited-and-compact : {X : 𝓀 Μ‡ }
                                           β†’ is-βˆƒ-compactβˆ™ X
                                           β†’ βˆ₯ X βˆ₯ Γ— is-βˆƒ-compact X
βˆƒ-compactβˆ™-types-are-inhabited-and-compact {𝓀} {X} c = Ξ³
 where
  g₁ : βˆ₯ Ξ£ (Ξ» xβ‚€ β†’ β‚€ ＝ ₁ β†’ (x : X) β†’ β‚€ ＝ ₁) βˆ₯
  g₁ = c (Ξ» x β†’ β‚€)

  gβ‚‚ : (p : X β†’ 𝟚)
     β†’ (Ξ£ xβ‚€ κž‰ X , (p xβ‚€ ＝ ₁ β†’ (x : X) β†’ p x ＝ ₁))
     β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
  gβ‚‚ p (xβ‚€ , Ο†) = h (𝟚-is-discrete (p xβ‚€) ₁)
   where
    h : is-decidable (p xβ‚€ ＝ ₁) β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
    h (inl r) = inr (βˆ₯βˆ₯-rec 𝟘-is-prop f)
     where
      f : Β¬ (Ξ£ x κž‰ X , p x ＝ β‚€)
      f (x , s) = zero-is-not-one (s ⁻¹ βˆ™ Ο† r x)
    h (inr u) = inl ∣ xβ‚€ , (different-from-₁-equal-β‚€ u) ∣

  Ξ³ : βˆ₯ X βˆ₯ Γ— is-βˆƒ-compact X
  Ξ³ = βˆ₯βˆ₯-functor pr₁ g₁ ,
      (Ξ» p β†’ βˆ₯βˆ₯-rec (decidability-of-prop-is-prop fe' βˆ₯βˆ₯-is-prop)
               (gβ‚‚ p) (c p))

inhabited-and-compact-types-are-βˆƒ-compactβˆ™ : {X : 𝓀 Μ‡ }
                                           β†’ βˆ₯ X βˆ₯ Γ— is-βˆƒ-compact X
                                           β†’ is-βˆƒ-compactβˆ™ X
inhabited-and-compact-types-are-βˆƒ-compactβˆ™ {𝓀} {X} (t , c) p = Ξ³
 where
  f : X β†’ βˆƒ xβ‚€ κž‰ X , (p xβ‚€ ＝ ₁ β†’ (x : X) β†’ p x ＝ ₁)
  f xβ‚€ = g (𝟚-is-discrete (p xβ‚€) β‚€) (c p)
   where
    g : is-decidable (p xβ‚€ ＝ β‚€)
      β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
      β†’ βˆƒ xβ‚€ κž‰ X , (p xβ‚€ ＝ ₁ β†’ (x : X) β†’ p x ＝ ₁)
    g (inl r) _       = ∣ xβ‚€ , (Ξ» s _ β†’ 𝟘-elim (zero-is-not-one (r ⁻¹ βˆ™ s))) ∣
    g (inr _) (inl t) = βˆ₯βˆ₯-functor h t
     where
      h : (Ξ£ x κž‰ X , p x ＝ β‚€) β†’ Ξ£ xβ‚€ κž‰ X , (p xβ‚€ ＝ ₁ β†’ (x : X) β†’ p x ＝ ₁)
      h (x , r) = x , Ξ» s _ β†’ 𝟘-elim (zero-is-not-one (r ⁻¹ βˆ™ s))
    g (inr _) (inr v) = ∣ xβ‚€ , (Ξ» _ β†’ not-existsβ‚€-implies-forall₁ p v) ∣

  Ξ³ : βˆƒ xβ‚€ κž‰ X , (p xβ‚€ ＝ ₁ β†’ (x : X) β†’ p x ＝ ₁)
  Ξ³ = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop f t

\end{code}

This characterizes the βˆƒ-compactβˆ™ types as those that are βˆƒ-compact
and inhabited. We can also characterize the βˆƒ-compact types as those
that are βˆƒ-compactβˆ™ or empty:

\begin{code}

being-βˆƒ-compactβˆ™-and-empty-is-prop : {X : 𝓀 Μ‡ }
                                   β†’ is-prop (is-βˆƒ-compactβˆ™ X + is-empty X)
being-βˆƒ-compactβˆ™-and-empty-is-prop {𝓀} {X} =
 sum-of-contradictory-props
  βˆƒ-compactnessβˆ™-is-prop
  (Ξ -is-prop fe'
    (Ξ» _ β†’ 𝟘-is-prop))
  (Ξ» c u β†’ βˆ₯βˆ₯-rec 𝟘-is-prop (contrapositive pr₁ u) (c (Ξ» _ β†’ β‚€)))

βˆƒ-compactβˆ™-or-empty-types-are-βˆƒ-compact : {X : 𝓀 Μ‡ }
                                        β†’ is-βˆƒ-compactβˆ™ X + is-empty X
                                        β†’ is-βˆƒ-compact X
βˆƒ-compactβˆ™-or-empty-types-are-βˆƒ-compact (inl c) =
 prβ‚‚ (βˆƒ-compactβˆ™-types-are-inhabited-and-compact c)
βˆƒ-compactβˆ™-or-empty-types-are-βˆƒ-compact (inr u) =
 empty-types-are-βˆƒ-compact u

βˆƒ-compact-types-are-βˆƒ-compactβˆ™-or-empty : {X : 𝓀 Μ‡ }
                                        β†’ is-βˆƒ-compact X
                                        β†’ is-βˆƒ-compactβˆ™ X + is-empty X
βˆƒ-compact-types-are-βˆƒ-compactβˆ™-or-empty {𝓀} {X} c = g
 where
  h : is-decidable (βˆƒ x κž‰ X , β‚€ ＝ β‚€) β†’ is-βˆƒ-compactβˆ™ X + is-empty X
  h (inl t) = inl (inhabited-and-compact-types-are-βˆƒ-compactβˆ™
                    (βˆ₯βˆ₯-functor pr₁ t , c))
  h (inr u) = inr (contrapositive (Ξ» x β†’ ∣ x , refl ∣) u)

  g : is-βˆƒ-compactβˆ™ X + is-empty X
  g = h (c (Ξ» _ β†’ β‚€))

\end{code}

8 Feb 2018: A type X is Ξ -compact iff every map X β†’ 𝟚 has an infimum:

\begin{code}

_has-inf_ : {X : 𝓀 Μ‡ } β†’ (X β†’ 𝟚) β†’ 𝟚 β†’ 𝓀 Μ‡
p has-inf n = (βˆ€ x β†’ n ≀ p x) Γ— (βˆ€ (m : 𝟚) β†’ (βˆ€ x β†’ m ≀ p x) β†’ m ≀ n)

having-inf-is-prop : {X : 𝓀 Μ‡ } (p : X β†’ 𝟚) (n : 𝟚) β†’ is-prop (p has-inf n)
having-inf-is-prop {𝓀} {X} p n (f , g) (f' , g') = to-Γ—-＝ r s
 where
  r : f ＝ f'
  r = dfunext fe' (Ξ» x β†’ ≀₂-is-prop-valued (f x) (f' x))
  s : g ＝ g'
  s = dfunext fe' (Ξ» m β†’ dfunext fe' (Ξ» Ο• β†’ ≀₂-is-prop-valued (g m Ο•) (g' m Ο•)))

at-most-one-inf : {X : 𝓀 Μ‡ } (p : X β†’ 𝟚) β†’ is-prop (Ξ£ n κž‰ 𝟚 , p has-inf n)
at-most-one-inf p (n , f , g) (n' , f' , g') = to-Ξ£-＝ (≀₂-anti (g' n f) (g n' f') , having-inf-is-prop p n' _ _)

has-infs : 𝓀 Μ‡ β†’ 𝓀 Μ‡
has-infs X = βˆ€ (p : X β†’ 𝟚) β†’ Ξ£ n κž‰ 𝟚 , p has-inf n

having-infs-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (has-infs X)
having-infs-is-prop {𝓀} {X} = Ξ -is-prop fe' at-most-one-inf

Ξ -compact-has-infs : {X : 𝓀 Μ‡ } β†’ is-Ξ -compact X β†’ has-infs X
Ξ -compact-has-infs c p = g (c p)
 where
  g : is-decidable (βˆ€ x β†’ p x ＝ ₁) β†’ Ξ£ n κž‰ 𝟚 , p has-inf n
  g (inl Ξ±) = ₁ , (Ξ» x β†’ transport⁻¹ (₁ ≀₂_) (Ξ± x) (≀₂-refl {β‚€})) , Ξ» m Ο• β†’ ₁-top
  g (inr u) = β‚€ , (Ξ» _ β†’ β‚€-bottom {β‚€}) , h
   where
    h : (m : 𝟚) β†’ (βˆ€ x β†’ m ≀ p x) β†’ m ≀ β‚€
    h m Ο† = ≀₂-criterion f
     where
      f : m ＝ ₁ β†’ β‚€ ＝ ₁
      f r = 𝟘-elim (u α)
       where
        Ξ± : βˆ€ x β†’ p x ＝ ₁
        Ξ± x = ₁-maximal (transport (_≀ p x) r (Ο† x))

has-infs-Ξ -compact : {X : 𝓀 Μ‡ } β†’ has-infs X β†’ is-Ξ -compact X
has-infs-Ξ -compact h p = f (h p)
 where
  f : (Ξ£ n κž‰ 𝟚 , p has-inf n) β†’ is-decidable (βˆ€ x β†’ p x ＝ ₁)
  f (β‚€ , _ , l) = inr u
   where
    u : Β¬ βˆ€ x β†’ p x ＝ ₁
    u Ξ± = l ₁ (Ξ» x β†’ ≀₂-criterion (Ξ» _ β†’ Ξ± x))
  f (₁ , g , _) = inl Ξ±
   where
    Ξ± : βˆ€ x β†’ p x ＝ ₁
    Ξ± x = ₁-maximal (g x)

\end{code}

TODO. Show equivalence with existence of suprema. Is there a similar
characterization of βˆƒ-compactness?

Implicit application of type-theoretical choice:

\begin{code}

inf : {X : 𝓀 Μ‡ } β†’ is-Ξ -compact X β†’ (X β†’ 𝟚) β†’ 𝟚
inf c p = pr₁ (Ξ -compact-has-infs c p)

inf-property : {X : 𝓀 Μ‡ } β†’ (c : is-Ξ -compact X) (p : X β†’ 𝟚) β†’ p has-inf (inf c p)
inf-property c p = prβ‚‚ (Ξ -compact-has-infs c p)

inf₁ : {X : 𝓀 Μ‡ } (c : is-Ξ -compact X) {p : X β†’ 𝟚}
     β†’ inf c p ＝ ₁ β†’ βˆ€ x β†’ p x ＝ ₁
inf₁ c {p} r x = ≀₂-criterion-converse (pr₁ (inf-property c p) x) r

inf₁-converse : {X : 𝓀 Μ‡ } (c : is-Ξ -compact X) {p : X β†’ 𝟚}
              β†’ (βˆ€ x β†’ p x ＝ ₁) β†’ inf c p ＝ ₁
inf₁-converse c {p} Ξ± = ₁-maximal (h g)
 where
  h : (βˆ€ x β†’ ₁ ≀ p x) β†’ ₁ ≀ inf c p
  h = prβ‚‚ (inf-property c p) ₁

  g : βˆ€ x β†’ ₁ ≀ p x
  g x = ₁-maximal-converse (Ξ± x)

\end{code}

21 Feb 2018.

It is well known that infima and suprema are characterized as
adjoints. TODO. Link the above development with the following (easy).

In synthetic topology with the dominance 𝟚, a type is called 𝟚-compact
if the map Κ : 𝟚 β†’ (X β†’ 𝟚) has a right adjoint A : (X β†’ 𝟚) β†’ 𝟚, with
respect to the natural ordering of 𝟚 and the pointwise order of the
function type (X β†’ 𝟚), and 𝟚-overt if it has a left-adjoint
E : (X β†’ 𝟚) β†’ 𝟚.

Κ is the usual combinator (written Kappa rather than Kay here):

\begin{code}

Κ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ Y β†’ (X β†’ Y)
Κ y x = y

\end{code}

The pointwise order on boolean predicates:

\begin{code}

_≀̇_ : {X : 𝓀 Μ‡ } β†’ (X β†’ 𝟚) β†’ (X β†’ 𝟚) β†’ 𝓀 Μ‡
p ≀̇ q = βˆ€ x β†’ p x ≀ q x

\end{code}

We define adjunctions in the two special cases where one of the sides
is Κ with Y=𝟚, for simplicity, rather than in full generality:

\begin{code}

Κ⊣ : {X : 𝓀 Μ‡ } β†’ ((X β†’ 𝟚) β†’ 𝟚) β†’ 𝓀 Μ‡
Κ⊣ A = (n : 𝟚) (p : _ β†’ 𝟚) β†’ Κ n ≀̇ p ↔ n ≀ A p

_⊣Κ : {X : 𝓀 Μ‡ } β†’ ((X β†’ 𝟚) β†’ 𝟚) β†’ 𝓀 Μ‡
E ⊣Κ = (n : 𝟚) (p : _ β†’ 𝟚) β†’ E p ≀ n ↔ p ≀̇ Κ n

\end{code}

TODO: The types Κ⊣ A and E ⊣Κ are propositions, and so are the types
Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚) , Κ⊣ A (compactness) and
Ξ£ E κž‰ (X β†’ 𝟚) β†’ 𝟚) , E ⊣Κ (overtness).

Right adjoints to Κ are characterized as follows:

\begin{code}

Κ⊣-charac : {X : 𝓀 Μ‡ } β†’ (A : (X β†’ 𝟚) β†’ 𝟚)
          β†’ Κ⊣ A ↔ ((p : X β†’ 𝟚) β†’ A p ＝ ₁ ↔ p ＝ (Ξ» x β†’ ₁))
Κ⊣-charac {𝓀} {X} A = f , g
 where
  f : Κ⊣ A β†’ (p : X β†’ 𝟚) β†’ A p ＝ ₁ ↔ p ＝ (Ξ» x β†’ ₁)
  f Ο† p = fβ‚€ , f₁
   where
    fβ‚€ : A p ＝ ₁ β†’ p ＝ (Ξ» x β†’ ₁)
    fβ‚€ r = dfunext fe' l₃
     where
      lβ‚€ : ₁ ≀ A p β†’ Κ ₁ ≀̇ p
      lβ‚€ = prβ‚‚ (Ο† ₁ p)
      l₁ : Κ ₁ ≀̇ p
      l₁ = lβ‚€ (₁-maximal-converse r)
      lβ‚‚ : (x : X) β†’ ₁ ≀ p x
      lβ‚‚ = l₁
      l₃ : (x : X) β†’ p x ＝ ₁
      l₃ x = ≀₂-criterion-converse (lβ‚‚ x) refl
    f₁ : p ＝ (Ξ» x β†’ ₁) β†’ A p ＝ ₁
    f₁ s = ≀₂-criterion-converse lβ‚€ refl
     where
      l₃ : (x : X) β†’ p x ＝ ₁
      l₃ = happly s
      lβ‚‚ : (x : X) β†’ ₁ ≀ p x
      lβ‚‚ x = ₁-maximal-converse (l₃ x)
      l₁ : Κ ₁ ≀̇ p
      l₁ = lβ‚‚
      lβ‚€ : ₁ ≀ A p
      lβ‚€ = pr₁ (Ο† ₁ p) l₁
  g : ((p : X β†’ 𝟚) β†’ A p ＝ ₁ ↔ p ＝ (Ξ» x β†’ ₁)) β†’ Κ⊣ A
  g Ξ³ n p = (gβ‚€ n refl , g₁ n refl)
   where
    gβ‚€ : βˆ€ m β†’ m ＝ n β†’ Κ m ≀̇ p β†’ m ≀ A p
    gβ‚€ β‚€ r l = β‚€-bottom {β‚€}
    gβ‚€ ₁ refl l = ₁-maximal-converse (prβ‚‚ (Ξ³ p) l₁)
     where
      lβ‚€ : (x : X) β†’ p x ＝ ₁
      lβ‚€ x = ₁-maximal (l x)
      l₁ : p ＝ (Ξ» x β†’ ₁)
      l₁ = dfunext fe' lβ‚€

    g₁ : βˆ€ m β†’ m ＝ n β†’ m ≀ A p β†’ Κ m ≀̇ p
    g₁ β‚€ r l x = β‚€-bottom {β‚€}
    g₁ ₁ refl l x = ₁-maximal-converse (lβ‚€ x)
     where
      l₁ : p ＝ (Ξ» x β†’ ₁)
      l₁ = pr₁ (Ξ³ p) (₁-maximal l)
      lβ‚€ : (x : X) β†’ p x ＝ ₁
      lβ‚€ = happly l₁

\end{code}

Using this as a lemma, we see that a type is Ξ -compact in the sense we
defined iff it is compact in the usual sense of synthetic topology for
the dominance 𝟚.

\begin{code}

Ξ -compact-iff-Κ-has-right-adjoint : {X : 𝓀 Μ‡ }
                                  β†’ is-Ξ -compact X ↔ (Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚), Κ⊣ A)
Ξ -compact-iff-Κ-has-right-adjoint {𝓀} {X} = (f , g)
 where
  f : is-Ξ -compact X β†’ Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚), Κ⊣ A
  f c = (A , prβ‚‚ (Κ⊣-charac A) l₁)
   where
    c' : (p : X β†’ 𝟚) β†’ is-decidable (p ＝ (Ξ» x β†’ ₁))
    c' = Ξ -compact-types-are-Ξ -compact' c

    lβ‚€ : (p : X β†’ 𝟚)
       β†’ is-decidable (p ＝ (Ξ» x β†’ ₁)) β†’ Ξ£ n κž‰ 𝟚 , (n ＝ ₁ ↔ p ＝ (Ξ» x β†’ ₁))
    lβ‚€ p (inl r) = (₁ , ((Ξ» _ β†’ r) , Ξ» _ β†’ refl))
    lβ‚€ p (inr u) = (β‚€ , ((Ξ» s β†’ 𝟘-elim (zero-is-not-one s)) , Ξ» r β†’ 𝟘-elim (u r)))

    A : (X β†’ 𝟚) β†’ 𝟚
    A p = pr₁ (lβ‚€ p (c' p))

    l₁ : (p : X β†’ 𝟚) β†’ A p ＝ ₁ ↔ p ＝ (Ξ» x β†’ ₁)
    l₁ p = prβ‚‚ (lβ‚€ p (c' p))

  g : ((Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚), Κ⊣ A)) β†’ is-Ξ -compact X
  g (A , Ο†) = Ξ -compact'-types-are-Ξ -compact c'
   where
    l₁ : (p : X β†’ 𝟚) β†’ A p ＝ ₁ ↔ p ＝ (Ξ» x β†’ ₁)
    l₁ = pr₁ (Κ⊣-charac A) Ο†

    lβ‚€ : (p : X β†’ 𝟚) β†’ is-decidable (A p ＝ ₁) β†’ is-decidable (p ＝ (Ξ» x β†’ ₁))
    lβ‚€ p (inl r) = inl (pr₁ (l₁ p) r)
    lβ‚€ p (inr u) = inr (contrapositive (prβ‚‚ (l₁ p)) u)

    c' : (p : X β†’ 𝟚) β†’ is-decidable (p ＝ (Ξ» x β†’ ₁))
    c' p = lβ‚€ p (𝟚-is-discrete (A p) ₁)

\end{code}

Next we show that ΞΊ has a right adjoint iff it has a left adjoint,
namely its De Morgan dual, which exists because 𝟚 is a boolean algebra
and hence so is the type (X β†’ 𝟚) with the pointwise operations.

\begin{code}

𝟚-DeMorgan-dual : {X : 𝓀 Μ‡ } β†’ ((X β†’ 𝟚) β†’ 𝟚) β†’ ((X β†’ 𝟚) β†’ 𝟚)
𝟚-DeMorgan-dual Ο† p = complement (Ο† (Ξ» x β†’ complement (p x)))

𝟚-DeMorgan-dual-involutive : {X : 𝓀 Μ‡ } β†’ (Ο† : (X β†’ 𝟚) β†’ 𝟚)
                           β†’ 𝟚-DeMorgan-dual (𝟚-DeMorgan-dual Ο†) ＝ Ο†
𝟚-DeMorgan-dual-involutive {𝓀} Ο† = dfunext fe' h
 where
  f : βˆ€ p β†’ complement (complement (Ο† (Ξ» x β†’ complement (complement (p x)))))
          ＝ Ο† (Ξ» x β†’ complement (complement (p x)))
  f p = complement-involutive (Ο† (Ξ» x β†’ complement (complement (p x))))

  g : βˆ€ p β†’ Ο† (Ξ» x β†’ complement (complement (p x))) ＝ Ο† p
  g p = ap Ο† (dfunext fe' (Ξ» x β†’ complement-involutive (p x)))

  h : βˆ€ p β†’ 𝟚-DeMorgan-dual (𝟚-DeMorgan-dual Ο†) p ＝ Ο† p
  h p = f p βˆ™ g p

Ξ -compact-is-𝟚-overt : {X : 𝓀 Μ‡ } β†’ (A : (X β†’ 𝟚) β†’ 𝟚)
                     β†’ Κ⊣ A β†’ (𝟚-DeMorgan-dual A) ⊣Κ
Ξ -compact-is-𝟚-overt {𝓀} {X} A = f
 where
  E : (X β†’ 𝟚) β†’ 𝟚
  E = 𝟚-DeMorgan-dual A
  f : Κ⊣ A β†’ E ⊣Κ
  f Ο† = Ξ³
   where
     Ξ³ : (n : 𝟚) (p : X β†’ 𝟚) β†’ (E p ≀ n) ↔ (p ≀̇ Κ n)
     Ξ³ n p = (Ξ³β‚€ , γ₁ )
      where
       Ξ³β‚€ : E p ≀ n β†’ p ≀̇ Κ n
       Ξ³β‚€ l = m₃
        where
         mβ‚€ : complement n ≀ A (Ξ» x β†’ complement (p x))
         mβ‚€ = complement-left l
         m₁ : Κ (complement n) ≀̇ (Ξ» x β†’ complement (p x))
         m₁ = prβ‚‚ (Ο† (complement n) (Ξ» x β†’ complement (p x))) mβ‚€
         mβ‚‚ : (x : X) β†’ complement n ≀ complement (p x)
         mβ‚‚ = m₁
         m₃ : (x : X) β†’ p x ≀ n
         m₃ x = complement-both-left (mβ‚‚ x)

       γ₁ : p ≀̇ Κ n β†’ E p ≀ n
       γ₁ l = complement-left mβ‚€
        where
         m₃ : (x : X) β†’ p x ≀ n
         m₃ = l
         mβ‚‚ : (x : X) β†’ complement n ≀ complement (p x)
         mβ‚‚ x = complement-both-right (m₃ x)
         m₁ : Κ (complement n) ≀̇ (Ξ» x β†’ complement (p x))
         m₁ = mβ‚‚
         mβ‚€ : complement n ≀ A (Ξ» x β†’ complement (p x))
         mβ‚€ = pr₁ (Ο† (complement n) (Ξ» x β†’ complement (p x))) m₁

𝟚-overt-is-Ξ -compact : {X : 𝓀 Μ‡ } β†’ (E : (X β†’ 𝟚) β†’ 𝟚)
                     β†’ E ⊣Κ β†’ Κ⊣ (𝟚-DeMorgan-dual E)
𝟚-overt-is-Ξ -compact {𝓀} {X} E = g
 where
  A : (X β†’ 𝟚) β†’ 𝟚
  A = 𝟚-DeMorgan-dual E
  g : E ⊣Κ β†’ Κ⊣ A
  g Ξ³ = Ο†
   where
     Ο† : (n : 𝟚) (p : X β†’ 𝟚) β†’ Κ n ≀̇ p ↔ n ≀ A p
     Ο† n p = (Ο†β‚€ , φ₁ )
      where
       Ο†β‚€ : Κ n ≀̇ p β†’ n ≀ A p
       Ο†β‚€ l = complement-right mβ‚€
        where
         m₃ : (x : X) β†’ n ≀ p x
         m₃ = l
         mβ‚‚ : (x : X) β†’ complement (p x) ≀ complement n
         mβ‚‚ x = complement-both-right (m₃ x)
         m₁ : (Ξ» x β†’ complement (p x)) ≀̇ Κ (complement n)
         m₁ = mβ‚‚
         mβ‚€ : E (Ξ» x β†’ complement (p x)) ≀ complement n
         mβ‚€ = prβ‚‚ (Ξ³ (complement n) (Ξ» x β†’ complement (p x))) mβ‚‚

       φ₁ : n ≀ A p β†’ Κ n ≀̇ p
       φ₁ l = m₃
        where
         mβ‚€ : E (Ξ» x β†’ complement (p x)) ≀ complement n
         mβ‚€ = complement-right l
         m₁ : (Ξ» x β†’ complement (p x)) ≀̇ Κ (complement n)
         m₁ = pr₁ (Ξ³ (complement n) (Ξ» x β†’ complement (p x))) mβ‚€
         mβ‚‚ : (x : X) β†’ complement (p x) ≀ complement n
         mβ‚‚ = m₁
         m₃ : (x : X) β†’ n ≀ p x
         m₃ x = complement-both-left (mβ‚‚ x)

\end{code}

We have the following corollaries:

\begin{code}

Ξ -compact-iff-𝟚-overt : {X : 𝓀 Μ‡ }
                      β†’ (Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚), Κ⊣ A) ↔ (Ξ£ E κž‰ ((X β†’ 𝟚) β†’ 𝟚), E ⊣Κ)
Ξ -compact-iff-𝟚-overt {𝓀} {X} = (f , g)
 where
  f : (Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚), Κ⊣ A) β†’ (Ξ£ E κž‰ ((X β†’ 𝟚) β†’ 𝟚), E ⊣Κ)
  f (A , Ο†) = (𝟚-DeMorgan-dual A , Ξ -compact-is-𝟚-overt A Ο†)

  g : (Ξ£ E κž‰ ((X β†’ 𝟚) β†’ 𝟚), E ⊣Κ) β†’ (Ξ£ A κž‰ ((X β†’ 𝟚) β†’ 𝟚), Κ⊣ A)
  g (E , γ) = (𝟚-DeMorgan-dual E , 𝟚-overt-is-Π-compact E γ)

\end{code}

In this corollary we record explicitly that a type is Ξ -compact iff it
is 𝟚-overt:

\begin{code}

Ξ -compact-iff-Κ-has-left-adjoint : {X : 𝓀 Μ‡ }
                                 β†’ is-Ξ -compact X ↔ (Ξ£ E κž‰ ((X β†’ 𝟚) β†’ 𝟚), E ⊣Κ)
Ξ -compact-iff-Κ-has-left-adjoint {𝓀} {X} = (f , g)
 where
  f : is-Ξ -compact X β†’ (Ξ£ E κž‰ ((X β†’ 𝟚) β†’ 𝟚), E ⊣Κ)
  f c = pr₁ Ξ -compact-iff-𝟚-overt (pr₁ Ξ -compact-iff-Κ-has-right-adjoint c)

  g : (Ξ£ E κž‰ ((X β†’ 𝟚) β†’ 𝟚), E ⊣Κ) β†’ is-Ξ -compact X
  g o = prβ‚‚ Ξ -compact-iff-Κ-has-right-adjoint (prβ‚‚ Ξ -compact-iff-𝟚-overt o)

\end{code}

TODO. We get as a corollary that

      E ⊣Κ ↔ ((p : X β†’ 𝟚) β†’ E p ＝ β‚€ ↔ p ＝ (Ξ» x β†’ β‚€)).

TODO. Find the appropriate place in this file to remark that decidable
propositions are closed under Ξ -compact/overt meets and joins. And
then clopen sets (or 𝟚-open sets, or complemented subsets) are closed
under Ξ -compact/over unions and intersections.

20 Feb 2018. In classical topology, a space X is compact iff the
projection A Γ— X β†’ A is a closed map for every space A, meaning that
the image of every closed set is closed. In our case, because of the
use of decidable truth-values in the definition of Ξ -compactness, the
appropriate notion is that of clopen map, that is, a map that sends
clopen sets to clopen sets. As in our setup, clopen sets correspond to
decidable subsets, or sets with 𝟚-valued characteristic functions. In
our case, the clopeness of the projections characterize the notion of
βˆƒ-compactness, which is stronger than compactness.

There is a certain asymmetry in the following definition, in that the
input decidable predicate (or clopen subtype) is given as a 𝟚-valued
function, whereas instead of saying that the image predicate factors
through the embedding 𝟚 of into the type of truth values, we say that
it has decidable truth-values, which is equivalent. Such an asymmetry
is already present in our formulation of the notion of compactness.

We have defined image with lower case in the module UF. We now need
Images with upper case:

\begin{code}

Image : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
     β†’ (X β†’ Y) β†’ (X β†’ 𝓦 Μ‡ ) β†’ (Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡ )
Image f A = Ξ» y β†’ βˆƒ x κž‰ domain f , A x Γ— (f x ＝ y)

is-clopen-map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-clopen-map {𝓀} {π“₯} {X} {Y} f = (p : X β†’ 𝟚) (y : Y)
                                β†’ is-decidable (Image f (Ξ» x β†’ p x ＝ β‚€) y)

being-clopen-map-is-prop : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                           β†’ (f : X β†’ Y) β†’ is-prop (is-clopen-map f)
being-clopen-map-is-prop {𝓀} {π“₯} f =
 Ξ β‚‚-is-prop fe' (Ξ» p y β†’ decidability-of-prop-is-prop fe' βˆ₯βˆ₯-is-prop)

fst : (A : 𝓀 Μ‡ ) (X : π“₯ Μ‡ ) β†’ A Γ— X β†’ A
fst _ _ = pr₁

βˆƒ-compact-clopen-projections : (X : 𝓀 Μ‡ )
                             β†’ is-βˆƒ-compact X
                             β†’ (βˆ€ {π“₯} (A : π“₯ Μ‡ ) β†’ is-clopen-map (fst A X))
βˆƒ-compact-clopen-projections X c A p a = g (c (Ξ» x β†’ p (a , x)))
 where
  g : is-decidable (βˆƒ x κž‰ X , p (a , x) ＝ β‚€)
    β†’ is-decidable (βˆƒ z κž‰ A Γ— X , (p z ＝ β‚€) Γ— (pr₁ z ＝ a))
  g (inl e) = inl ((βˆ₯βˆ₯-functor h) e)
   where
    h : (Ξ£ x κž‰ X , p (a , x) ＝ β‚€) β†’ Ξ£ z κž‰ A Γ— X , (p z ＝ β‚€) Γ— (pr₁ z ＝ a)
    h (x , r) =  (a , x) , (r , refl)
  g (inr u) = inr (contrapositive (βˆ₯βˆ₯-functor h) u)
   where
    h : (Ξ£ z κž‰ A Γ— X , (p z ＝ β‚€) Γ— (pr₁ z ＝ a)) β†’ Ξ£ x κž‰ X , p (a , x) ＝ β‚€
    h ((a' , x) , (r , s)) = x , transport (Ξ» - β†’ p (- , x) ＝ β‚€) s r

clopen-projections-βˆƒ-compact : βˆ€ {𝓀 𝓦} (X : 𝓀 Μ‡ )
                             β†’ (βˆ€ {π“₯} (A : π“₯ Μ‡ ) β†’ is-clopen-map (fst A X))
                             β†’ is-βˆƒ-compact X
clopen-projections-βˆƒ-compact {𝓀} {𝓦} X ΞΊ p = g (ΞΊ πŸ™ (Ξ» z β†’ p (prβ‚‚ z)) ⋆)
 where
  g : is-decidable (βˆƒ z κž‰ πŸ™ {𝓦} Γ— X , (p (prβ‚‚ z) ＝ β‚€) Γ— (pr₁ z ＝ ⋆))
    β†’ is-decidable (βˆƒ x κž‰ X , p x ＝ β‚€)
  g (inl e) = inl (βˆ₯βˆ₯-functor h e)
   where
    h : (Ξ£ z κž‰ πŸ™ Γ— X , (p (prβ‚‚ z) ＝ β‚€) Γ— (pr₁ z ＝ ⋆)) β†’ Ξ£ x κž‰ X , p x ＝ β‚€
    h ((⋆ , x) , r , _) = x , r
  g (inr u) = inr (contrapositive (βˆ₯βˆ₯-functor h) u)
   where
    h : (Ξ£ x κž‰ X , p x ＝ β‚€) β†’ Ξ£ z κž‰ πŸ™ Γ— X , (p (prβ‚‚ z) ＝ β‚€) Γ— (pr₁ z ＝ ⋆)
    h (x , r) = (⋆ , x) , (r , refl)

\end{code}

TODO.

⋆ Consider 𝟚-perfect maps.

⋆ βˆƒ-compactness: attainability of minima. Existence of potential
  maxima.

⋆ Relation of Ξ -compactness with finiteness and discreteness.

⋆ Non-classical cotaboos Every Ξ -compact subtype of β„• is finite. Every
  Ξ -compact subtype of a discrete type is finite. What are the
  cotaboos necessary (and sufficient) to prove that the type of
  decidable subsingletons of β„•βˆžβ†’β„• is Ξ -compact?  Continuity principles
  are enough.

⋆ 𝟚-subspace: e:Xβ†’Y such that every clopen Xβ†’πŸš extends to some clopen
  Yβ†’πŸš (formulated with Ξ£ and βˆƒ). Or to a largest such clopen, or a
  smallest such clopen (right and left adjoints to the restriction map
  (Yβ†’πŸš)β†’(Xβ†’πŸš) that maps v to v ∘ e and could be written e ⁻¹[ v ].  A
  𝟚-subspace-embedding of totally separated types should be a
  (homotopy) embedding, but not conversely (find a counter-example).

⋆ 𝟚-injective types (injectives wrt to 𝟚-subspace-embeddigs). They
  should be the retracts of powers of 𝟚. Try to characterize them
  "intrinsically".

⋆ Relation of 𝟚-subspaces with Ξ -compact subtypes.

⋆ 𝟚-Hofmann-Mislove theorem: clopen filters of clopens should
  correspond to Π-compact (𝟚-saturated) 𝟚-subspaces. Are cotaboos
  needed for this?

⋆ Which results here depend on the particular dominance 𝟚, and which
  ones generalize to any dominance, or to any "suitable" dominance? In
  particular, it is of interest to generalize this to "Sierpinki like"
  dominances. And what is "Sierpinski like" in precise (internal)
  terms? This should be formulated in terms of cotaboos.