open import 1Lab.Prelude

open import Data.Nat.Properties

open import Homotopy.Connectedness

module Homotopy.Wedge where


# Wedge connectivityπ

The wedge connectivity lemma gives a set of sufficient conditions for constructing a section

of a type family over pointed, connected types and While the actual statement and the proof are highly technical, it specialises to a fairly straightforward construction: to give a map it suffices to specify how it varies in each coordinate, and to show that these descriptions agree on the basepoints.

module
Wedge
{β β' β''} {Aβ@(A , aβ) : Typeβ β} {Bβ@(B , bβ) : Typeβ β'} {P : A β B β Type β''}


In addition to generalising to dependent functions, the actual statement of the lemma includes the conditions of connectedness on the two argument types, and truncation on the codomain. If is and is ( then each must be

    (n m : Nat)
(a-conn : is-n-connected A (2 + n))
(b-conn : is-n-connected B (2 + m))
(p-hl : β x y β is-hlevel (P x y) (2 + n + m))


Provided that everything fits together, we can actually give the data of interest: A function a function and a coherence path

    (f : β a β P a bβ) (g : β b β P aβ b) (coh : f aβ β‘ g bβ)
where

As mentioned above, the construction is highly technical. Itβs a direct transcription of the proof in .
  private
Q : A β Type (β' β β'')
Q a = Ξ£ ((b : B) β P a b) (Ξ» k β k bβ β‘ f a)

remβ' : (x : A) β is-hlevel (fibre (_β (Ξ» _ β bβ)) (Ξ» _ β f x)) (1 + n)
remβ' a = relative-n-type-const-plus {A = β€} (P a) (Ξ» _ β bβ) (suc m) (suc n)
(point-is-n-connected bβ m b-conn)
(Ξ» b β subst (is-hlevel (P a b)) (sym (ap suc (+-sucr n m))) (p-hl a b))
(Ξ» _ β f a)

opaque
worker : Ξ£ ((b : A) β Q b) (Ξ» h β Path (β€ β Q aβ) (Ξ» _ β h aβ) (Ξ» _ β g , sym coh))
worker = connected-elimination-principle (suc n) Q hl (g , sym coh) a-conn where
hl : (x : A) β is-hlevel (Q x) (suc n)
hl x = retractβis-hlevel (suc n)
(Ξ» (p , q) β p , happly q tt)
(Ξ» (p , q) β p , funext Ξ» _ β q)
(Ξ» _ β refl) (remβ' x)


If everything fits together, then we end up with the following data, in addition to the section A proof a proof that and a proof that, at these differ by the specified coherence

  opaque
elim : β x y β P x y
elim x y = worker .fst x .fst y

Ξ²β : β a β elim a bβ β‘ f a
Ξ²β a = worker .fst a .snd

Ξ²β : β b β elim aβ b β‘ g b
Ξ²β b = ap fst (worker .snd $β tt)$β b

Ξ²-path : Ξ²β bβ β sym coh β‘ Ξ²β aβ
Ξ²-path = squareβcommutes (ap snd (worker .snd \$β tt)) β β-idr _