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

--------------------------------------------------------------------------------
-- Lemma 2.2: for g : E → F with all strict fibres fibrant and F fibrant, the
-- coercion (x, q) ↦ (x, ι q) from the strict to the homotopy fibre is an
-- equivalence.
-- The homotopy fibre has to be read through fibrant matches, so we give:
--
--   * the strict singleton contraction E ≅ Σᵉ F (fibᵉ g)  (`Σ-fibres-≅`);
--   * `E-isFibrant`, whose match is definitionally the inner total space of
--     the matched fibres, so that the matched g is pr₁ (`total-is-match`);
--   * `canonical-fibre-equiv`, fibre-match p₀ ≃ fiber pr₁ …, whose underlying
--     map is the match rendering of (x, q) ↦ (x, ι q).
--
-- `strict-to-homotopy-ext` is the instance for the restriction fibration of a
-- cofibration with cofibrant domain, used in the proof of Lemma 4.2.
--------------------------------------------------------------------------------

module Extension.CanonicalFibre where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.Glue using (fibᵉ)

private
  variable
    ℓ ℓ' : Level

--------------------------------------------------------------------------------
-- Inner helper: the fibre of a Σ-projection over a is the family value at a,
-- via the canonical map  u ↦ ((a , u) , refl).
--------------------------------------------------------------------------------

module _ {A : UU ℓ} {P : A → UU ℓ'} (a : A) where

  value-to-fiber : P a → fiber (pr1 {B = P}) a
  value-to-fiber u = (a , u) , refl

  value-to-fiber-isEquiv : isEquiv value-to-fiber
  value-to-fiber-isEquiv =
    invertibles-are-equiv value-to-fiber (to' , (tf' , ft'))
    where
    to' : fiber (pr1 {B = P}) a → P a
    to' ((a' , p') , q) = tr P q p'
    tf' : (to' ∘ value-to-fiber) ~ id
    tf' u = refl
    ft' : (value-to-fiber ∘ to') ~ id
    ft' ((a' , p') , refl) = refl

--------------------------------------------------------------------------------
-- The canonical comparison, for a fibrewise-fibrant map into a fibrant base.
--------------------------------------------------------------------------------

-- E and F are taken at a common level: the fibrant match of E must live at
-- the level of E itself, and it is the total space of the matched fibres.
module _ {E F : UUᵉ ℓ}
         (WF : isFibrant F) (g : E → F)
         (fibW : (p : F) → isFibrant (fibᵉ g p))
       where

  matchF : UU ℓ
  matchF = fibrant-match WF

  to-match : F → C matchF
  to-match = pr1ᵉ (fibrant-witness WF)

  from-match : C matchF → F
  from-match = pr1ᵉ (pr2ᵉ (fibrant-witness WF))

  from-to-match : (p : F) → from-match (to-match p) =ᵉ p
  from-to-match = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WF)))

  -- matches of the strict fibres
  fibre-match : F → UU ℓ
  fibre-match p = fibrant-match (fibW p)

  -- the inner total space (= the match of E, see below)
  total-match : UU ℓ
  total-match = Σ matchF (λ m → fibre-match (from-match (c m)))

  -- The strict singleton contraction:  E  ≅  Σᵉ (p : F). fibᵉ g p.
  Σ-fibres-≅ : E ≅ Σᵉ F (fibᵉ g)
  Σ-fibres-≅ = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))
    where
    to : E → Σᵉ F (fibᵉ g)
    to x = g x ,ᵉ (x ,ᵉ reflᵉ)
    from : Σᵉ F (fibᵉ g) → E
    from (p ,ᵉ (x ,ᵉ q)) = x
    from-to : (x : E) → from (to x) =ᵉ x
    from-to x = reflᵉ
    to-from : (w : Σᵉ F (fibᵉ g)) → to (from w) =ᵉ w
    to-from (.(g x) ,ᵉ (x ,ᵉ reflᵉ)) = reflᵉ

  -- E is fibrant, with fibrant match `total-match` (definitionally).
  E-isFibrant : isFibrant E
  E-isFibrant = isFibrant-iso (≅-sym Σ-fibres-≅) (isFibrant-Σ WF fibW)

  -- Machine-checked witness that the match of E-isFibrant is total-match
  -- (the identity typechecks only because the two are definitionally equal).
  total-is-match : total-match → fibrant-match E-isFibrant
  total-is-match w = w

  -- The canonical map: an element of the strict-fibre match over p₀ sits,
  -- after strict realignment along  from-match (to-match p₀) =ᵉ p₀, over the
  -- reflected base point  ic (to-match p₀), with path refl.  This is the
  -- match rendering of  (x, q) ↦ (x, ι q).
  canonical-map : (p₀ : F)
    → fibre-match p₀
    → fiber (pr1 {B = λ m → fibre-match (from-match (c m))}) (ic (to-match p₀))
  canonical-map p₀ m =
    (ic (to-match p₀) ,
     ic (exo-tr (λ p → C (fibre-match p)) (exo-inv (from-to-match p₀)) (c m))) ,
    refl

  private
    shift : {p q : F} (e : p =ᵉ q) → fibre-match p → fibre-match q
    shift e m = ic (exo-tr (λ p → C (fibre-match p)) e (c m))

    shift-isEquiv : {p q : F} (e : p =ᵉ q) → isEquiv (shift e)
    shift-isEquiv reflᵉ =
      invertibles-are-equiv _ ((λ m → m) , ((λ m → refl) , (λ m → refl)))

  -- The canonical map is an equivalence.
  canonical-map-isEquiv : (p₀ : F) → isEquiv (canonical-map p₀)
  canonical-map-isEquiv p₀ =
    ∘-is-equiv (shift (exo-inv (from-to-match p₀)))
               (value-to-fiber (ic (to-match p₀)))
               (shift-isEquiv (exo-inv (from-to-match p₀)))
               (value-to-fiber-isEquiv (ic (to-match p₀)))

  canonical-fibre-equiv : (p₀ : F)
    → fibre-match p₀
      ≃ fiber (pr1 {B = λ m → fibre-match (from-match (c m))}) (ic (to-match p₀))
  canonical-fibre-equiv p₀ = canonical-map p₀ , canonical-map-isEquiv p₀

--------------------------------------------------------------------------------
-- Instance: the restriction fibration of a cofibration with cofibrant domain.
-- The strict fibres of  i* : Πᵉ Ψ (C∘Y) → Πᵉ Φ (C∘Y∘i)  are definitionally the
-- extension types, so the coercion map from the match of  Extᵢ(Y,a)  to the
-- homotopy fibre of the matched restriction map is an equivalence.
--------------------------------------------------------------------------------

-- (Φ and Ψ at a common level, so that domain and codomain of the restriction
-- map live at the same level, as the packaging above requires.)
module _ {ℓS : Level} {Φ Ψ : UUᵉ ℓS} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (cofΦ : isCofibrant Φ ℓ) (Y : Ψ → UU ℓ)
       where

  strict-to-homotopy-ext =
    canonical-fibre-equiv (Π-fibrant-witness (cofΦ (λ φ → Y (i φ))))
                          (i* i Y)
                          (Ext-isFibrant cof Y)