{-# OPTIONS --erased-cubical --safe #-}
import Equality.Path as P
module Pointed-type.Connected
{e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where
open P.Derived-definitions-and-properties eq
open import Prelude
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import Group equality-with-J as G using (_≃ᴳ_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
import Nat equality-with-J as Nat
open import Pointed-type equality-with-J
open import Pointed-type.Homotopy-group eq
private
variable
p : Level
P : Pointed-type p
Connected : Pointed-type p → Type p
Connected (A , x) = (y : A) → ∥ x ≡ y ∥
Connected-component : Pointed-type p → Pointed-type p
Connected-component (A , x) =
(∃ λ y → ∥ x ≡ y ∥) , (x , ∣ refl _ ∣)
Connected-component↣ᴮ : Connected-component P ↝[ embedding ]ᴮ P
Connected-component↣ᴮ =
record { to = proj₁
; is-embedding = λ x y →
_≃_.is-equivalence $
Eq.with-other-function
(x ≡ y ↔⟨ inverse $ ignore-propositional-component T.truncation-is-proposition ⟩□
proj₁ x ≡ proj₁ y □)
(cong proj₁)
proj₁-Σ-≡,≡←≡
}
, refl _
Connected-Connected-component :
{P : Pointed-type p} →
Connected (Connected-component P)
Connected-Connected-component y =
flip T.∥∥-map (proj₂ y) λ eq →
Σ-≡,≡→≡ eq (T.truncation-is-proposition _ _)
H-level-Connected-component :
∀ {P : Pointed-type p} n →
H-level (1 + n) (proj₁ P) →
H-level (1 + n) (proj₁ (Connected-component P))
H-level-Connected-component {P = A , x} n =
H-level (1 + n) A ↝⟨ (λ h →
Σ-closure (1 + n) h λ _ →
mono (Nat.suc≤suc (Nat.zero≤ n))
T.truncation-is-proposition) ⟩
H-level (1 + n) (∃ λ y → ∥ x ≡ y ∥) □
H-level-Ω-Connected-component :
∀ {P : Pointed-type p} n →
H-level n (proj₁ (Ω P)) →
H-level n (proj₁ (Ω (Connected-component P)))
H-level-Ω-Connected-component {P = _ , x} n =
H-level n (x ≡ x) ↝⟨ H-level-cong _ _ (ignore-propositional-component T.truncation-is-proposition) ⟩□
H-level n ((x , _) ≡ (x , _)) □
Fundamental-group′-Connected-component≃ᴳ :
{s₁ : Is-set (proj₁ (Ω (Connected-component P)))}
{s₂ : Is-set (proj₁ (Ω P))} →
Fundamental-group′ (Connected-component P) s₁ ≃ᴳ
Fundamental-group′ P s₂
Fundamental-group′-Connected-component≃ᴳ {P = _ , x} = λ where
.G.Homomorphic.related →
Eq.with-other-function
((x , _) ≡ (x , _) ↔⟨ inverse $ ignore-propositional-component T.truncation-is-proposition ⟩□
x ≡ x □)
(cong proj₁)
proj₁-Σ-≡,≡←≡
.G.Homomorphic.homomorphic p q →
cong proj₁ (trans p q) ≡⟨ cong-trans _ _ _ ⟩∎
trans (cong proj₁ p) (cong proj₁ q) ∎