{-# OPTIONS --without-K --exact-split --two-level #-}
--------------------------------------------------------------------------------
-- The homotopical RS lemmas (RS17 §4.6–4.12).
-- Lemma 3.11 (relative funext), Lemma 3.13, Lemma 3.14, Lemma 3.15.
--
-- These are genuinely two-level: they assert homotopical properties (contractible,
-- n-type, …) of the extension type, which live in its *fibrant match*. A full
-- proof needs "restriction along a cofibration is a fibration" (so that `Ext` is
-- a fibrant strict fibre), the Leibniz-exponential machinery of [2LTT, §3], which
-- the base library does not provide. We formalize:
--
-- * the strict form of Lemma 3.11 (relative function extensionality): if each
-- fibre is *strictly* contractible then `Ext` is strictly contractible. This
-- is pure strict-fibre content and needs no cofibrancy. (`Ext-strict-contr`.)
-- * the genuine homotopy ingredient available from cofibrancy: the total-section
-- type of a pointwise-contractible fibrant family over a cofibrant shape has
-- contractible fibrant match. (`total-sections-contr`.)
--
-- Together these are the two halves of the RS 4.6 argument; the missing link is
-- the fibrancy of `Ext` as a strict fibre of the restriction map (see README).
--------------------------------------------------------------------------------
module Extension.RSHomotopy where
open import Extension.Prelude
open import Extension.Core
private
variable
ℓΦ ℓΨ ℓA : Level
--------------------------------------------------------------------------------
-- RS 4.6, strict form. If each A ψ is strictly contractible, then
-- Extᵢ(A , a) is strictly contractible, for any boundary datum a and cofibration
-- i (no fibrancy or cofibrancy needed).
--------------------------------------------------------------------------------
module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {A : Ψ → UUᵉ ℓA}
(a : (φ : Φ) → A (i φ)) (cA : (ψ : Ψ) → is-contrᵉ (A ψ))
where
private
-- the pointwise centres form a total section
centre : (ψ : Ψ) → A ψ
centre ψ = pr1ᵉ (cA ψ)
-- which restricts strictly to any given boundary a (each fibre is a strict
-- proposition, having a centre)
e₀ : restrict i centre =ᵉ a
e₀ = funextᵉ (λ φ → pr2ᵉ (cA (i φ)) (a φ))
Ext-strict-contr : is-contrᵉ (Ext i A a)
Ext-strict-contr = (centre ,ᵉ e₀) ,ᵉ contraction
where
contraction : (fq : Ext i A a) → (centre ,ᵉ e₀) =ᵉ fq
contraction (f ,ᵉ q) = ext-≡ (funextᵉ (λ ψ → pr2ᵉ (cA ψ) (f ψ)))
--------------------------------------------------------------------------------
-- The homotopy ingredient of RS 4.6 available from cofibrancy: if Ψ is cofibrant
-- and each A ψ : UU is (inner-)contractible, the total-section type
-- Πᵉ Ψ (λ ψ. C (A ψ)) has contractible fibrant match. (Directly from Uskuplu's
-- `contr-preserve-witness`.)
--------------------------------------------------------------------------------
module _ {Ψ : UUᵉ ℓΨ} (cofΨ : isCofibrant Ψ ℓA)
(A : Ψ → UU ℓA) (cA : (ψ : Ψ) → is-contr (A ψ))
where
total-sections-contr :
Fib-is-contr (Πᵉ Ψ (λ ψ → C (A ψ))) {Π-fibrant-witness (cofΨ A)}
total-sections-contr = contr-preserve-witness (cofΨ A) cA
{- 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
[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
[2LTT-Agda] Elif Uskuplu. 2LTT-Agda: formalization of 2LTT in Agda.
https://github.com/ElifUskuplu/2LTT-Agda, commit b064091 (6 August 2025).
Described in: Elif Uskuplu, Formalizing two-level type theory with
cofibrant exo-nat, Mathematical Structures in Computer Science 35:e30,
2025. doi:10.1017/S0960129525100297
-}