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

--------------------------------------------------------------------------------
-- The map-level cofibration machinery of [2LTT, §3], re-derived on top of
-- Uskuplu's library, so that the extension type is a fibrant strict fibre and
-- the homotopical RS lemmas become provable.
--
--   * `is-cofib i`: a map i is a 2LTT cofibration iff restriction along i is a
--     fibration for every fibrant family (the [2LTT, Lem 3.18] characterization,
--     taken as the working definition);
--   * `Ext-isFibrant`: `Ext` along a cofibration into a fibrant family is
--     fibrant (immediate: it is a strict fibre of the restriction fibration);
--   * `reindex`: the total-section space is the Σ of extension types over the
--     restricted boundaries:  Πψ.A ≅ Σ(z : Πφ.A∘i). Extᵢ(A,z).
--------------------------------------------------------------------------------

module Extension.CofibFibration where

open import Extension.Prelude
open import Extension.Core

private
  variable
    ℓΦ ℓΨ ℓ : Level

--------------------------------------------------------------------------------
-- Cofibrations of maps, and fibrancy of the extension type.
--------------------------------------------------------------------------------

-- Restriction along i, on a fibrant family Y : Ψ → UU.
i* : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (Y : Ψ → UU ℓ)
   → ((ψ : Ψ) → C (Y ψ)) → ((φ : Φ) → C (Y (i φ)))
i* i Y = restrict i

-- [2LTT, Lem 3.18] as definition: i is a cofibration iff i* is a fibration for
-- every fibrant family.
is-cofib : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (ℓ : Level)
         → UUᵉ (lsuc (ℓΦ ⊔ ℓΨ ⊔ ℓ))
is-cofib {Φ = Φ} {Ψ} i ℓ = (Y : Ψ → UU ℓ) → isFibration (i* i Y)

-- The extension type along a cofibration, into a fibrant family, is fibrant:
-- it is the strict fibre of the restriction fibration over a.
Ext-isFibrant : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
              → is-cofib i ℓ → (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
              → isFibrant (Ext i (λ ψ → C (Y ψ)) a)
Ext-isFibrant cof Y a = cof Y a

--------------------------------------------------------------------------------
-- Reindexing: total sections = Σ of extension types over restricted boundaries.
--------------------------------------------------------------------------------

reindex : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (A : Ψ → UUᵉ ℓ)
        → ((ψ : Ψ) → A ψ) ≅ Σᵉ ((φ : Φ) → A (i φ)) (Ext i A)
reindex i A = to ,ᵉ (from ,ᵉ (from-to ,ᵉ to-from))
  where
  to : ((ψ : _) → A ψ) → Σᵉ ((φ : _) → A (i φ)) (Ext i A)
  to f = restrict i f ,ᵉ (f ,ᵉ reflᵉ)

  from : Σᵉ ((φ : _) → A (i φ)) (Ext i A) → ((ψ : _) → A ψ)
  from w = pr1ᵉ (pr2ᵉ w)

  from-to : (f : (ψ : _) → A ψ) → from (to f) =ᵉ f
  from-to f = reflᵉ

  to-from : (w : Σᵉ ((φ : _) → A (i φ)) (Ext i A)) → to (from w) =ᵉ w
  to-from (z ,ᵉ (f ,ᵉ e)) =
    dep-pair-=ᵉ _ _ (e ,ᵉ ext-≡ (pr1ᵉ-exo-tr-const e (f ,ᵉ reflᵉ)))

{- 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

-}