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

--------------------------------------------------------------------------------
-- The fundamental theorem of identity types (inner HoTT).
--
-- A fibrewise map out of a based-path family is a fibrewise equivalence iff its
-- total space is contractible.  We need the ⟸ direction, and the underlying
-- `fiberwise-from-total`.  These are the engine that turns "the total space of
-- pointwise-identity products is contractible" (provable as in `RS46`) into the
-- identity-type characterization of the extension type, and hence the homotopy
-- forms of RS 4.8 / RS 4.12.  Lemma 3.13, Lemma 3.15.
--------------------------------------------------------------------------------

module Extension.FundamentalId where

open import Extension.Prelude
open import Extension.GlueUA using (contr-contr-isEquiv)

private
  variable
    ℓ ℓ' ℓ'' : Level

-- Total map of a fibrewise map.
tot : {A : UU ℓ} {P : A → UU ℓ'} {Q : A → UU ℓ''} (f : (a : A) → P a → Q a)
    → Σ A P → Σ A Q
tot f (a , p) = a , f a p

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

  private
    -- naturality of f under transport
    nat : {a' a : A} (e : Id a' a) (p' : P a') → Id (f a (tr P e p')) (tr Q e (f a' p'))
    nat refl p' = refl

  -- fibrewise-from-total: if the total map is an equivalence, each component is.
  -- Each fibre of  f a  is a retract of the (contractible) fibre of  tot f.
  fiberwise-from-total : isEquiv (tot f) → (a : A) → isEquiv (f a)
  fiberwise-from-total etot a q = retract-of-singleton (retr , sect , retr-sect) (etot (a , q))
    where
    sect : fiber (f a) q → fiber (tot f) (a , q)
    sect (p , e) = (a , p) , dep-pair⁼ _ _ (refl , e)

    retr : fiber (tot f) (a , q) → fiber (f a) q
    retr ((a' , p') , w) =
        tr P (pr1 (inv-dep-pair⁼ _ _ w)) p'
      , nat (pr1 (inv-dep-pair⁼ _ _ w)) p' · pr2 (inv-dep-pair⁼ _ _ w)

    retr-sect : (retr ∘ sect) ~ id
    retr-sect (p , e) = ap retr' (htpy-inv-dep-pair⁼-dep-pair⁼ _ _ (refl , e))
      where
      -- retr as a function of the decomposed path components
      retr' : dep-pair-Id (a , f a p) (a , q) → fiber (f a) q
      retr' (e₁ , e₂) = tr P e₁ p , nat e₁ p · e₂

-- The fundamental theorem: a fibrewise map from a based-path family whose total
-- space is contractible is a fibrewise equivalence.
module _ {A : UU ℓ} {a₀ : A} {Q : A → UU ℓ'}
         (f : (a : A) → Id a₀ a → Q a)
       where

  private
    based-path-contr : is-contr (Σ A (λ a → Id a₀ a))
    based-path-contr = (a₀ , refl) , (λ {(a , refl) → refl})

  fundamental-id : is-contr (Σ A Q) → (a : A) → isEquiv (f a)
  fundamental-id cΣQ = fiberwise-from-total f (contr-contr-isEquiv based-path-contr cΣQ (tot f))

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

-}