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

--------------------------------------------------------------------------------
-- Definition 3.9 and Lemma 3.11.
--
-- `(i, U)` satisfies relative function extensionality if Extᵢ(A,a) is
-- fibrantly contractible for every pointwise contractible fibrant A.  By
-- Remark 3.10 this is the trivial-fibration half of the 2LTT
-- cofibration property, read through [2LTT, Lem 3.18].  So:
--
--   * `is-cofib-2LTT`: the fibration half plus `satisfies-rel-funext`;
--   * `rel-funext-holds-2LTT`: Lemma 3.11, definitional in this packaging,
--     since the trivial half is the statement;
--   * `rel-funext-holds`: for cofibrant shapes the trivial half follows from
--     the fibration half alone, which is the content of Extension.RS46;
--   * `cofibrant-is-cofib-2LTT`: the same, packaged as a full cofibration.
--
-- RS have to postulate relative funext because their cofibrations are bare
-- shape inclusions.
--------------------------------------------------------------------------------

module Extension.RelFunext where

open import Extension.Prelude
open import Extension.CofibFibration
open import Extension.RS46 using (RS46)

private
  variable
    ℓ ℓΦ ℓΨ : Level

-- Definition 3.9, the predicate, for a fixed cofibration `i`; equivalently,
-- the trivial-fibration half of [2LTT, Def 3.13] for the restriction map.
module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : is-cofib i ℓ) where

  satisfies-rel-funext : UUᵉ (lsuc ℓ ⊔ ℓΦ ⊔ ℓΨ)
  satisfies-rel-funext =
      (Y : Ψ → UU ℓ) → ((ψ : Ψ) → is-contr (Y ψ)) → (a : (φ : Φ) → C (Y (i φ)))
    → is-contr (fibrant-match (Ext-isFibrant cof Y a))

-- The full 2LTT cofibration [2LTT, Def 3.13, via the Lem 3.18
-- characterization]: fibration half plus trivial-fibration half.
is-cofib-2LTT : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (ℓ : Level)
              → UUᵉ (lsuc (ℓΦ ⊔ ℓΨ ⊔ ℓ))
is-cofib-2LTT i ℓ = Σᵉ (is-cofib i ℓ) satisfies-rel-funext

-- Lemma 3.11 (paper form): every full 2LTT cofibration satisfies
-- relative funext, no cofibrancy of Φ or Ψ.  Definitional in this packaging.
rel-funext-holds-2LTT : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
                        (c2 : is-cofib-2LTT i ℓ)
                      → satisfies-rel-funext (pr1ᵉ c2)
rel-funext-holds-2LTT c2 = pr2ᵉ c2

-- Cofibrant shapes discharge the trivial half from the fibration half alone:
-- the homotopy RS 4.6 of `Extension.RS46` inhabits the predicate.
rel-funext-holds : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
                   (cof : is-cofib i ℓ) (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ)
                 → satisfies-rel-funext cof
rel-funext-holds cof cofΨ cofΦ Y cY a = RS46 cof cofΨ cofΦ Y cY a

-- ... and hence upgrade the fibration half to a full 2LTT cofibration.
cofibrant-is-cofib-2LTT : {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
                          (cof : is-cofib i ℓ)
                          (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ)
                        → is-cofib-2LTT i ℓ
cofibrant-is-cofib-2LTT cof cofΨ cofΦ = cof ,ᵉ rel-funext-holds cof cofΨ cofΦ

{- References:

  [2LTT]       Danil Annenkov, Paolo Capriotti, Nicolai Kraus and Christian Sattler.
               Two-level type theory and applications.  Mathematical Structures in
               Computer Science 33(8):688-743, 2023.  doi:10.1017/s0960129523000130

  [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

-}