Ian Ray, 23rd July 2024

Modifications made by Ian Ray on 26th September 2024

We define connected types and maps. We then explore relationships, closure
properties and characterizations of interest pertaining to the concept of
connectedness.

\begin{code}

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

open import UF.FunExt

module UF.ConnectedTypes
        (fe : Fun-Ext)
       where
                          
open import MLTT.Spartan hiding (_+_)
open import Notation.Order
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PropTrunc 
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Truncations fe
open import UF.TruncationLevels
open import UF.TruncatedTypes fe
open import UF.Univalence

\end{code}

We now define the notion of connectedness for types and functions with respect
to truncation levels.

\begin{code}

module _ (te : general-truncations-exist) where

 private 
  pt : propositional-truncations-exist
  pt = general-truncations-give-propositional-truncations te

 open general-truncations-exist te
 open propositional-truncations-exist pt
 open import UF.ImageAndSurjection pt

 _is_connected : ๐“ค ฬ‡ โ†’ โ„•โ‚‹โ‚‚ โ†’ ๐“ค ฬ‡
 X is k connected = is-contr (โˆฅ X โˆฅ[ k ])

 _is_connected-map : {X : ๐“ค ฬ‡} {Y : ๐“ฅ ฬ‡} โ†’ (f : X โ†’ Y) โ†’ โ„•โ‚‹โ‚‚ โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
 f is k connected-map = each-fiber-of f (ฮป - โ†’ - is k connected)

\end{code}

TODO: show that connectedness as defined elsewhere in the library is
a special case of k-connectedness. Connectedness typically means set
connectedness, by our convention it will mean 0-connectedness.

We characterize โˆ’1-connected types as inhabited types and โˆ’1-connected maps as
surjections.

\begin{code}

 inhabited-if-โˆ’1-connected : {X : ๐“ค ฬ‡}
                           โ†’ X is โˆ’1 connected โ†’ โˆฅ X โˆฅ
 inhabited-if-โˆ’1-connected X-1-conn = โˆ’1-trunc-to-prop-trunc pt (center X-1-conn)

 โˆ’1-connected-if-inhabited : {X : ๐“ค ฬ‡}
                           โ†’ โˆฅ X โˆฅ โ†’ X is โˆ’1 connected
 โˆ’1-connected-if-inhabited x-anon =
  pointed-props-are-singletons (prop-trunc-to-โˆ’1-trunc pt x-anon) โˆ’1-trunc-is-prop

 โˆ’1-connected-iff-inhabited : {X : ๐“ค ฬ‡}
                            โ†’ X is โˆ’1 connected โ†” โˆฅ X โˆฅ
 โˆ’1-connected-iff-inhabited =
  (inhabited-if-โˆ’1-connected , โˆ’1-connected-if-inhabited)

 map-is-surj-if-โˆ’1-connected : {X : ๐“ค ฬ‡} {Y : ๐“ฅ ฬ‡} {f : X โ†’ Y}
                             โ†’ f is โˆ’1 connected-map โ†’ is-surjection f
 map-is-surj-if-โˆ’1-connected m y = inhabited-if-โˆ’1-connected (m y)

 map-is-โˆ’1-connected-if-surj : {X : ๐“ค ฬ‡} {Y : ๐“ฅ ฬ‡} {f : X โ†’ Y}
                             โ†’ is-surjection f โ†’ f is โˆ’1 connected-map
 map-is-โˆ’1-connected-if-surj f-is-surj y = โˆ’1-connected-if-inhabited (f-is-surj y)

 map-is-โˆ’1-connected-iff-surj : {X : ๐“ค ฬ‡} {Y : ๐“ฅ ฬ‡} {f : X โ†’ Y}
                              โ†’ f is โˆ’1 connected-map โ†” is-surjection f
 map-is-โˆ’1-connected-iff-surj =
  (map-is-surj-if-โˆ’1-connected , map-is-โˆ’1-connected-if-surj)

\end{code}

We develop some closure conditions pertaining to connectedness. Connectedness
is closed under equivalence as expected, but more importantly connectedness
extends below: more precisely if a type is k connected then it is l connected
for all l โ‰ค k. We provide a few incarnations of this fact below which may prove
useful. 

