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

--------------------------------------------------------------------------------
-- A repackaging of RS 4.10 (Extension.RS410, the homotopy extension property)
-- as a single Σᵉ-valued, opaque operation.
--
-- the strict extension `a'` and its homotopy agreement `a'-agrees-b`, are
-- related by a conversion (the type of `a'-agrees-b` mentions `a'` itself).
-- Consumers that instantiate them at large argument terms (in particular
-- Extension.GlueConstructorPackage, where the total section `b` is the centre
-- of a contractibility proof built from the whole Step A-C equivalence chain)
-- force Agda to re-check this conversion at the instance, which unfolds the
-- RS46 contractibility engine applied to the large arguments and explodes
-- (observed: > 20 min / > 26 GB).  Here the conversion is performed once, at
-- the generic level where all arguments are variables (cheap), and the result
-- is exported behind an `opaque` definition, so instances only ever compare
-- argument spines against a rigid head.
--
-- The statement exported is RS 4.10, packaged:
--   hep = (a' , λ ψ. c (a'-agrees-b ψ))  :
--     Σᵉ (w : Extᵢ(Y, a)). Πψ. C (Id (w₀ ψ) (b ψ)).
--------------------------------------------------------------------------------

module Extension.RS410Pack where

open import Extension.Prelude
open import Extension.Core using (Ext)
open import Extension.CofibFibration using (is-cofib)
open import Extension.RS410 using (a' ; a'-agrees-b)
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

  -- The packaged homotopy extension property: a strict extension of a along i
  -- together with a pointwise homotopy between its underlying section and b.
  HEP : UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓ)
  HEP = Σᵉ (Ext i (λ ψ → C (Y ψ)) a)
           (λ w → (ψ : Ψ) → C (Id (ic (pr1ᵉ w ψ)) (ic (b ψ))))

  opaque
    hep : HEP
    hep = a' cof triv Y b a e
        ,ᵉ (λ ψ → c (a'-agrees-b cof triv Y b a e ψ))

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

-}