Ian Ray, 23rd July 2024

Modifications made by Ian Ray on 26th September 2024.

Modifications made by Ian Ray on 17th December 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.Base
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PropTrunc
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.TruncatedTypes fe
open import UF.Truncations fe
open import UF.TruncationLevels
open import UF.Univalence
open import UF.Yoneda

\end{code}

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

\begin{code}

private
 fe' : FunExt
 fe' ๐“ค ๐“ฅ = fe {๐“ค} {๐“ฅ}

module connectedness-results (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)

 being-connected-is-prop : {k : โ„•โ‚‹โ‚‚} {X : ๐“ค ฬ‡ }
                         โ†’ is-prop (X is k connected)
 being-connected-is-prop = being-truncated-is-prop

 being-connected-map-is-prop : {k : โ„•โ‚‹โ‚‚} {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y}
                             โ†’ is-prop (f is k connected-map)
 being-connected-map-is-prop = ฮ -is-prop fe (ฮป y โ†’ being-connected-is-prop)

 connected-if-contr : {X : ๐“ค ฬ‡ } {k : โ„•โ‚‹โ‚‚}
                    โ†’ is-contr X
                    โ†’ X is k connected
 connected-if-contr {_} {X} {โˆ’2} X-is-contr = โˆ’2-trunc-is-contr
 connected-if-contr {_} {X} {succ k} (c , C) = (โˆฃ c โˆฃ[ k + 1 ] , C')
  where
   C'' : (x : X) โ†’ โˆฃ c โˆฃ[ k + 1 ] ๏ผ โˆฃ x โˆฃ[ k + 1 ]
   C'' x = canonical-identity-trunc-map โˆฃ C x โˆฃ[ k ]
   C' : is-central โˆฅ X โˆฅ[ k + 1 ] โˆฃ c โˆฃ[ k + 1 ]
   C' = โˆฅโˆฅโ‚™-ind (ฮป v โ†’ ฮป p q โ†’ truncation-levels-closed-under-Id
                 (โˆฅโˆฅโ‚™-is-truncated โˆฃ c โˆฃ[ succ k ] v) p q) C''

\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}

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

 inhabited-types-are-โˆ’1-connected : {X : ๐“ค ฬ‡ }
                                  โ†’ โˆฅ X โˆฅ โ†’ X is โˆ’1 connected
 inhabited-types-are-โˆ’1-connected 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 =
  (โˆ’1-connected-types-are-inhabited , inhabited-types-are-โˆ’1-connected)

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

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

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

\end{code}

We develop some closure conditions pertaining to connectedness. Connectedness
is closed under retracts and 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}

 retract-is-connected : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {k : โ„•โ‚‹โ‚‚}
                      โ†’ retract Y of X
                      โ†’ X is k connected
                      โ†’ Y is k connected
 retract-is-connected R X-conn =
  retract-of-singleton (truncation-closed-under-retract R) X-conn

 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   โˆŽ

 map-connectedness-is-lower-closed : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {f : X โ†’ Y} {k l : โ„•โ‚‹โ‚‚}
                                   โ†’ (l โ‰ค k)
                                   โ†’ f is k connected-map
                                   โ†’ f is l connected-map
 map-connectedness-is-lower-closed o f-k-con y =
  connectedness-is-lower-closed' o (f-k-con y)