\begin{code}

 connectedness-closed-under-equiv : {X : ๐“ค ฬ‡} {Y : ๐“ฅ ฬ‡} {k : โ„•โ‚‹โ‚‚}
                                  โ†’ X โ‰ƒ Y
                                  โ†’ Y is k connected
                                  โ†’ X is k connected
 connectedness-closed-under-equiv e Y-con =
  equiv-to-singleton (truncation-closed-under-equiv e) Y-con

 contractible-types-are-connected : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                                  โ†’ is-contr X
                                  โ†’ X is k connected
 contractible-types-are-connected {๐“ค} {X} {k} (c , C) = ((โˆฃ c โˆฃ[ k ]) , C')
  where
   C' : (s : โˆฅ X โˆฅ[ k ]) โ†’ (โˆฃ c โˆฃ[ k ]) ๏ผ s
   C' = โˆฅโˆฅโ‚™-ind (truncation-levels-closed-under-Id โˆฅโˆฅโ‚™-is-truncated (โˆฃ c โˆฃ[ k ]))
                (ฮป x โ†’ ap โˆฃ_โˆฃ[ k ] (C x))

 connectedness-is-lower-closed : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                               โ†’ X is (k + 1) connected
                               โ†’ X is k connected
 connectedness-is-lower-closed {๐“ค} {X} {k} X-succ-con =
  equiv-to-singleton successive-truncations-equiv 
                     (contractible-types-are-connected X-succ-con)

 connectedness-is-lower-closed-+ : {X : ๐“ค ฬ‡} {l : โ„•โ‚‹โ‚‚} {k : โ„•}
                                 โ†’ X is (l + k) connected
                                 โ†’ X is l connected
 connectedness-is-lower-closed-+ {๐“ค} {X} {l} {0} X-con = X-con
 connectedness-is-lower-closed-+ {๐“ค} {X} {l} {succ k} X-con =
  connectedness-is-lower-closed-+ (connectedness-is-lower-closed X-con)

 connectedness-is-lower-closed' : {X : ๐“ค ฬ‡} {k l : โ„•โ‚‹โ‚‚}
                                โ†’ (l โ‰ค k)
                                โ†’ X is k connected
                                โ†’ X is l connected
 connectedness-is-lower-closed' {๐“ค} {X} {k} {l} o X-con =
  connectedness-is-lower-closed-+ (transport (ฮป z โ†’ X is z connected) p X-con)
  where
   m : โ„•
   m = subtraction-โ„•โ‚‹โ‚‚-term l k o
   p = k       ๏ผโŸจ subtraction-โ„•โ‚‹โ‚‚-identification l k o โปยน โŸฉ
       l + m   โˆŽ

\end{code}

We characterize connected types in terms of inhabitedness and connectedness of
the identity type at one level below. We will assume univalence only when necessary.

\begin{code}

 inhabited-if-connected : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                        โ†’ X is (k + 1) connected โ†’ โˆฅ X โˆฅ
 inhabited-if-connected {_} {_} {k} X-conn =
  inhabited-if-โˆ’1-connected (connectedness-is-lower-closed' โ‹† X-conn)

 _is-locally_connected : (X : ๐“ค ฬ‡) (k : โ„•โ‚‹โ‚‚) โ†’ ๐“ค  ฬ‡
 X is-locally k connected = (x y : X) โ†’ (x ๏ผ y) is k connected

 connected-types-are-locally-connected : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                                       โ†’ is-univalent ๐“ค
                                       โ†’ X is (k + 1) connected
                                       โ†’ X is-locally k connected
 connected-types-are-locally-connected {_} {_} {k} ua X-conn x y =
  equiv-to-singleton (eliminated-trunc-identity-char ua)
   (is-prop-implies-is-prop' (singletons-are-props X-conn)
    โˆฃ x โˆฃ[ succ k ] โˆฃ y โˆฃ[ succ k ])

 connected-types-are-inhabited-and-locally-connected : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                                                     โ†’ is-univalent ๐“ค
                                                     โ†’ X is (k + 1) connected
                                                     โ†’ โˆฅ X โˆฅ
                                                     ร— X is-locally k connected
 connected-types-are-inhabited-and-locally-connected ua X-conn =
  (inhabited-if-connected X-conn , connected-types-are-locally-connected ua X-conn)

 inhabited-and-locally-connected-types-are-connected : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                                                     โ†’ is-univalent ๐“ค
                                                     โ†’ โˆฅ X โˆฅ
                                                     โ†’ X is-locally k connected
                                                     โ†’ X is (k + 1) connected
 inhabited-and-locally-connected-types-are-connected
  {_} {_} {โˆ’2} ua anon-x id-conn =
  pointed-props-are-singletons (prop-trunc-to-โˆ’1-trunc pt anon-x) โˆ’1-trunc-is-prop
 inhabited-and-locally-connected-types-are-connected
  {_} {_} {succ k} ua anon-x id-conn =
  โˆฅโˆฅ-rec (being-singleton-is-prop fe)
         (ฮป x โ†’ (โˆฃ x โˆฃ[ (k + 1) + 1 ]
          , โˆฅโˆฅโ‚™-ind (ฮป v โ†’ truncation-levels-are-upper-closed
           (ฮป p q โ†’ โˆฅโˆฅโ‚™-is-truncated โˆฃ x โˆฃ[ (k + 1) + 1 ] v p q)) 
            (ฮป y โ†’ forth-trunc-id-char ua (center (id-conn x y)))))
         anon-x

 connected-characterization : {X : ๐“ค ฬ‡} {k : โ„•โ‚‹โ‚‚}
                            โ†’ is-univalent ๐“ค
                            โ†’ X is (k + 1) connected
                            โ†” โˆฅ X โˆฅ ร— X is-locally k connected
 connected-characterization ua =
  (connected-types-are-inhabited-and-locally-connected ua
   , uncurry (inhabited-and-locally-connected-types-are-connected ua))

 ap-is-less-connected : {X : ๐“ค ฬ‡} {Y : ๐“ฅ ฬ‡} {k : โ„•โ‚‹โ‚‚} 
                      โ†’ (ua : is-univalent (๐“ค โŠ” ๐“ฅ))
                      โ†’ (f : X โ†’ Y)
                      โ†’ f is (k + 1) connected-map
                      โ†’ {x x' : X}
                      โ†’ (ap f {x} {x'}) is k connected-map
 ap-is-less-connected ua f f-conn {x} {x'} p =
  equiv-to-singleton (truncation-closed-under-equiv (fiber-of-ap-โ‰ƒ f p))
   (connected-types-are-locally-connected ua (f-conn (f x'))
    (x , p) (x' , refl))

\end{code}