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

--------------------------------------------------------------------------------
-- Towards the homotopy forms of RS 4.8 / RS 4.12: the outer product over a
-- cofibrant shape preserves truncation levels.  Lemma 3.15.
--
-- This module builds the two clean exo helpers feeding the total-space
-- contractibility argument (used with `FundamentalId` to characterize the
-- identity type of the match of a cofibrant product).
--------------------------------------------------------------------------------

module Extension.PiTruncation where

open import Extension.Prelude
open import Extension.RS46 using (Fib-iso-contr')
open import Extension.FundamentalId using (fundamental-id)

private
  variable
    ℓ ℓ' ℓ'' ℓΨ : Level

-- A fibrewise exo-isomorphism lifts to an exo-isomorphism of outer products.
Πᵉ-fam-iso : {A : UUᵉ ℓ} {X : A → UUᵉ ℓ'} {X' : A → UUᵉ ℓ'}
           → ((a : A) → X a ≅ X' a) → Πᵉ A X ≅ Πᵉ A X'
Πᵉ-fam-iso e =
    (λ g a → pr1ᵉ (e a) (g a))
  ,ᵉ ( (λ h a → pr1ᵉ (pr2ᵉ (e a)) (h a))
     ,ᵉ ( (λ g → funextᵉ (λ a → pr1ᵉ (pr2ᵉ (pr2ᵉ (e a))) (g a)))
         ,ᵉ (λ h → funextᵉ (λ a → pr2ᵉ (pr2ᵉ (pr2ᵉ (e a))) (h a))) ) )

-- The type-theoretic axiom of choice, at the outer level: a family of sums of
-- sections is a section of the family of sums.  (Both round trips are η.)
ACᵉ : {A : UUᵉ ℓ} {X : A → UUᵉ ℓ'} {Z : (a : A) → X a → UUᵉ ℓ''}
    → Σᵉ (Πᵉ A X) (λ g → Πᵉ A (λ a → Z a (g a))) ≅ Πᵉ A (λ a → Σᵉ (X a) (Z a))
ACᵉ =
    (λ w a → pr1ᵉ w a ,ᵉ pr2ᵉ w a)
  ,ᵉ ( (λ k → (λ a → pr1ᵉ (k a)) ,ᵉ (λ a → pr2ᵉ (k a)))
     ,ᵉ ( (λ w → reflᵉ) ,ᵉ (λ k → reflᵉ) ) )

-- Forward based-path space is contractible.
fwd-path-contr : {A : UU ℓ} (a₀ : A) → is-contr (Σ A (λ a → Id a₀ a))
fwd-path-contr a₀ = (a₀ , refl) , (λ {(a , refl) → refl})

--------------------------------------------------------------------------------
-- Total-space contractibility: for a fixed section f₀, the total space (over the
-- match of the outer product) of the pointwise-identity products is contractible.
-- This is the RS 4.6 argument for the based-path family; with `FundamentalId` it
-- characterizes the identity type of the match.
--------------------------------------------------------------------------------

module _ {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓ) (Y : Ψ → UU ℓ)
         (f₀ : Πᵉ Ψ (λ ψ → C (Y ψ)))
       where

  private
    IdF : (g : Πᵉ Ψ (λ ψ → C (Y ψ))) → Ψ → UU ℓ
    IdF g ψ = Id (ic (f₀ ψ)) (ic (g ψ))

    WY : isFibrant (Πᵉ Ψ (λ ψ → C (Y ψ)))
    WY = Π-fibrant-witness (cofΨ Y)

  -- public: these three form the statement of `funext-Id-equiv` (and are
  -- referenced by the paper index src/index.agda)
  FMY : UU (ℓΨ ⊔ ℓ)
  FMY = fibrant-match WY

  private
    αY : C FMY → Πᵉ Ψ (λ ψ → C (Y ψ))
    αY = pr1ᵉ (pr2ᵉ (fibrant-witness WY))

  Q' : FMY → UU (ℓΨ ⊔ ℓ)
  Q' w = fibrant-match (Π-fibrant-witness (cofΨ (IdF (αY (c w)))))

  private
    Big : UUᵉ (ℓΨ ⊔ ℓ)
    Big = Σᵉ (Πᵉ Ψ (λ ψ → C (Y ψ))) (λ g → Πᵉ Ψ (λ ψ → C (IdF g ψ)))

    WBig : isFibrant Big
    WBig = isFibrant-Σ WY (λ g → Π-fibrant-witness (cofΨ (IdF g)))

    Single : Ψ → UU ℓ
    Single ψ = Σ (Y ψ) (λ y → Id (ic (f₀ ψ)) y)

    Big≅ΠSingle : Big ≅ Πᵉ Ψ (λ ψ → C (Single ψ))
    Big≅ΠSingle =
      ≅-trans (ACᵉ {X = λ ψ → C (Y ψ)} {Z = λ ψ x → C (Id (ic (f₀ ψ)) (ic x))})
              (Πᵉ-fam-iso (λ ψ → exo-Σᵉ-equiv))

    ΠSingle-contr :
      Fib-is-contr (Πᵉ Ψ (λ ψ → C (Single ψ))) {Π-fibrant-witness (cofΨ Single)}
    ΠSingle-contr =
      contr-preserve-witness (cofΨ Single) (λ ψ → fwd-path-contr (ic (f₀ ψ)))

  -- Σ Q' contractible.  (Its type reduces to  is-contr (Σ FMY Q')  since the
  -- fibrant match of `Big` is that Σ, by `isFibrant-Σ`.)
  based-path-prod-contr : Fib-is-contr Big {WBig}
  based-path-prod-contr =
    Fib-iso-contr' (Π-fibrant-witness (cofΨ Single)) WBig
                   (≅-sym Big≅ΠSingle) ΠSingle-contr

  -- The identity type of the match, characterized as the match of the
  -- pointwise-identity product (the homotopy relative funext, RS 4.8 core).
  fY : Πᵉ Ψ (λ ψ → C (Y ψ)) → C FMY
  fY = pr1ᵉ (fibrant-witness WY)

  private
    gfY : (T : Πᵉ Ψ (λ ψ → C (Y ψ))) → αY (fY T) =ᵉ T
    gfY = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WY)))

    g₀ : Πᵉ Ψ (λ ψ → C (Y ψ))
    g₀ = αY (fY f₀)

    refl-sec : Πᵉ Ψ (λ ψ → C (IdF g₀ ψ))
    refl-sec ψ = c (=ᵉ-to-Id (exo-inv (happlyᵉ (gfY f₀) ψ)))

    q₀ : Q' (ic (fY f₀))
    q₀ = ic (pr1ᵉ (fibrant-witness (Π-fibrant-witness (cofΨ (IdF g₀)))) refl-sec)

  funext-Id-equiv : (w : FMY) → Id (ic (fY f₀)) w ≃ Q' w
  funext-Id-equiv w =
    (λ p → tr Q' p q₀) , fundamental-id (λ _ p → tr Q' p q₀) based-path-prod-contr w

