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

--------------------------------------------------------------------------------
-- Σ-types are closed under truncation levels (inner HoTT), and the converse
-- fibre statement.  The one ingredient Uskuplu's library does not already
-- provide for lifting the product-case homotopy RS 4.8 / RS 4.12 to the
-- extension type.  Lemma 3.15.
--------------------------------------------------------------------------------

module Extension.SigmaTruncation where

open import Extension.Prelude

private
  variable
    ℓ ℓ' : Level

-- Σ of a contractible base with contractible fibres is contractible.
Σ-contr : {A : UU ℓ} {P : A → UU ℓ'}
        → is-contr A → ((a : A) → is-contr (P a)) → is-contr (Σ A P)
Σ-contr {A = A} {P} cA hP = (a₀ , p₀) , contr
  where
  a₀ = center A cA
  p₀ = center (P a₀) (hP a₀)
  contr : (w : Σ A P) → Id w (a₀ , p₀)
  contr (a , p) =
    dep-pair⁼ _ _ (centrality A cA a , centrality (P a₀) (hP a₀) (tr P (centrality A cA a) p))

-- Σ preserves every truncation level.
Σ-preserves-truncation :
    (t : 𝕋) (A : UU ℓ) (P : A → UU ℓ')
  → is-type t A → ((a : A) → is-type t (P a)) → is-type t (Σ A P)
Σ-preserves-truncation neg-two-𝕋 A P hA hP = Σ-contr hA hP
Σ-preserves-truncation (succ-𝕋 t') A P hA hP w w' =
  is-truncation-cong (Σ-Id-char w w') t' IH
  where
  IH : is-type t' (dep-pair-Id w w')
  IH = Σ-preserves-truncation t'
         (Id (pr1 w) (pr1 w')) (λ p → Id (tr P p (pr2 w)) (pr2 w'))
         (hA (pr1 w) (pr1 w'))
         (λ p → hP (pr1 w') (tr P p (pr2 w)) (pr2 w'))

-- Converse: with a truncated total space and base, each fibre is truncated.
Σ-base-fibre-truncation :
    (t : 𝕋) {A : UU ℓ} {P : A → UU ℓ'}
  → is-type t (Σ A P) → is-type t A → (a : A) → is-type t (P a)
Σ-base-fibre-truncation t {A} {P} hΣ hA a =
  is-truncation-cong P≃fiber t fiber-is-type
  where
  P≃fiber : P a ≃ fiber (pr1 {B = P}) a
  P≃fiber = to' , invertibles-are-equiv to' (from' , (ft' , tf'))
    where
    to' : P a → fiber (pr1 {B = P}) a
    to' p = (a , p) , refl
    from' : fiber (pr1 {B = P}) a → P a
    from' ((a' , p') , q) = tr P q p'
    ft' : (from' ∘ to') ~ id
    ft' p = refl
    tf' : (to' ∘ from') ~ id
    tf' ((a' , p') , refl) = refl

  fiber-is-type : is-type t (fiber (pr1 {B = P}) a)
  fiber-is-type =
    Σ-preserves-truncation t (Σ A P) (λ w → Id (pr1 w) a)
      hΣ (λ w → type-hrchy A t hA (pr1 w) a)

{- References:

  [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

  [RS]         Emily Riehl and Michael Shulman.  A type theory for synthetic
               ∞-categories.  Higher Structures 1(1):147-224, 2017.
               doi:10.21136/hs.2017.06

-}