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

--------------------------------------------------------------------------------
-- Remark 4.4: the Glue rules in homotopy form and strictly coherent Glue
-- structures are interderivable, differing only in their isEquiv components.
--
--   * `strict-coh-to-homotopy-rules`: take underlying maps; unglue = π₁ ∘ u
--     definitionally, and the boundary of item (3) is π₁ of the coherence.
--     No hypotheses.
--   * `homotopy-rules-to-strict-coh`: realign the isEquiv witnesses along the
--     cofibration.  The paper cites Corollary 3.12; we prove the instance
--     directly, since λψ. isEquiv(unglue_ψ) is a fibrant family of inhabited
--     propositions, so the trivial half of the cofibration makes the
--     extension type contractible.  No cofibrancy of Φ or Ψ.  Underlying maps
--     are preserved definitionally: `Realign.preserves-unglue` is reflᵉ.
--
-- Only existence of the realignment is formalized, not its uniqueness.
--------------------------------------------------------------------------------

module Extension.GlueHomotopySemantic where

open import Extension.Prelude
open import Extension.Core using (Ext ; restrict)
open import Extension.CofibFibration using (is-cofib ; Ext-isFibrant)
open import Extension.RelFunext using (satisfies-rel-funext)
open import Extension.GlueRules using (satisfies-homotopy-glue-rules)
open import Extension.GlueStructure
  using (GlueData ; coerce-e ; has-strictly-coherent-glue)

private
  variable
    ℓ ℓ' ℓφ ℓΨ : Level

--------------------------------------------------------------------------------
-- Generic helpers.
--------------------------------------------------------------------------------

-- An inhabited proposition is contractible.
prop-point-contr : {A : UU ℓ} → is-prop A → A → is-contr A
prop-point-contr H a₀ = a₀ , (λ x → pr1 (H x a₀))