--------------------------------------------------------------------------------
-- The outer product over a cofibrant shape preserves truncation levels
-- (generalizing `contr-preserve-witness` from is-contr to every level).
--
-- Induction is on the truncation level `𝕋` (= ℕ: constructors neg-two-𝕋,
-- succ-𝕋, the levels −2, −1, 0, …, not the unit type).  This is a fibrant
-- `data` type with no η, so eliminating it into an exo motive is not admissible
-- in base 2LTT: it would amount to a map `ℕ → ℕᵉ` (cofibrant exo-nat), an extra
-- axiom.  Here the motive would additionally contain the exo hypothesis
-- `(ψ : Ψ) → is-type t (Y ψ)`, so the split is blocked.
--
-- (This is not a restriction on fibrant elimination in general.  η-records, the
-- unit type, Σ, eliminate into exo motives definitionally by η; that is
-- why the fibrant and exo unit coincide, provably and with no axiom.  Only the
-- η-less `data` types like ℕ/𝕋 need an axiom.)
--
-- We stay inside the base theory by packaging the pointwise hypothesis as a
-- fibrant type (`Hyp`, via cofibrancy) and matching `t` last.
--------------------------------------------------------------------------------

private
  Hyp : {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓ) (Y : Ψ → UU ℓ) (t : 𝕋) → UU (ℓΨ ⊔ ℓ)
  Hyp cofΨ Y t = fibrant-match (Π-fibrant-witness (cofΨ (λ ψ → is-type t (Y ψ))))

  unwrapHyp : {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓ) (Y : Ψ → UU ℓ) (t : 𝕋)
            → Hyp cofΨ Y t → (ψ : Ψ) → is-type t (Y ψ)
  unwrapHyp cofΨ Y t h ψ =
    ic (pr1ᵉ (pr2ᵉ (fibrant-witness (Π-fibrant-witness (cofΨ (λ ψ → is-type t (Y ψ)))))) (c h) ψ)

  wrapHyp : {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓ) (Y : Ψ → UU ℓ) (t : 𝕋)
          → ((ψ : Ψ) → is-type t (Y ψ)) → Hyp cofΨ Y t
  wrapHyp cofΨ Y t h =
    ic (pr1ᵉ (fibrant-witness (Π-fibrant-witness (cofΨ (λ ψ → is-type t (Y ψ))))) (λ ψ → c (h ψ)))

  Πᵉ-pres : {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓ) (Y : Ψ → UU ℓ) (t : 𝕋)
          → Hyp cofΨ Y t → is-type t (fibrant-match (Π-fibrant-witness (cofΨ Y)))
  Πᵉ-pres cofΨ Y neg-two-𝕋 hyp = contr-preserve-witness (cofΨ Y) (unwrapHyp cofΨ Y neg-two-𝕋 hyp)
  Πᵉ-pres {Ψ = Ψ} cofΨ Y (succ-𝕋 t') hyp f' g' = goal
    where
    WYl  = Π-fibrant-witness (cofΨ Y)
    αYl  = pr1ᵉ (pr2ᵉ (fibrant-witness WYl))
    fYl  = pr1ᵉ (fibrant-witness WYl)
    fgY  = pr2ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WYl)))
    αf'  = αYl (c f')
    αg'  = αYl (c g')

    hY : (ψ : Ψ) → is-type (succ-𝕋 t') (Y ψ)
    hY = unwrapHyp cofΨ Y (succ-𝕋 t') hyp

    IdfamFG : Ψ → UU _
    IdfamFG ψ = Id (ic (αf' ψ)) (ic (αg' ψ))

    IH : is-type t' (fibrant-match (Π-fibrant-witness (cofΨ IdfamFG)))
    IH = Πᵉ-pres cofΨ IdfamFG t'
           (wrapHyp cofΨ IdfamFG t' (λ ψ → hY ψ (ic (αf' ψ)) (ic (αg' ψ))))

    step1 : is-type t' (Id (ic (fYl αf')) g')
    step1 = is-truncation-cong (funext-Id-equiv cofΨ Y αf' g') t' IH

    efg : Id (ic (fYl αf')) f'
    efg = =ᵉ-to-Id (fgY (c f'))

    goal : is-type t' (Id f' g')
    goal = tr (λ z → is-type t' (Id z g')) efg step1

Πᵉ-preserves-truncation :
    (t : 𝕋) {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓ) (Y : Ψ → UU ℓ)
  → ((ψ : Ψ) → is-type t (Y ψ))
  → is-type t (fibrant-match (Π-fibrant-witness (cofΨ Y)))
Πᵉ-preserves-truncation t cofΨ Y hY = Πᵉ-pres cofΨ Y t (wrapHyp cofΨ Y t hY)

{- References:

  [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

-}