\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}

 connected-types-are-inhabited : {X : ๐“ค ฬ‡ } {k : โ„•โ‚‹โ‚‚}
                               โ†’ X is (k + 1) connected โ†’ โˆฅ X โˆฅ
 connected-types-are-inhabited {_} {_} {k} X-conn =
  โˆ’1-connected-types-are-inhabited (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 =
  (connected-types-are-inhabited 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}

We prove a characterization of connectedness from the HoTT book
(see Corollary 7.5.9.). Notice we choose to directly prove this result
rather than instantiate it as a special case of a more general result
(Lemma 7.5.7.) which is stated below.

NOTE: We will NOT state the corollary as an iff statement due to a large
quantification issue.

\begin{code}

 private
  consts : (X : ๐“ค ฬ‡ ) (Y : ๐“ฅ ฬ‡ )
         โ†’ Y โ†’ (X โ†’ Y)
  consts X Y y x = y

 maps-with-connected-dom-truncated-cod-are-constant : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {n : โ„•โ‚‹โ‚‚}
                                                    โ†’ X is n connected
                                                    โ†’ Y is n truncated
                                                    โ†’ Y โ‰ƒ (X โ†’ Y)
 maps-with-connected-dom-truncated-cod-are-constant {๐“ค} {_} {X} {Y} {n}
  X-conn Y-trunc = e
  where
   e : Y โ‰ƒ (X โ†’ Y)
   e = Y                โ‰ƒโŸจ ๐Ÿ™โ†’ fe โŸฉ
       (๐Ÿ™ {๐“ค} โ†’ Y)      โ‰ƒโŸจ โ†’cong'' fe fe I โŸฉ
       (โˆฅ X โˆฅ[ n ] โ†’ Y) โ‰ƒโŸจ โˆฅโˆฅโ‚™-universal-property Y-trunc โŸฉ
       (X โ†’ Y)          โ– 
    where
     I : ๐Ÿ™ {๐“ค} โ‰ƒ โˆฅ X โˆฅ[ n ]
     I = singleton-โ‰ƒ-๐Ÿ™' X-conn
   observation : consts X Y ๏ผ โŒœ e โŒ
   observation = refl

 constants-map-from-truncated-type-is-equiv : {X : ๐“ค ฬ‡ } {n : โ„•โ‚‹โ‚‚}
                                            โ†’ (Y : ๐“ฅ ฬ‡ )
                                            โ†’ X is n connected
                                            โ†’ Y is n truncated
                                            โ†’ is-equiv (consts X Y)
 constants-map-from-truncated-type-is-equiv Y X-conn Y-trunc =
  โŒœโŒ-is-equiv (maps-with-connected-dom-truncated-cod-are-constant X-conn Y-trunc)

 connected-when-consts-is-equiv : {X : ๐“ค ฬ‡ } {n : โ„•โ‚‹โ‚‚}
                              โ†’ ({๐“ฅ : Universe} (Y : ๐“ฅ ฬ‡ )
                               โ†’ Y is n truncated
                               โ†’ is-equiv (consts X Y))
                              โ†’ X is n connected
 connected-when-consts-is-equiv {_} {X} {n} is-equiv-from-trunc = (c , G)
  where
   s : (X โ†’ โˆฅ X โˆฅ[ n ]) โ†’ โˆฅ X โˆฅ[ n ]
   s = section-map (consts X โˆฅ X โˆฅ[ n ])
        (equivs-have-sections (consts X โˆฅ X โˆฅ[ n ])
        (is-equiv-from-trunc โˆฅ X โˆฅ[ n ] โˆฅโˆฅโ‚™-is-truncated))
   H : (consts X โˆฅ X โˆฅ[ n ]) โˆ˜ s โˆผ id
   H = section-equation (consts X โˆฅ X โˆฅ[ n ])
        (equivs-have-sections (consts X โˆฅ X โˆฅ[ n ])
         (is-equiv-from-trunc โˆฅ X โˆฅ[ n ] โˆฅโˆฅโ‚™-is-truncated))
   c : โˆฅ X โˆฅ[ n ]
   c = s โˆฃ_โˆฃ[ n ]
   H' : (consts X โˆฅ X โˆฅ[ n ]) c ๏ผ โˆฃ_โˆฃ[ n ]
   H' = H โˆฃ_โˆฃ[ n ]
   G : (v : โˆฅ X โˆฅ[ n ]) โ†’ c ๏ผ v
   G = โˆฅโˆฅโ‚™-ind (ฮป - โ†’ truncation-levels-are-upper-closed โˆฅโˆฅโ‚™-is-truncated c -)
               (ฮป x โ†’ happly H' x)

\end{code}

We will now prove a general result from the HoTT book that characterizes when
a map is connected (see Lemma 7.5.7.)

\begin{code}

 dependent-equiv-from-truncated-fam-connected-map
  : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {n : โ„•โ‚‹โ‚‚}
  โ†’ (f : X โ†’ Y)
  โ†’ (P : Y โ†’ ๐“ฆ ฬ‡ )
  โ†’ ((y : Y) โ†’ (P y) is n truncated)
  โ†’ f is n connected-map
  โ†’ ((y : Y) โ†’ P y) โ‰ƒ ((x : X) โ†’ P (f x))
 dependent-equiv-from-truncated-fam-connected-map
  {_} {_} {_} {X} {Y} {n} f P
  P-trunc f-conn = e
  where
   e : ((y : Y) โ†’ P y) โ‰ƒ ((x : X) โ†’ P (f x))
   e = ((y : Y) โ†’ P y)                                         โ‰ƒโŸจ I โŸฉ
       ((y : Y) โ†’ (fiber f y โ†’ P y))                           โ‰ƒโŸจ II โŸฉ
       ((y : Y) โ†’ (x : X) โ†’ (p : f x ๏ผ y) โ†’ P y)              โ‰ƒโŸจ ฮ -flip' โŸฉ
       ((x : X) โ†’ (y : Y) โ†’ (p : f x ๏ผ y) โ†’ P y)              โ‰ƒโŸจ III โŸฉ
       ((x : X) โ†’ P (f x))                                     โ– 
    where
     I = ฮ -cong fe fe (ฮป - โ†’ maps-with-connected-dom-truncated-cod-are-constant
                       (f-conn -) (P-trunc -))
     II = ฮ -cong fe fe (ฮป - โ†’ curry-uncurry' fe fe)
     III = ฮ -cong fe fe (ฮป - โ†’ โ‰ƒ-sym (Yoneda-equivalence fe' (f -) P))
   observation : โŒœ e โŒ ๏ผ dprecomp P f
   observation = refl

 dep-precomp-from-truncated-family-is-equiv
  : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {n : โ„•โ‚‹โ‚‚}
  โ†’ (f : X โ†’ Y)
  โ†’ (P : Y โ†’ ๐“ฆ ฬ‡ )
  โ†’ ((y : Y) โ†’ (P y) is n truncated)
  โ†’ f is n connected-map
  โ†’ is-equiv (dprecomp P f)
 dep-precomp-from-truncated-family-is-equiv f P P-trunc f-conn =
  โŒœโŒ-is-equiv (dependent-equiv-from-truncated-fam-connected-map f P P-trunc f-conn)

 dep-precomp-has-section-if-is-equiv
  : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ }
  โ†’ (f : X โ†’ Y)
  โ†’ (P : Y โ†’ ๐“ฆ ฬ‡ )
  โ†’ is-equiv (dprecomp P f)
  โ†’ has-section (dprecomp P f)
 dep-precomp-has-section-if-is-equiv f P = equivs-have-sections (dprecomp P f)

 map-is-connected-if-dep-precomp-from-truncated-family-has-section
  : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {n : โ„•โ‚‹โ‚‚}
  โ†’ (f : X โ†’ Y)
  โ†’ ({๐“ฆ : Universe} (P : Y โ†’ ๐“ฆ ฬ‡ ) โ†’ ((y : Y) โ†’ (P y) is n truncated)
                                 โ†’ has-section (dprecomp P f))
  โ†’ f is n connected-map
 map-is-connected-if-dep-precomp-from-truncated-family-has-section
  {๐“ค} {๐“ฅ} {X} {Y} {n} f sec-from-trunc y = (c y , C)
  where
   Q : Y โ†’ ๐“ค โŠ” ๐“ฅ ฬ‡
   Q y = โˆฅ fiber f y โˆฅ[ n ]
   c' : ((x : X) โ†’ โˆฅ fiber f (f x) โˆฅ[ n ])
      โ†’ ((y : Y) โ†’ โˆฅ fiber f y โˆฅ[ n ])
   c' = section-map (dprecomp Q f) (sec-from-trunc Q (ฮป - โ†’ โˆฅโˆฅโ‚™-is-truncated))
   c : (y : Y) โ†’ โˆฅ fiber f y โˆฅ[ n ]
   c = c' (ฮป - โ†’ โˆฃ (- , refl) โˆฃ[ n ])
   H' : (dprecomp Q f) โˆ˜ c' โˆผ id
   H' = section-equation (dprecomp Q f)
                         (sec-from-trunc Q (ฮป - โ†’ โˆฅโˆฅโ‚™-is-truncated))
   H : (x : X) โ†’ c (f x) ๏ผ โˆฃ (x , refl) โˆฃ[ n ]
   H = happly' ((dprecomp Q f โˆ˜ c') (ฮป - โ†’ โˆฃ (- , refl) โˆฃ[ n ]))
               (ฮป - โ†’ โˆฃ (- , refl) โˆฃ[ n ]) (H' (ฮป - โ†’ โˆฃ (- , refl) โˆฃ[ n ]))
   C : (w : โˆฅ fiber f y โˆฅ[ n ]) โ†’ c y ๏ผ w
   C = โˆฅโˆฅโ‚™-ind (ฮป - โ†’ truncation-levels-are-upper-closed โˆฅโˆฅโ‚™-is-truncated
                (c y) -)
               C'
    where
     C' : ((x , p) : fiber f y) โ†’ c y ๏ผ โˆฃ (x , p) โˆฃ[ n ]
     C' (x , refl) = H x

\end{code}

We show that the n-truncation map is n-connected.

\begin{code}

 trunc-map-is-connected : {X : ๐“ค ฬ‡ } {n : โ„•โ‚‹โ‚‚}
                        โ†’ โˆฃ_โˆฃ[ n ] is n connected-map
 trunc-map-is-connected {_} {X} {n} =
  map-is-connected-if-dep-precomp-from-truncated-family-has-section
   โˆฃ_โˆฃ[ n ] has-sec
  where
   has-sec : {๐“ฆ : Universe}
           โ†’ (P : โˆฅ X โˆฅ[ n ] โ†’ ๐“ฆ ฬ‡ )
           โ†’ ((v : โˆฅ X โˆฅ[ n ]) โ†’ P v is n truncated)
           โ†’ has-section (dprecomp P โˆฃ_โˆฃ[ n ])
   has-sec {_} P P-trunc = (โˆฅโˆฅโ‚™-ind P-trunc , comp-rule)
    where
     comp-rule : dprecomp P โˆฃ_โˆฃ[ n ] โˆ˜ โˆฅโˆฅโ‚™-ind P-trunc โˆผ id
     comp-rule h = (dprecomp P โˆฃ_โˆฃ[ n ]) (โˆฅโˆฅโ‚™-ind P-trunc h) ๏ผโŸจ refl โŸฉ
                   (โˆฅโˆฅโ‚™-ind P-trunc h) โˆ˜ โˆฃ_โˆฃ[ n ]            ๏ผโŸจ I โŸฉ
                   h                                         โˆŽ
      where
       I = dfunext fe (โˆฅโˆฅโ‚™-ind-comp P-trunc h)

\end{code}

We provide a useful result about maps from the constant type to a connected
type (see Lemma 7.5.11 of the HoTT book for the full statement). Observe we
do assume univalence locally here (the HoTT book assumes it implicitly).

\begin{code}

 basepoint-map-is-less-connected : {X : ๐“ค ฬ‡ } {n : โ„•โ‚‹โ‚‚}
                                 โ†’ is-univalent ๐“ค
                                 โ†’ (xโ‚€ : ๐Ÿ™ {๐“ค} โ†’ X)
                                 โ†’ X is (n + 1) connected
                                 โ†’ xโ‚€ is n connected-map
 basepoint-map-is-less-connected {_} {X} {n} ua xโ‚€ X-con x =
  connectedness-closed-under-equiv ๐Ÿ™-lneutral
   (connected-types-are-locally-connected ua X-con (xโ‚€ โ‹†) x)

\end{code}