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

--------------------------------------------------------------------------------
-- RS 4.6 (relative function extensionality), homotopy form.
-- the paper, Lemma 3.11 / Lemma 3.11.
--
--   If  i : Φ ↪ Ψ  is a cofibration with Φ, Ψ cofibrant, and  A : Ψ → UU  is a
--   fibrant family with each  A ψ  contractible, then  Extᵢ(A , a)  is
--   contractible (in the fibrant sense: its fibrant match is contractible).
--
-- Proof (the paper's argument, made precise): the total-section space is the Σ
-- of extension types over restricted boundaries (`reindex`); it is contractible
-- (cofibrancy + `contr-preserve-witness`); the base is contractible; so each
-- fibre, an extension type, is contractible (`Σ-base-contr-fibre-contr`).
--------------------------------------------------------------------------------

module Extension.RS46 where

open import Extension.Prelude
open import Extension.Core
open import Extension.GlueUA using (contr-contr-isEquiv ; contr-map-fibre-contr)
open import Extension.CofibFibration

private
  variable
    ℓ ℓ' ℓΦ ℓΨ : Level

--------------------------------------------------------------------------------
-- Inner HoTT: a Σ-type with contractible total space and contractible base has
-- contractible fibres.
--------------------------------------------------------------------------------

Σ-base-contr-fibre-contr : {A : UU ℓ} {P : A → UU ℓ'}
                         → is-contr (Σ A P) → is-contr A → (a : A) → is-contr (P a)
Σ-base-contr-fibre-contr {A = A} {P} cΣ cA a =
  is-contr-cong fiber≃P (contr-map-fibre-contr cΣ cA pr1 a)
  where
  fiber≃P : fiber pr1 a ≃ P a
  fiber≃P = to' , invertibles-are-equiv to' (from' , (ft' , tf'))
    where
    to' : fiber pr1 a → P a
    to' ((a' , p') , q) = tr P q p'
    from' : P a → fiber pr1 a
    from' p = (a , p) , refl
    ft' : (from' ∘ to') ~ id
    ft' ((a' , p') , refl) = refl
    tf' : (to' ∘ from') ~ id
    tf' p = refl

-- Level-general transport of match-contractibility along an exo-iso (the
-- library's `Fib-iso-contr` forces both sides to one level; `is-contr-cong` is
-- level-general, and an exo-iso  A ≅ B  of fibrant types induces an inner
-- equivalence of their matches).
Fib-iso-contr' : {A : UUᵉ ℓ} {B : UUᵉ ℓ'} (W : isFibrant A) (V : isFibrant B)
               → A ≅ B → Fib-is-contr A {W} → Fib-is-contr B {V}
Fib-iso-contr' W V iso cA =
  is-contr-cong equiv cA
  where
  wA = fibrant-witness W
  wB = fibrant-witness V
  MA = fibrant-match W
  MB = fibrant-match V
  j : C MA ≅ C MB
  j = ≅-trans (≅-sym wA) (≅-trans iso wB)
  jf  = pr1ᵉ j
  jg  = pr1ᵉ (pr2ᵉ j)
  jgf = pr1ᵉ (pr2ᵉ (pr2ᵉ j))
  jfg = pr2ᵉ (pr2ᵉ (pr2ᵉ j))
  equiv : MA ≃ MB
  equiv = (λ x → ic (jf (c x)))
        , invertibles-are-equiv _
            ( (λ y → ic (jg (c y)))
            , ( (λ x → =ᵉ-to-Id (jgf (c x)))
              , (λ y → =ᵉ-to-Id (jfg (c y))) ) )

--------------------------------------------------------------------------------
-- RS 4.6, homotopy form.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ)
         (Y : Ψ → UU ℓ) (cY : (ψ : Ψ) → is-contr (Y ψ))
         (a : (φ : Φ) → C (Y (i φ)))
       where

  private
    CY : Ψ → UUᵉ ℓ
    CY ψ = C (Y ψ)

    -- total sections and restricted boundaries are fibrant and contractible
    contrΨ : Fib-is-contr (Πᵉ Ψ CY) {Π-fibrant-witness (cofΨ Y)}
    contrΨ = contr-preserve-witness (cofΨ Y) cY

    WΦ : isFibrant (Πᵉ Φ (λ φ → C (Y (i φ))))
    WΦ = Π-fibrant-witness (cofΦ (λ φ → Y (i φ)))

    contrΦ : Fib-is-contr (Πᵉ Φ (λ φ → C (Y (i φ)))) {WΦ}
    contrΦ = contr-preserve-witness (cofΦ (λ φ → Y (i φ))) (λ φ → cY (i φ))

    -- each extension type is fibrant; assemble the reindexed Σ
    Qz : (z : (φ : Φ) → C (Y (i φ))) → isFibrant (Ext i CY z)
    Qz = Ext-isFibrant cof Y

    contrRHS : Fib-is-contr (Σᵉ ((φ : Φ) → C (Y (i φ))) (Ext i CY)) {isFibrant-Σ WΦ Qz}
    contrRHS = Fib-iso-contr' (Π-fibrant-witness (cofΨ Y)) (isFibrant-Σ WΦ Qz)
                              (reindex i CY) contrΨ

    -- components of the fibrant structure on the boundary space
    fΦ : ((φ : Φ) → C (Y (i φ))) → C (fibrant-match WΦ)
    fΦ = pr1ᵉ (fibrant-witness WΦ)

    gΦ : C (fibrant-match WΦ) → ((φ : Φ) → C (Y (i φ)))
    gΦ = pr1ᵉ (pr2ᵉ (fibrant-witness WΦ))

    gfΦ : (z : (φ : Φ) → C (Y (i φ))) → gΦ (fΦ z) =ᵉ z
    gfΦ = pr1ᵉ (pr2ᵉ (pr2ᵉ (fibrant-witness WΦ)))

    E : ((φ : Φ) → C (Y (i φ))) → UU (ℓΦ ⊔ ℓΨ ⊔ ℓ)
    E z = fibrant-match (Qz z)

    -- fibrewise contractibility over the (contractible) match of the base
    fibre-contr : (x : fibrant-match WΦ) → is-contr (E (gΦ (c x)))
    fibre-contr = Σ-base-contr-fibre-contr contrRHS contrΦ

  -- RS 4.6: Ext is (fibrantly) contractible.  Transport the fibre at  fΦ a
  -- back along  gΦ (fΦ a) =ˢ a  to the fibre at a.
  RS46 : Fib-is-contr (Ext i CY a) {Ext-isFibrant cof Y a}
  RS46 = ic (exo-tr (λ z → C (is-contr (E z))) (gfΦ a)
                    (c (fibre-contr (ic (fΦ a)))))

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

-}