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

--------------------------------------------------------------------------------
-- Gluing.  Section "Gluing", subsection
-- "Explicit pointwise formulas: homotopy and strict fibres".
--
--   * pointwise Glue via homotopy fibres, `Glue-pt`;
--   * strict-fibre variant: `Glue-strict`, with strict boundary compatibility;
--   * with strict-equivalence
--     boundary data (strict inverse + strict retract/section laws), `unglue` is
--     a strict equivalence and the boundary projections are strict equivalences
--     with strict compatibility.  This needs neither univalence nor cofibrancy.
--------------------------------------------------------------------------------

module Extension.Glue where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓφ ℓA ℓT : Level

-- Strict fibre of a boundary map at a point.
fibᵉ : {A : UUᵉ ℓA} {T : UUᵉ ℓT} (e : T → A) (a : A) → UUᵉ (ℓA ⊔ ℓT)
fibᵉ {T = T} e a = Σᵉ T (λ t → e t =ᵉ a)

module _ (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (T : φ → UUᵉ ℓT) (e : (p : φ) → T p → A) where

  -- Strict-fibre Glue.
  Glue-strict : UUᵉ (ℓφ ⊔ ℓA ⊔ ℓT)
  Glue-strict = Σᵉ A (λ a → (p : φ) → fibᵉ (e p) a)

  -- unglue is the first projection (`unglue(a,h) ≔ a`).
  unglue : Glue-strict → A
  unglue = pr1ᵉ

  -- Boundary projection  ρ_p(a,h) ≔ π₁(h p).
  ρ : (p : φ) → Glue-strict → T p
  ρ p g = pr1ᵉ (pr2ᵉ g p)

  -- Strict boundary compatibility  e_p ∘ ρ_p =ˢ unglue  (2nd comp of h p).
  ρ-boundary : (p : φ) (g : Glue-strict) → e p (ρ p g) =ᵉ unglue g
  ρ-boundary p g = pr2ᵉ (pr2ᵉ g p)

--------------------------------------------------------------------------------
-- fibrant (inner) and e p : T p → A; the homotopy fibre uses the inner Id.
--------------------------------------------------------------------------------

Glue-pt : (φ : UUᵉ ℓφ) (A : UU ℓA) (T : φ → UU ℓT) (e : (p : φ) → T p → A)
        → UUᵉ (ℓφ ⊔ ℓA ⊔ ℓT)
Glue-pt φ A T e = Σᵉ (C A) (λ a → (p : φ) → C (Σ (T p) (λ t → Id (e p t) (ic a))))

--------------------------------------------------------------------------------
-- Strict Glue from strict-equivalence boundary data.
--------------------------------------------------------------------------------

module _ (φ : UUᵉ ℓφ) (A : UUᵉ ℓA) (T : φ → UUᵉ ℓT)
         (e : (p : φ) → T p → A) (r : (p : φ) → A → T p)
         (sec : (p : φ) (a : A) → e p (r p a) =ᵉ a)
         (ret : (p : φ) (t : T p) → r p (e p t) =ᵉ t)
       where

  private
    G = Glue-strict φ A T e

    -- Each strict fibre is strictly contractible, centre (r p a , sec p a).
    fib-contr : (p : φ) (a : A) (w : fibᵉ (e p) a) → (r p a ,ᵉ sec p a) =ᵉ w
    fib-contr p a (t ,ᵉ q) =
      dep-pair-=ᵉ _ _ (exo-concat (exo-ap (r p) (exo-inv q)) (ret p t) ,ᵉ UIPᵉ _ _)

    glue-inv : A → G
    glue-inv a = a ,ᵉ (λ p → r p a ,ᵉ sec p a)

  -- (1) unglue is a strict equivalence; hence G is fibrant when A is.
  unglue-strict-equiv : G ≅ A
  unglue-strict-equiv = unglue φ A T e ,ᵉ (glue-inv ,ᵉ (retr ,ᵉ sect))
    where
    retr : (g : G) → glue-inv (unglue φ A T e g) =ᵉ g
    retr (a ,ᵉ h) = dep-pair-=ᵉ _ _ (reflᵉ ,ᵉ funextᵉ (λ p → fib-contr p a (h p)))
    sect : (a : A) → unglue φ A T e (glue-inv a) =ᵉ a
    sect a = reflᵉ

  -- e_p is itself a strict equivalence (from the strict inverse data).
  e-iso : (p : φ) → T p ≅ A
  e-iso p = e p ,ᵉ (r p ,ᵉ (ret p ,ᵉ sec p))

  -- (2)+(3) The boundary is a strict equivalence  G ≅ T p,  obtained as the
  -- composite  G ≅ A ≅ T p;  and  ρ-boundary  gives  e_p ∘ ρ_p =ˢ unglue,  so
  -- the boundary projection ρ_p is (strictly equal to) this strict equivalence.
  Glue-boundary-≅ : (p : φ) → G ≅ T p
  Glue-boundary-≅ p = ≅-trans unglue-strict-equiv (≅-sym (e-iso p))