Martin Escardo

For the moment we consider 0-connected types only, referred to as
connected types for the sake of brevity.

There is a formulation that doesn't require propositional truncations,
but increases universe levels. We start with that formulation.


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

open import MLTT.Spartan
open import UF.PropTrunc

module UF.Connected (pt : propositional-truncations-exist) where

open PropositionalTruncation pt

open import UF.FunExt
open import UF.Hedberg
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

is-wconnected : 𝓤 ̇  𝓤 ̇
is-wconnected X = (x y : X)   x  y 

is-connected : 𝓤 ̇  𝓤 ̇
is-connected X =  X  × is-wconnected X

being-wconnected-is-prop : funext 𝓤 𝓤  {X : 𝓤 ̇ }  is-prop (is-wconnected X)
being-wconnected-is-prop fe = Π-is-prop fe  x  Π-is-prop fe  y  ∥∥-is-prop))

being-connected-is-prop : funext 𝓤 𝓤  {X : 𝓤 ̇ }  is-prop (is-connected X)
being-connected-is-prop fe = ×-is-prop ∥∥-is-prop (being-wconnected-is-prop fe)

maps-of-wconnected-types-into-sets-are-constant : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                                                 is-set Y
                                                 is-wconnected X
                                                 (f : X  Y)  wconstant f
maps-of-wconnected-types-into-sets-are-constant {𝓤} {𝓥} {X} {Y} s w f x x' = γ
  a :  x  x' 
  a = w x x'
  γ : f x  f x'
  γ = ∥∥-rec s (ap f) a