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

--------------------------------------------------------------------------------
-- RS 4.10, the homotopy extension property.  Lemma 3.14
-- (and Lemma 3.14).
--
--   Given a total section  b : Πψ.A,  a partial section  a : Πφ.A∘i,  and a weak
--   boundary agreement  e : Πφ. a φ = b(iφ),  there is a strict extension
--   a' : Extᵢ(A, a)  (agreeing with a strictly on Φ) together with a homotopy
--   a' ≈ b  extending e.
--
-- Proof (the paper's): the extension type of the singleton family
-- Y'ψ ≔ Σ(y:Yψ). y = bψ  (each fibre contractible) with boundary  (a,e)  is
-- contractible by `RS46`, hence inhabited; projecting the inhabitant's underlying
-- section gives a' and the homotopy.  This strictifies weak boundary data.
--------------------------------------------------------------------------------

module Extension.RS410 where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RelFunext using (satisfies-rel-funext)

private
  variable
    ℓ ℓΦ ℓΨ : Level

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (triv : satisfies-rel-funext cof)
         (Y : Ψ → UU ℓ) (b : (ψ : Ψ) → C (Y ψ))
         (a : (φ : Φ) → C (Y (i φ)))
         (e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ))))
       where

  private
    -- the singleton (based-path) family; each fibre is contractible
    Y' : Ψ → UU ℓ
    Y' ψ = Σ (Y ψ) (λ y → Id y (ic (b ψ)))

    cY' : (ψ : Ψ) → is-contr (Y' ψ)
    cY' ψ = path-type-is-contr (ic (b ψ))

    -- boundary datum, packaging the partial section with the weak agreement
    bdry : (φ : Φ) → C (Y' (i φ))
    bdry φ = c (ic (a φ) , e φ)

    fibW : isFibrant (Ext i (λ ψ → C (Y' ψ)) bdry)
    fibW = Ext-isFibrant cof Y' bdry

    -- Relative function extensionality makes the extension type contractible.
    ext-contr : Fib-is-contr (Ext i (λ ψ → C (Y' ψ)) bdry) {fibW}
    ext-contr = triv Y' cY' bdry

    w : Ext i (λ ψ → C (Y' ψ)) bdry
    w = pr1ᵉ (pr2ᵉ (fibrant-witness fibW)) (c (center _ ext-contr))

    wsec : (ψ : Ψ) → C (Y' ψ)
    wsec = ext-app w

  -- The strict extension: agrees with a strictly on Φ.
  a' : Ext i (λ ψ → C (Y ψ)) a
  a' = (λ ψ → c (pr1 (ic (wsec ψ))))
     ,ᵉ exo-ap (λ s φ → c (pr1 (ic (s φ)))) (pr2ᵉ w)

  -- a' agrees with the total section b up to homotopy (the extension of e).
  a'-agrees-b : (ψ : Ψ) → Id (ic (ext-app a' ψ)) (ic (b ψ))
  a'-agrees-b ψ = pr2 (ic (wsec ψ))

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

-}