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}