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

--------------------------------------------------------------------------------
-- weak = strict, named forms.
-- Lemma 2.4, Lemma 3.14.
--
-- Over a cofibration into a fibrant family, the total-section space assembles,
-- up to (inner) equivalence, as the Σ over restricted boundaries of the fibrant
-- matches of the extension types:
--
--   ⟨Πψ.A⟩  ≃  Σ (z : ⟨Πφ.A∘i⟩). ⟨Extᵢ(A,z)⟩
--
-- (angle brackets = fibrant match).  This is the homotopy/strict-fibre agreement
-- of the restriction map: the strict extension type over each boundary is the
-- homotopy fibre.  Lemma 3.14 (a weak boundary agreement can be
-- strictified) is the inhabited form, already proved constructively in
-- `Extension.RS410`.
--------------------------------------------------------------------------------

module Extension.WeakStrict where

open import Extension.Prelude
open import Extension.CofibFibration
open import Extension.RS412Ext using (match-equiv)

private
  variable
    ℓ ℓΦ ℓΨ : Level

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ)
         (Y : Ψ → UU ℓ)
       where

  private
    WΨ = Π-fibrant-witness (cofΨ Y)
    WΦ = Π-fibrant-witness (cofΦ (λ φ → Y (i φ)))

  -- The match of the total sections is the Σ, over the match of the restricted
  -- boundaries, of the extension-type matches.  (The right-hand side is
  -- `fibrant-match (isFibrant-Σ WΦ (Ext-isFibrant cof Y))`, i.e.
  --  Σ ⟨Πφ.A∘i⟩ (λ z → ⟨Extᵢ(A, restrict-of z)⟩), by `isFibrant-Σ`.)
  weak=strict : fibrant-match WΨ ≃ fibrant-match (isFibrant-Σ WΦ (Ext-isFibrant cof Y))
  weak=strict = match-equiv WΨ (isFibrant-Σ WΦ (Ext-isFibrant cof Y))
                            (reindex i (λ ψ → C (Y ψ)))