{-# OPTIONS --without-K --exact-split --two-level #-}
--------------------------------------------------------------------------------
-- RS 4.11, the consistency check mentioned in Section 3: the naive form of
-- RS 4.8 together with RS 4.10 give RS 4.6.
--
-- To formalize the implication rather than re-derive RS 4.6, the three
-- properties are predicates on a fixed map carrying only the fibration half:
-- `HEP` (RS 4.10 with both components), `NaiveExtExt` (naive RS 4.8 in the
-- rendering of RS48Ext), and `satisfies-rel-funext` (RS 4.6). `RS411` is the
-- implication, by the paper's argument: centres give a total section, RS 4.10
-- strictifies the agreement, and a second application to the path family
-- strictifies its boundary, after which naive RS 4.8 concludes.
--
-- `HEP-holds` and `NaiveExtExt-holds` discharge both hypotheses from a full
-- 2LTT cofibration, and `rs46-recovered` closes the loop.
--------------------------------------------------------------------------------
module Extension.RS411 where
open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RelFunext using (satisfies-rel-funext)
open import Extension.RS48Ext using (naive-ext-ext)
private
variable
ℓ ℓΦ ℓΨ : Level
module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ} (cof : is-cofib i ℓ) where
------------------------------------------------------------------------------
-- Fibrant matches of extension types, and the path family between two match
-- elements with its canonical "refl on Φ" boundary. The term shapes are
-- copied verbatim from Extension.RS48Ext so that the instantiation below is
-- definitional.
------------------------------------------------------------------------------
ExtMatch : (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ))) → UU (ℓΦ ⊔ ℓΨ ⊔ ℓ)
ExtMatch Y a = fibrant-match (Ext-isFibrant cof Y a)
toMatch : (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
→ Ext i (λ ψ → C (Y ψ)) a → C (ExtMatch Y a)
toMatch Y a = pr1ᵉ (fibrant-witness (Ext-isFibrant cof Y a))
fromMatch : (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
→ C (ExtMatch Y a) → Ext i (λ ψ → C (Y ψ)) a
fromMatch Y a = pr1ᵉ (pr2ᵉ (fibrant-witness (Ext-isFibrant cof Y a)))
-- pointwise-identity family between (the extensions underlying) two match
-- elements
PathFam : (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
(f g : ExtMatch Y a) → Ψ → UU ℓ
PathFam Y a f g ψ =
Id (ic (ext-app (fromMatch Y a (c f)) ψ)) (ic (ext-app (fromMatch Y a (c g)) ψ))
-- the canonical rendering of "refl on Φ": the coercion of the strict
-- boundary of f, transported along the strict boundary of g (in the paper
-- both boundaries are judgmental and this is refl)
pathBdry : (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
(f g : ExtMatch Y a) (φ : Φ) → C (PathFam Y a f g (i φ))
pathBdry Y a f g φ =
exo-tr (λ v → C (Id (ic (ext-app (fromMatch Y a (c f)) (i φ))) (ic v)))
(exo-inv (ext-bdry (fromMatch Y a (c g)) φ))
(c (=ᵉ-to-Id {a = ic (ext-app (fromMatch Y a (c f)) (i φ))} {b = ic (a φ)}
(ext-bdry (fromMatch Y a (c f)) φ)))
------------------------------------------------------------------------------
-- The two hypotheses of RS 4.11, as predicates of the fixed i.
------------------------------------------------------------------------------
-- RS 4.10, the homotopy extension property (both components, as in the
-- paper's Lemma 3.14: a' : Extᵢ(A,a) and e' : Extᵢ(λψ. a'ψ = bψ, e)).
HEP : UUᵉ (lsuc ℓ ⊔ ℓΦ ⊔ ℓΨ)
HEP = (Y : Ψ → UU ℓ) (b : (ψ : Ψ) → C (Y ψ)) (a : (φ : Φ) → C (Y (i φ)))
(e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ))))
→ Σᵉ (Ext i (λ ψ → C (Y ψ)) a) (λ a' →
Ext i (λ ψ → C (Id (ic (ext-app a' ψ)) (ic (b ψ))))
(λ φ → exo-tr (λ v → C (Id (ic v) (ic (b (i φ)))))
(exo-inv (ext-bdry a' φ)) (c (e φ))))
-- naive RS 4.8 (Rzk NaiveExtExt): extensions that are pointwise equal,
-- with (the canonical rendering of) refl on Φ, are equal.
NaiveExtExt : UUᵉ (lsuc ℓ ⊔ ℓΦ ⊔ ℓΨ)
NaiveExtExt = (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
(f g : ExtMatch Y a)
→ ExtMatch (PathFam Y a f g) (pathBdry Y a f g)
→ Id f g
------------------------------------------------------------------------------
-- RS 4.11: the implication. The conclusion `satisfies-rel-funext cof` is
-- RS 4.6 / relative function extensionality for i (Extension.RelFunext).
------------------------------------------------------------------------------
RS411 : HEP → NaiveExtExt → satisfies-rel-funext cof
RS411 hep nee Y cY a = m₀ , contra
where
-- the centres assemble to a total section, agreeing weakly with a on Φ
b : (ψ : Ψ) → C (Y ψ)
b ψ = c (center (Y ψ) (cY ψ))
e : (φ : Φ) → Id (ic (a φ)) (ic (b (i φ)))
e φ = centrality (Y (i φ)) (cY (i φ)) (ic (a φ))
-- first application of 4.10: a strict extension a' of a, the centre
A' : Ext i (λ ψ → C (Y ψ)) a
A' = pr1ᵉ (hep Y b a e)
m₀ : ExtMatch Y a
m₀ = ic (toMatch Y a A')
contra : (x : ExtMatch Y a) → Id x m₀
contra x = nee Y a x m₀ h
where
-- the path family between x and the centre: pointwise contractible,
-- since paths in the contractible Y ψ are unique
Wfam : Ψ → UU ℓ
Wfam = PathFam Y a x m₀
cW : (ψ : Ψ) → is-contr (Wfam ψ)
cW ψ = is-prop-is-contr (Y ψ) (cY ψ)
(ic (ext-app (fromMatch Y a (c x)) ψ))
(ic (ext-app (fromMatch Y a (c m₀)) ψ))
bW : (ψ : Ψ) → C (Wfam ψ)
bW ψ = c (center (Wfam ψ) (cW ψ))
aW : (φ : Φ) → C (Wfam (i φ))
aW = pathBdry Y a x m₀
eW : (φ : Φ) → Id (ic (aW φ)) (ic (bW (i φ)))
eW φ = centrality (Wfam (i φ)) (cW (i φ)) (ic (aW φ))
-- second application of 4.10: strictify the boundary of the pointwise
-- paths to the canonical "refl" datum ...
E₂ : Ext i (λ ψ → C (Wfam ψ)) aW
E₂ = pr1ᵉ (hep Wfam bW aW eW)
h : ExtMatch Wfam aW
h = ic (toMatch Wfam aW E₂)
-- ... and conclude x = m₀ by the naive 4.8 (via nee above).
------------------------------------------------------------------------------
-- Bonus: once relative function extensionality for i is supplied, both
-- hypotheses hold, so RS 4.11 is a consistency check.
------------------------------------------------------------------------------
module _ (triv : satisfies-rel-funext cof) where
private
-- Fibre components of strictly equal pairs in a based-path family
-- agree over any strict identification of the base components (UIPᵉ).
pair-snd-lemma : {X : UU ℓ} {pt : X}
(u v : C (Σ X (λ y → Id y pt))) (E : u =ᵉ v)
(q : c (pr1 (ic u)) =ᵉ c (pr1 (ic v)))
→ c (pr2 (ic u))
=ᵉ exo-tr (λ z → C (Id (ic z) pt)) (exo-inv q) (c (pr2 (ic v)))
pair-snd-lemma u .u reflᵉ q = exo-inv (exo-ap-tr (UIPᵉ (exo-inv q) reflᵉ))
-- The full RS 4.10, from RS 4.6 (the proof of Extension.RS410, keeping
-- also the strict boundary of the extended homotopy).
HEP-holds : HEP
HEP-holds Y b a e = a' ,ᵉ e'
where
-- 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 ψ))
bdry : (φ : Φ) → C (Y' (i φ))
bdry φ = c (ic (a φ) , e φ)
fibW : isFibrant (Ext i (λ ψ → C (Y' ψ)) bdry)
fibW = Ext-isFibrant cof Y' bdry
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
a' : Ext i (λ ψ → C (Y ψ)) a
a' = (λ ψ → c (pr1 (ic (wsec ψ))))
,ᵉ exo-ap (λ t φ → c (pr1 (ic (t φ)))) (pr2ᵉ w)
e' : Ext i (λ ψ → C (Id (ic (ext-app a' ψ)) (ic (b ψ))))
(λ φ → exo-tr (λ v → C (Id (ic v) (ic (b (i φ)))))
(exo-inv (ext-bdry a' φ)) (c (e φ)))
e' = (λ ψ → c (pr2 (ic (wsec ψ))))
,ᵉ funextᵉ (λ φ → pair-snd-lemma (wsec (i φ)) (bdry φ)
(happlyᵉ (pr2ᵉ w) φ) (ext-bdry a' φ))
-- naive RS 4.8, from Extension.RS48Ext (definitional instantiation).
NaiveExtExt-holds : NaiveExtExt
NaiveExtExt-holds Y a f g h = naive-ext-ext cof triv Y a f g h
-- the consistency check: 4.10 + naive 4.8 recover 4.6
rs46-recovered : satisfies-rel-funext cof
rs46-recovered = RS411 HEP-holds NaiveExtExt-holds
{- 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
[Rzk] Nikolai Kudasov and others. Rzk proof assistant, since 2023.
https://github.com/rzk-lang/rzk
-}