-- Transporting backwards and forwards along the same strict equality is the
-- identity.
tr-inv-tr : {A : UUᵉ ℓ} (P : A → UUᵉ ℓ') {x y : A} (E : x =ᵉ y) (z : P y)
          → exo-tr P E (exo-tr P (exo-inv E) z) =ᵉ z
tr-inv-tr P reflᵉ z = reflᵉ

-- Strict equality of coerced inner Σ-pairs, componentwise: a strict equality
-- of the (coerced) first components together with a strict equality of the
-- transported second components gives a strict equality of the pairs.
pairΣC-eq : {X : UU ℓ} {P : X → UU ℓ'} {x₁ x₂ : X} {y₁ : P x₁} {y₂ : P x₂}
            (E : c x₁ =ᵉ c x₂)
          → exo-tr (λ (h : C X) → C (P (ic h))) E (c y₁) =ᵉ c y₂
          → c {A = Σ X P} (x₁ , y₁) =ᵉ c (x₂ , y₂)
pairΣC-eq {x₁ = x₁} reflᵉ W =
  exo-ap (λ (z : C _) → c (x₁ , ic z)) W

-- π₁ commutes with the two family-level transports: the underlying map of
-- e^p (= coerce-e) is the transport, in the family of function spaces, of the
-- underlying maps of e.  By exo-J on the boundary p.
pr1-coerce-e :
    {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
    (A : Ψ → UU 𝓤) (G : Ψ → UU 𝓤) (T : Φ → UU 𝓤)
    (e : (φ : Φ) → C (T φ ≃ A (i φ)))
    (p : (λ φ → G (i φ)) =ᵉ T) (φ : Φ)
  → c (pr1 (ic (coerce-e i 𝓤 A T e G p φ)))
    =ᵉ exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
              (λ ξ → c (pr1 (ic (e ξ)))) φ
pr1-coerce-e i 𝓤 A G .(λ φ → G (i φ)) e reflᵉ φ = reflᵉ

--------------------------------------------------------------------------------
-- Direction 1: strictly coherent gluing ⇒ homotopy form.  No hypotheses.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) where

  strict-coh-to-homotopy-rules :
    has-strictly-coherent-glue i 𝓤 → satisfies-homotopy-glue-rules i 𝓤
  strict-coh-to-homotopy-rules scg A T e =
      G
    ,ᵉ (p
    ,ᵉ ((λ ψ → pr1 (ic (u ψ)))                       -- unglue ≔ π₁ ∘ u
    ,ᵉ ((λ φ → exo-concat
          (exo-ap (λ q → c (pr1 (ic q))) (coh φ))    -- π₁ of the coherence
          (pr1-coerce-e i 𝓤 A G T e p φ))
    ,ᵉ (λ ψ → c (pr2 (ic (u ψ)))))))                 -- invertibility ≔ π₂ ∘ u
    where
    gd  = scg A T e
    G   = pr1ᵉ (pr1ᵉ gd)
    p   = pr1ᵉ (pr2ᵉ (pr1ᵉ gd))
    u   = pr2ᵉ (pr2ᵉ (pr1ᵉ gd))
    coh = pr2ᵉ gd

--------------------------------------------------------------------------------
-- Direction 2: homotopy form ⇒ strictly coherent gluing, by strict realignment
-- of the isEquiv components (the prop-realign instance, via relative funext).
--------------------------------------------------------------------------------

module Realign
    {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {𝓤 : Level}
    (cof : is-cofib i 𝓤) (triv : satisfies-rel-funext cof)
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (e : (φ : Φ) → C (T φ ≃ A (i φ)))
    (G : Ψ → UU 𝓤) (p : (λ φ → G (i φ)) =ᵉ T)
    (ung : (ψ : Ψ) → G ψ → A ψ)
    (ubd : (φ : Φ) → c (ung (i φ)) =ᵉ
             exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
                    (λ ξ → c (pr1 (ic (e ξ)))) φ)
    (inv : (ψ : Ψ) → C (isEquiv (ung ψ)))
  where

  private
    -- e^p, and the strict agreement of underlying maps on the boundary
    Ce : (φ : Φ) → C (G (i φ) ≃ A (i φ))
    Ce φ = coerce-e i 𝓤 A T e G p φ

    E : (φ : Φ) → c (ung (i φ)) =ᵉ c (pr1 (ic (Ce φ)))
    E φ = exo-concat (ubd φ) (exo-inv (pr1-coerce-e i 𝓤 A G T e p φ))

    -- the property family: a fibrant family of inhabited propositions
    P : Ψ → UU 𝓤
    P ψ = isEquiv (ung ψ)

    cP : (ψ : Ψ) → is-contr (P ψ)
    cP ψ = prop-point-contr (is-prop-isEquiv (ung ψ)) (ic (inv ψ))

    -- the boundary datum: the isEquiv witness of e^p, transported to unglue
    -- along the strict boundary agreement E
    FE : (φ : Φ) → C (G (i φ) → A (i φ)) → UUᵉ 𝓤
    FE φ h = C (isEquiv (ic h))

    l : (φ : Φ) → C (P (i φ))
    l φ = exo-tr (FE φ) (exo-inv (E φ)) (c (pr2 (ic (Ce φ))))

    -- relative funext: the extension type of the inhabited-proposition family
    -- has contractible fibrant match; extract an actual strict extension
    contr-match : is-contr (fibrant-match (Ext-isFibrant cof P l))
    contr-match = triv P cP l

    ε : Ext i (λ ψ → C (P ψ)) l
    ε = pr1ᵉ (pr2ᵉ (fibrant-witness (Ext-isFibrant cof P l)))
             (c (pr1 contr-match))

    ε₀ : (ψ : Ψ) → C (P ψ)
    ε₀ = pr1ᵉ ε

    εbd : restrict i ε₀ =ᵉ l
    εbd = pr2ᵉ ε

  -- the realigned equivalence family: unglue with the realigned witnesses
  u : (ψ : Ψ) → C (G ψ ≃ A ψ)
  u ψ = c (ung ψ , ic (ε₀ ψ))

  -- π₁ ∘ u ≐ unglue, definitionally (the realignment changes nothing else)
  preserves-unglue : (ψ : Ψ) → c (pr1 (ic (u ψ))) =ᵉ c (ung ψ)
  preserves-unglue ψ = reflᵉ

  -- strict coherence: u restricts to e^p strictly
  coh : (φ : Φ) → u (i φ) =ᵉ Ce φ
  coh φ =
    pairΣC-eq (E φ)
      (exo-concat
        (exo-ap (exo-tr (FE φ) (E φ)) (happlyᵉ εbd φ))
        (tr-inv-tr (FE φ) (E φ) (c (pr2 (ic (Ce φ))))))

  -- the strictly coherent Glue datum
  realigned-data : GlueData i 𝓤 A T e
  realigned-data = (G ,ᵉ (p ,ᵉ u)) ,ᵉ coh

--------------------------------------------------------------------------------
-- The packaged direction 2, and the two directions side by side.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} {𝓤 : Level}
         (cof : is-cofib i 𝓤) (triv : satisfies-rel-funext cof) where

  homotopy-rules-to-strict-coh :
    satisfies-homotopy-glue-rules i 𝓤 → has-strictly-coherent-glue i 𝓤
  homotopy-rules-to-strict-coh rules A T e =
    Realign.realigned-data cof triv A T e
      (pr1ᵉ tup) (pr1ᵉ (pr2ᵉ tup)) (pr1ᵉ (pr2ᵉ (pr2ᵉ tup)))
      (pr1ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ tup)))) (pr2ᵉ (pr2ᵉ (pr2ᵉ (pr2ᵉ tup))))
    where
    tup = rules A T e

  -- Remark 4.4, both directions at (i,𝓤): homotopy form holds
  -- iff a strictly coherent Glue structure exists.  (Direction 1 needs no
  -- hypotheses; it is exported above at its true generality.)
  homotopy-vs-semantic :
    (satisfies-homotopy-glue-rules i 𝓤 → has-strictly-coherent-glue i 𝓤)
    ×ᵉ (has-strictly-coherent-glue i 𝓤 → satisfies-homotopy-glue-rules i 𝓤)
  homotopy-vs-semantic =
    homotopy-rules-to-strict-coh ,ᵉ strict-coh-to-homotopy-rules i 𝓤