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

--------------------------------------------------------------------------------
-- Strictifications: the strict fibre versus the homotopy fibre.
--
-- Lemma 2.2 (and the Strictifications
-- section).  "If f : Y ↠ X is a fibration and X is fibrant, then the homotopy
-- fibre and the strict fibre of f over any x : X are equivalent."
--
-- By Uskuplu/[2LTT, Lem. 3.9] a fibration over a fibrant base is the same as a
-- family of fibrant types over a fibrant (inner) base.  We therefore phrase the
-- comparison for an inner base  X : UU  and inner family  P : X → UU, no
-- fibrancy hypotheses are then needed, they are built into `UU`.  The two fibres
-- are both computed to be  P x₀:
--
--   * the strict fibre  Σᵉ (C X) (λ x. (c x₀ =ᵉ x) ×ᵉ C (P …))  is exo-iso to
--     C (P x₀), strict singleton contraction  (`strict-sing-≅`);
--   * the homotopy fibre  Σ X (λ x. Id x₀ x × P x)  is equivalent to  P x₀,
--     based-path contraction  (`hom-sing-≃`).
--
-- Hence the strict fibre is a fibrant type whose fibrant match is `P x₀`, and
-- the homotopy fibre is `≃ P x₀`: the two agree.  (`strict-vs-homotopy-fibre`.)
--------------------------------------------------------------------------------

module Extension.Fibre where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓ ℓX : Level

--------------------------------------------------------------------------------
-- Strict singleton contraction (exo level).  For a family P over an exo-type X,
-- the strict fibre of  Σᵉ X P → X  over x₀ is strictly isomorphic to  P x₀.
--------------------------------------------------------------------------------

Sfibre : {X : UUᵉ ℓX} (P : X → UUᵉ ℓ) (x₀ : X) → UUᵉ (ℓX ⊔ ℓ)
Sfibre {X = X} P x₀ = Σᵉ X (λ x → (x₀ =ᵉ x) ×ᵉ P x)

strict-sing-≅ : {X : UUᵉ ℓX} (P : X → UUᵉ ℓ) (x₀ : X)
              → Sfibre P x₀ ≅ P x₀
strict-sing-≅ {X = X} P x₀ = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))
  where
  to : Sfibre P x₀ → P x₀
  to (x ,ᵉ (e ,ᵉ p)) = exo-tr P (exo-inv e) p

  from : P x₀ → Sfibre P x₀
  from p = x₀ ,ᵉ (reflᵉ ,ᵉ p)

  from-to : (w : Sfibre P x₀) → from (to w) =ᵉ w
  from-to (x ,ᵉ (reflᵉ ,ᵉ p)) = reflᵉ

  to-from : (p : P x₀) → to (from p) =ᵉ p
  to-from p = reflᵉ

--------------------------------------------------------------------------------
-- Homotopy singleton contraction (inner level).  For an inner family P over an
-- inner type X, the homotopy fibre of  Σ X P → X  over x₀ is equivalent to P x₀.
--------------------------------------------------------------------------------

Hfibre : {X : UU ℓX} (P : X → UU ℓ) (x₀ : X) → UU (ℓX ⊔ ℓ)
Hfibre {X = X} P x₀ = Σ X (λ x → Id x₀ x × P x)

hom-sing-≃ : {X : UU ℓX} (P : X → UU ℓ) (x₀ : X)
           → Hfibre P x₀ ≃ P x₀
hom-sing-≃ {X = X} P x₀ = to , invertibles-are-equiv to (from , (from-to , to-from))
  where
  to : Hfibre P x₀ → P x₀
  to (x , (q , p)) = tr P (q ⁻¹) p

  from : P x₀ → Hfibre P x₀
  from p = x₀ , (refl , p)

  from-to : (from ∘ to) ~ id
  from-to (x , (refl , p)) = refl

  to-from : (to ∘ from) ~ id
  to-from p = refl

--------------------------------------------------------------------------------
-- The comparison (Lemma 2.2).
--
-- For an inner base X : UU and inner family P : X → UU, the strict fibre and the
-- homotopy fibre over x₀ both compute to P x₀.  We package this as: the strict
-- fibre (with C-coerced fibres, so it is an exo-type) is exo-iso to C (P x₀),
-- exhibiting it as fibrant with match P x₀; and the homotopy fibre is ≃ P x₀.
--------------------------------------------------------------------------------

module _ {X : UU ℓX} (P : X → UU ℓ) (x₀ : X) where

  -- The strict fibre of the coerced family, as an exo-type.
  Sfibreᶜ : UUᵉ (ℓX ⊔ ℓ)
  Sfibreᶜ = Sfibre (λ x → C (P (ic x))) (c x₀)

  -- Strict fibre: exo-iso to the exo image of the fibre  P x₀  (so it is a
  -- fibrant type whose fibrant match is  P x₀).
  strict-fibre-match : Sfibreᶜ ≅ C (P x₀)
  strict-fibre-match = strict-sing-≅ (λ x → C (P (ic x))) (c x₀)

  -- Homotopy fibre: equivalent to the fibre  P x₀.
  homotopy-fibre-equiv : Hfibre P x₀ ≃ P x₀
  homotopy-fibre-equiv = hom-sing-≃ P x₀

  -- Conclusion (Lemma 2.2): both the strict fibre and the
  -- homotopy fibre are  P x₀,  hence "equivalent to each other", the strict
  -- fibre via the exo-iso  `strict-fibre-match`,  the homotopy fibre via the
  -- inner equivalence  `homotopy-fibre-equiv`.
--
  -- NB the comparison is necessarily via the shared fibre  P x₀,  not via a
  -- pointwise iso of the boundary conditions:  there is no map  Id a b → a =ᵉ b
  -- (a fibrant type cannot be eliminated into an exo target, homotopy equality
  -- does not imply strict equality), which is why the paper's proof runs
  -- through the singleton contraction rather than a pointwise comparison.

{- References:

  [2LTT]       Danil Annenkov, Paolo Capriotti, Nicolai Kraus and Christian Sattler.
               Two-level type theory and applications.  Mathematical Structures in
               Computer Science 33(8):688-743, 2023.  doi:10.1017/s0960129523000130

  [2LTT-Agda]  Elif Uskuplu.  2LTT-Agda: formalization of 2LTT in Agda.
               https://github.com/ElifUskuplu/2LTT-Agda, commit b064091 (6 August 2025).
               Described in: Elif Uskuplu, Formalizing two-level type theory with
               cofibrant exo-nat, Mathematical Structures in Computer Science 35:e30,
               2025.  doi:10.1017/S0960129525100297

-}