{-# OPTIONS --without-K --exact-split --two-level #-}

--------------------------------------------------------------------------------
-- Lemma 5.13(3).
--
-- Let I have 0,1 : I with i∂ : ∂I ↪ I (∂I = ⊤ + ⊤).  A *homotopy coherent* Glue
-- structure for (i∂, 𝓤) yields a *weak* Glue structure for (I, 0, 1, 𝓤).
--
-- Given A,B : 𝓤 and f : A ≃ B, apply the homotopy coherent structure to the
-- constant family Ā = λ_.B, the copairing T = [A,B] : ∂I → 𝓤, and e = [f, id_B].
-- It returns (G, β, u) with strict boundary β and homotopy coherence
--   u(i∂φ) = e_φ coerced along β  (as equivalences).
-- Set b₀ = ι β_inl : G 0 = A, b₁ = ι β_inr : G 1 = B (`ι-fun`), and u' the
-- underlying maps of u.  The weak homotopies then read off from the coherence
-- and the unfolding `coerce-e-und` (which is the paper's idtoeqv(ι β) ~ c_β):
--   u'₀ ~ pr1(coerce-e)_inl ~ f ∘ idtoeqv(b₀),   u'₁ ~ … ~ idtoeqv(b₁).
--------------------------------------------------------------------------------

module Extension.GlueStrengthChain3 where

open import Extension.Prelude
open import Extension.GlueStructure using (has-homotopy-coherent-glue ; coerce-e-und ; ι-fun)
open import Extension.GlueRules using (WeakGlue)

private
  variable
    ℓI : Level

module _ (I : UUᵉ ℓI) (i∂ : (⊤ᵉ {ℓI} +ᵉ ⊤ᵉ {ℓI}) → I) (𝓤 : Level)
         (hcg : has-homotopy-coherent-glue i∂ 𝓤)
       where

  private
    0I 1I : I
    0I = i∂ (inlᵉ starᵉ)
    1I = i∂ (inrᵉ starᵉ)

  strength-chain-3 : WeakGlue I 0I 1I 𝓤
  strength-chain-3 A B f = G ,ᵉ (b₀ ,ᵉ (b₁ ,ᵉ (u' ,ᵉ (H₀ ,ᵉ H₁))))
    where
    Ā : I → UU 𝓤
    Ā _ = B
    T : (⊤ᵉ {ℓI} +ᵉ ⊤ᵉ {ℓI}) → UU 𝓤
    T (inlᵉ _) = A
    T (inrᵉ _) = B
    e : (φ : ⊤ᵉ {ℓI} +ᵉ ⊤ᵉ {ℓI}) → C (T φ ≃ Ā (i∂ φ))
    e (inlᵉ _) = f
    e (inrᵉ _) = c (≃-refl B)

    gd  = hcg Ā T e
    out = pr1ᵉ gd
    coh = pr2ᵉ gd
    G  = pr1ᵉ out
    β  = pr1ᵉ (pr2ᵉ out)
    u  = pr2ᵉ (pr2ᵉ out)

    b₀ : C (Id (G 0I) A)
    b₀ = c (ι-fun (λ φ → G (i∂ φ)) T β (inlᵉ starᵉ))
    b₁ : C (Id (G 1I) B)
    b₁ = c (ι-fun (λ φ → G (i∂ φ)) T β (inrᵉ starᵉ))

    u' : (t : I) → C (G t → B)
    u' t = c (pr1 (ic (u t)))

    H₀ : C (ic (u' 0I) ~ (λ x → pr1 (ic f) (pr1 (idtoeqv (ic b₀)) x)))
    H₀ = c (λ x → ap (λ E → pr1 E x) (ic (coh (inlᵉ starᵉ)))
                · coerce-e-und i∂ 𝓤 Ā G T e β (inlᵉ starᵉ) x)

    H₁ : C (ic (u' 1I) ~ pr1 (idtoeqv (ic b₁)))
    H₁ = c (λ x → ap (λ E → pr1 E x) (ic (coh (inrᵉ starᵉ)))
                · coerce-e-und i∂ 𝓤 Ā G T e β (inrᵉ starᵉ) x)