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 $P$ over pointed, connected types $A$ and $B\text{.}$ While the actual statement and the proof are highly technical, it specialises to a fairly straightforward construction: to give a map $e:A\to B\to C\text{,}$ 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 $A$ is $n\text{-connected}$ and $B$ is $m\text{-connected}$ ($n,m\ge 2\text{),}$ then each $P(-,-)$ must be $(n+m)\text{-truncated.}$

    (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) (suc n + suc m))

Provided that everything fits together, we can actually give the data of interest: A function $f:(a:A)\to P(a,\ast )\text{,}$ a function $g:(b:B)\to P(\ast ,b)\text{,}$ and a coherence path $f(\ast )=g(\ast )\text{.}$

    (f : ∀ a → P a b₀) (g : ∀ b → P a₀ b) (coh : f a₀ ≡ g b₀)
  where

  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 → 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 $e\text{:}$ A proof ${\beta }_1:e(a,\ast )=f(a)\text{;}$ a proof that ${\beta }_2:e(\ast ,b)=g(b)\text{;}$ and a proof that, at $e(\ast ,\ast )\text{,}$ these differ by the specified coherence $f(\ast )=g(\ast )\text{.}$

  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 _