```{-# OPTIONS --without-K --rewriting --overlapping-instances #-}

open import lib.Basics
open import lib.NType2
open import lib.Equivalence2
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths
open import lib.types.TLevel
open import lib.types.Truncation

module lib.NConnected where

is-connected : ∀ {i} → ℕ₋₂ → Type i → Type i
is-connected n A = is-contr (Trunc n A)

has-conn-fibers : ∀ {i j} {A : Type i} {B : Type j} → ℕ₋₂ → (A → B) → Type (lmax i j)
has-conn-fibers {A = A} {B = B} n f =
Π B (λ b → is-connected n (hfiber f b))

{- all types are -2-connected -}
-2-conn : ∀ {i} (A : Type i) → is-connected -2 A
-2-conn A = Trunc-level

{- all inhabited types are -1-connected -}
inhab-conn : ∀ {i} {A : Type i} (a : A) → is-connected -1 A
inhab-conn a = has-level-in ([ a ] , prop-has-all-paths [ a ])

{- connectedness is a prop -}
is-connected-is-prop : ∀ {i} {n : ℕ₋₂} {A : Type i}
→ is-prop (is-connected n A)
is-connected-is-prop = is-contr-is-prop

{- "induction principle" for n-connected maps (where codomain is n-type) -}
abstract
pre∘-conn-is-equiv : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂}
→ {h : A → B} → has-conn-fibers n h
→ (∀ {k} (P : B → n -Type k) → is-equiv (λ (s : Π B (fst ∘ P)) → s ∘ h))
pre∘-conn-is-equiv {A = A} {B = B} {n = n} {h = h} c P = is-eq f g f-g g-f
where f : Π B (fst ∘ P) → Π A (fst ∘ P ∘ h)
f k a = k (h a)

helper : Π A (fst ∘ P ∘ h)
→ (b : B) → Trunc n (Σ A (λ a → h a == b)) → (fst (P b))
helper t b r =
Trunc-rec {{snd (P b)}}
(λ x → transport (λ y → fst (P y)) (snd x) (t (fst x)))
r

g : Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
g t b = helper t b (contr-center (c b))

f-g : ∀ t → f (g t) == t
f-g t = λ= \$ λ a → transport
(λ r →  Trunc-rec {{snd (P (h a))}} _ r == t a)
(! (contr-path(c (h a)) [ (a , idp) ]))
idp

g-f : ∀ k → g (f k) == k
g-f k = λ= \$ λ (b : B) →
Trunc-elim {{λ {r} → =-preserves-level {x = helper (k ∘ h) b r} (snd (P b))}}
(λ x → lemma (fst x) b (snd x)) (contr-center (c b))
where
lemma : ∀ xl → ∀ b → (p : h xl == b) →
helper (k ∘ h) b [ (xl , p) ] == k b
lemma xl ._ idp = idp

conn-extend : ∀ {i j k} {A : Type i} {B : Type j} {n : ℕ₋₂}
→ {h : A → B} → has-conn-fibers n h
→ (P : B → n -Type k)
→ Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
conn-extend c P f = is-equiv.g (pre∘-conn-is-equiv c P) f

conn-out = conn-extend

conn-extend-β : ∀ {i j k} {A : Type i} {B : Type j} {n : ℕ₋₂}
{h : A → B} (c : has-conn-fibers n h)
(P : B → n -Type k) (f : Π A (fst ∘ P ∘ h))
→ ∀ a → (conn-extend c P f (h a)) == f a
conn-extend-β c P f = app= (is-equiv.f-g (pre∘-conn-is-equiv c P) f)

{- generalized "almost induction principle" for maps into ≥n-types
TODO: rearrange this to use ≤T?                                 -}
conn-extend-general : ∀ {i j} {A : Type i} {B : Type j} {n k : ℕ₋₂}
→ {f : A → B} → has-conn-fibers n f
→ ∀ {l} (P : B → (k +2+ n) -Type l)
→ ∀ t → has-level k (Σ (Π B (fst ∘ P)) (λ s → (s ∘ f) == t))
conn-extend-general {k = ⟨-2⟩} c P t =
equiv-is-contr-map (pre∘-conn-is-equiv c P) t
conn-extend-general {B = B} {n = n} {k = S k'} {f = f} c P t = has-level-in
λ {(g , p) (h , q) →
equiv-preserves-level (e g h p q)
{{conn-extend-general {k = k'} c (Q g h) (app= (p ∙ ! q))}} }
where
Q : (g h : Π B (fst ∘ P)) → B → (k' +2+ n) -Type _
Q g h b = ((g b == h b) , has-level-apply (snd (P b)) _ _)

app=-pre∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : B → Type k}
(f : A → B) {g h : Π B C} (p : g == h)
→ app= (ap (λ k → k ∘ f) p) == app= p ∘ f
app=-pre∘ f idp = idp

move-right-on-right-econv : ∀ {i} {A : Type i} {x y z : A}
(p : x == y) (q : x == z) (r : y == z)
→ (p == q ∙ ! r) ≃ (p ∙ r == q)
move-right-on-right-econv {x = x} p idp idp =
(_ , pre∙-is-equiv (∙-unit-r p))

lemma : ∀ g h p q → (H : g ∼ h)
→ ((H ∘ f) == app= (p ∙ ! q))
≃ (ap (λ v → v ∘ f) (λ= H) ∙ q == p)
lemma g h p q H =
move-right-on-right-econv (ap (λ v → v ∘ f) (λ= H)) p q
∘e transport (λ w → (w == app= (p ∙ ! q))
≃ (ap (λ v → v ∘ f) (λ= H) == p ∙ ! q))
(app=-pre∘ f (λ= H) ∙ ap (λ k → k ∘ f) (λ= \$ app=-β H))
(ap-equiv app=-equiv _ _ ⁻¹)

e : ∀ g h p q  →
(Σ (g ∼ h) (λ r → (r ∘ f) == app= (p ∙ ! q)))
≃ ((g , p) == (h , q))
e g h p q =
((=Σ-econv _ _ ∘e Σ-emap-r (λ u → ↓-app=cst-econv ∘e !-equiv))
∘e (Σ-emap-l _ λ=-equiv)) ∘e Σ-emap-r (lemma g h p q)

conn-in : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} {h : A → B}
→ (∀ (P : B → n -Type (lmax i j))
→ Σ (Π A (fst ∘ P ∘ h) → Π B (fst ∘ P))
(λ u → ∀ (t : Π A (fst ∘ P ∘ h)) → u t ∘ h ∼ t))
→ has-conn-fibers n h
conn-in {A = A} {B = B} {h = h} sec b =
let s = sec (λ b → (Trunc _ (hfiber h b) , Trunc-level))
in has-level-in (fst s (λ a → [ a , idp ]) b ,
Trunc-elim (λ k → transport
(λ v → fst s (λ a → [ a , idp ]) (fst v) == [ fst k , snd v ])
(contr-path (pathfrom-is-contr (h (fst k))) (b , snd k))
(snd s (λ a → [ a , idp ]) (fst k))))

abstract
pointed-conn-in : ∀ {i} {n : ℕ₋₂} (A : Type i) (a₀ : A)
→ has-conn-fibers {A = ⊤} n (cst a₀) → is-connected (S n) A
pointed-conn-in {n = n} A a₀ c = has-level-in
([ a₀ ] ,
Trunc-elim
(λ a → Trunc-rec
(λ x → ap [_] (snd x)) (contr-center \$ c a)))

abstract
pointed-conn-out : ∀ {i} {n : ℕ₋₂} (A : Type i) (a₀ : A)
{{_ : is-connected (S n) A}} → has-conn-fibers {A = ⊤} n (cst a₀)
pointed-conn-out {n = n} A a₀ {{c}} a = has-level-in
(point ,
λ y → ! (cancel point)
∙ (ap out \$ contr-has-all-paths (into point) (into y))
∙ cancel y)
where
into-aux : Trunc n (Σ ⊤ (λ _ → a₀ == a)) → Trunc n (a₀ == a)
into-aux = Trunc-fmap snd

into : Trunc n (Σ ⊤ (λ _ → a₀ == a))
→ [_] {n = S n} a₀ == [ a ]
into = <– (=ₜ-equiv [ a₀ ] [ a ]) ∘ into-aux

out-aux : Trunc n (a₀ == a) → Trunc n (Σ ⊤ (λ _ → a₀ == a))
out-aux = Trunc-fmap (λ p → (tt , p))

out : [_] {n = S n} a₀ == [ a ] → Trunc n (Σ ⊤ (λ _ → a₀ == a))
out = out-aux ∘ –> (=ₜ-equiv [ a₀ ] [ a ])

cancel : (x : Trunc n (Σ ⊤ (λ _ → a₀ == a))) → out (into x) == x
cancel x =
out (into x)
=⟨ ap out-aux (<–-inv-r (=ₜ-equiv [ a₀ ] [ a ]) (into-aux x)) ⟩
out-aux (into-aux x)
=⟨ Trunc-fmap-∘ _ _ x ⟩
Trunc-fmap (λ q → (tt , (snd q))) x
=⟨ Trunc-elim {P = λ x → Trunc-fmap (λ q → (tt , snd q)) x == x}
(λ _ → idp) x ⟩
x =∎

point : Trunc n (Σ ⊤ (λ _ → a₀ == a))
point = out \$ contr-has-all-paths [ a₀ ] [ a ]

prop-over-connected :  ∀ {i j} {A : Type i} {a : A} {{p : is-connected 0 A}}
→ (P : A → hProp j)
→ fst (P a) → Π A (fst ∘ P)
prop-over-connected P x = conn-extend (pointed-conn-out _ _) P (λ _ → x)

{- Connectedness of a truncated type -}
Trunc-preserves-conn : ∀ {i} {A : Type i} {n : ℕ₋₂} {m : ℕ₋₂}
→ is-connected n A → is-connected n (Trunc m A)
Trunc-preserves-conn {n = ⟨-2⟩} _ = Trunc-level
Trunc-preserves-conn {A = A} {n = S n} {m} c = lemma (contr-center c) (contr-path c)
where
lemma : (x₀ : Trunc (S n) A) → (∀ x → x₀ == x) → is-connected (S n) (Trunc m A)
lemma = Trunc-elim
(λ a → λ p → has-level-in ([ [ a ] ] ,
Trunc-elim
(Trunc-elim
{{=-preserves-level
(Trunc-preserves-level (S n) Trunc-level)}}
(λ x → <– (=ₜ-equiv [ [ a ] ] [ [ x ] ])
(Trunc-fmap (ap [_])
(–> (=ₜ-equiv [ a ] [ x ]) (p [ x ])))))))

instance
Trunc-preserves-conn-instance : ∀ {i} {A : Type i} {n : ℕ₋₂} {m : ℕ₋₂}
→ {{is-connected n A}} → is-connected n (Trunc m A)
Trunc-preserves-conn-instance {{pA}} = Trunc-preserves-conn pA

{- Connectedness of a Σ-type -}
abstract
Σ-conn : ∀ {i} {j} {A : Type i} {B : A → Type j} {n : ℕ₋₂}
→ is-connected n A → (∀ a → is-connected n (B a))
→ is-connected n (Σ A B)
Σ-conn {A = A} {B = B} {n = ⟨-2⟩} cA cB = -2-conn (Σ A B)
Σ-conn {A = A} {B = B} {n = S m} cA cB =
Trunc-elim
{P = λ ta → (∀ tx → ta == tx) → is-connected (S m) (Σ A B)}
(λ a₀ pA →
Trunc-elim
{P = λ tb → (∀ ty → tb == ty) → is-connected (S m) (Σ A B)}
(λ b₀ pB → has-level-in
([ a₀ , b₀ ] ,
Trunc-elim
{P = λ tp → [ a₀ , b₀ ] == tp}
(λ {(r , s) →
Trunc-rec
(λ pa → Trunc-rec
(λ pb → ap [_] (pair= pa (from-transp! B pa pb)))
(–> (=ₜ-equiv [ b₀ ] [ transport! B pa s ])
(pB [ transport! B pa s ])))
(–> (=ₜ-equiv [ a₀ ] [ r ]) (pA [ r ]))})))
(contr-center (cB a₀)) (contr-path (cB a₀)))
(contr-center cA) (contr-path cA)

×-conn : ∀ {i} {j} {A : Type i} {B : Type j} {n : ℕ₋₂}
→ is-connected n A → is-connected n B
→ is-connected n (A × B)
×-conn cA cB = Σ-conn cA (λ _ → cB)

instance
Σ-conn-instance : ∀ {i} {j} {A : Type i} {B : A → Type j} {n : ℕ₋₂}
→ {{is-connected n A}} → {{{a : A} → is-connected n (B a)}}
→ is-connected n (Σ A B)
Σ-conn-instance {{pA}} {{pB}} = Σ-conn pA (λ _ → pB)

{- connectedness of a path space -}
abstract
path-conn : ∀ {i} {A : Type i} {x y : A} {n : ℕ₋₂}
→ is-connected (S n) A → is-connected n (x == y)
path-conn {x = x} {y = y} cA =
equiv-preserves-level (=ₜ-equiv [ x ] [ y ])
{{has-level-apply (contr-is-prop cA) [ x ] [ y ]}}

instance
path-conn-instance : ∀ {i} {A : Type i} {x y : A} {n : ℕ₋₂}
→ {{is-connected (S n) A}} → is-connected n (x == y)
path-conn-instance {{pA}} = path-conn pA

{- an n-Type which is n-connected is contractible -}
connected-at-level-is-contr : ∀ {i} {A : Type i} {n : ℕ₋₂}
{{pA : has-level n A}} {{cA : is-connected n A}} → is-contr A
connected-at-level-is-contr {{pA}} {{cA}} =
equiv-preserves-level (unTrunc-equiv _) {{cA}}

{- if A is n-connected and m ≤ n, then A is m-connected -}
connected-≤T : ∀ {i} {m n : ℕ₋₂} {A : Type i}
→ m ≤T n → {{_ : is-connected n A}} → is-connected m A
connected-≤T {m = m} {n = n} {A = A} leq =
transport (λ B → is-contr B)
(ua (Trunc-fuse A m n) ∙ ap (λ k → Trunc k A) (minT-out-l leq))
(Trunc-preserves-level m ⟨⟩)

{- Equivalent types have the same connectedness -}
equiv-preserves-conn : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A ≃ B)
{{_ : is-connected n A}} → is-connected n B
equiv-preserves-conn {n = n} e = equiv-preserves-level (Trunc-emap e)

{- Composite of two connected functions is connected -}
∘-conn : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
→ {n : ℕ₋₂} → (f : A → B) → (g : B → C)
→ has-conn-fibers n f
→ has-conn-fibers n g
→ has-conn-fibers n (g ∘ f)
∘-conn {n = n} f g cf cg =
conn-in (λ P → conn-extend cg P ∘ conn-extend cf (P ∘ g) , lemma P)
where
lemma : ∀ P h x → conn-extend cg P (conn-extend cf (P ∘ g) h) (g (f x)) == h x
lemma P h x =
conn-extend cg P (conn-extend cf (P ∘ g) h) (g (f x))
=⟨ conn-extend-β cg P (conn-extend cf (P ∘ g) h) (f x) ⟩
conn-extend cf (P ∘ g) h (f x)
=⟨ conn-extend-β cf (P ∘ g) h x ⟩
h x
=∎
```