{-# OPTIONS --without-K --exact-split --two-level #-}
--------------------------------------------------------------------------------
-- Closure properties of 2LTT cofibrations.
--
-- * `fib-comp-iso`: the strict fibre of a composite splits as a Σᵉ of
-- strict fibres, by strict singleton contraction;
-- * `∘-is-cofib`, `∘-satisfies-rel-funext`, `∘-is-cofib-2LTT`: both halves,
-- and the full cofibration, are closed under composition;
-- * `isCofibrant→initial-cofib` and back: `isCofibrant B ℓ` says that
-- ⊥ᵉ → B is a full 2LTT cofibration;
-- * `cofib-codomain-cofibrant`: if i : A → B is a full cofibration and A is
-- cofibrant then so is B, since ∅ → B is (∅ → A) followed by i. This is
-- the step Lemma 2.3 needs.
--
-- `∘-is-cofib` takes the two outer types at a common level, which is what
-- makes the fibrant match of the composite fibre and the Σᵉ-decomposition
-- agree without cumulativity.
--------------------------------------------------------------------------------
module Extension.CofibClosure where
open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RelFunext
open import Extension.SigmaTruncation using (Σ-contr)
open import Extension.Glue using (fibᵉ)
private
variable
ℓ ℓX ℓY ℓZ : Level
--------------------------------------------------------------------------------
-- §1 The strict fibre of a composite map.
--------------------------------------------------------------------------------
module _ {X : UUᵉ ℓX} {Y : UUᵉ ℓY} {Z : UUᵉ ℓZ}
(g : X → Y) (f : Y → Z) (z : Z) where
private
-- composition of the two strict fibre witnesses, computing on reflᵉ in the
-- First argument (so that both round trips below are definitional)
glue-eq : {x : X} {y : Y} → g x =ᵉ y → f y =ᵉ z → f (g x) =ᵉ z
glue-eq reflᵉ q = q
-- Fib_{f∘g}(z) ≅ Σᵉ (w : Fib_f(z)). Fib_g(pr1ᵉ w), by strict singleton
-- contraction (pattern matching on reflᵉ).
fib-comp-iso : fibᵉ (λ x → f (g x)) z ≅ Σᵉ (fibᵉ f z) (λ w → fibᵉ g (pr1ᵉ w))
fib-comp-iso = to ,ᵉ (from ,ᵉ (ft ,ᵉ tf))
where
to : fibᵉ (λ x → f (g x)) z → Σᵉ (fibᵉ f z) (λ w → fibᵉ g (pr1ᵉ w))
to (x ,ᵉ p) = (g x ,ᵉ p) ,ᵉ (x ,ᵉ reflᵉ)
from : Σᵉ (fibᵉ f z) (λ w → fibᵉ g (pr1ᵉ w)) → fibᵉ (λ x → f (g x)) z
from ((y ,ᵉ p) ,ᵉ (x ,ᵉ q)) = x ,ᵉ glue-eq q p
ft : (w : fibᵉ (λ x → f (g x)) z) → from (to w) =ᵉ w
ft (x ,ᵉ p) = reflᵉ
tf : (w : Σᵉ (fibᵉ f z) (λ w → fibᵉ g (pr1ᵉ w))) → to (from w) =ᵉ w
tf ((.(g x) ,ᵉ p) ,ᵉ (x ,ᵉ reflᵉ)) = reflᵉ
--------------------------------------------------------------------------------
-- §2 Composition of cofibrations.
--
-- For i : Φ → Ψ and j : Ψ → Θ we have, definitionally,
-- restrict (j ∘ i) h = restrict i (restrict j h),
-- so restriction along j ∘ i is the composite of the two restriction maps and
-- its strict fibres decompose by `fib-comp-iso`:
-- Fib_{(j∘i)*}(a) ≅ Σᵉ (w : Fib_{i*}(a)). Fib_{j*}(pr1ᵉ w).
-- Both pieces are fibrant (the fibres of i* are extension types along i in
-- the restricted family Y ∘ j; the fibres of j* are extension types along j
-- in Y), so the composite fibre is fibrant by isFibrant-Σ.
--------------------------------------------------------------------------------
module _ {ℓΦ ℓS ℓ : Level} {Φ : UUᵉ ℓΦ} {Ψ Θ : UUᵉ ℓS}
{i : Φ → Ψ} {j : Ψ → Θ} where
∘-is-cofib : is-cofib i ℓ → is-cofib j ℓ → is-cofib (λ x → j (i x)) ℓ
∘-is-cofib cofI cofJ Y a =
isFibrant-iso
(≅-sym (fib-comp-iso (i* j Y) (i* i (λ ψ → Y (j ψ))) a))
(isFibrant-Σ (cofI (λ ψ → Y (j ψ)) a) (λ w → cofJ Y (pr1ᵉ w)))
-- The trivial-fibration half: the fibrant match of the composite fibre is,
-- by construction, the inner Σ of the match of the i*-fibre (an extension
-- type along i) and the matches of the j*-fibres (extension types along j);
-- both are contractible by the two relative-funext hypotheses, so the Σ is
-- contractible.
∘-satisfies-rel-funext :
(cofI : is-cofib i ℓ) (cofJ : is-cofib j ℓ)
→ satisfies-rel-funext cofI → satisfies-rel-funext cofJ
→ satisfies-rel-funext (∘-is-cofib cofI cofJ)
∘-satisfies-rel-funext cofI cofJ rfI rfJ Y cY a =
Σ-contr (rfI (λ ψ → Y (j ψ)) (λ ψ → cY (j ψ)) a)
(λ x → rfJ Y cY (pr1ᵉ (gI (c x))))
where
-- the from-map of the fibrancy witness of the i*-fibre, as used in the
-- match description produced by isFibrant-Σ
gI : C (fibrant-match (cofI (λ ψ → Y (j ψ)) a))
→ fibᵉ (i* i (λ ψ → Y (j ψ))) a
gI = pr1ᵉ (pr2ᵉ (fibrant-witness (cofI (λ ψ → Y (j ψ)) a)))
-- Full 2LTT cofibrations compose.
∘-is-cofib-2LTT : is-cofib-2LTT i ℓ → is-cofib-2LTT j ℓ
→ is-cofib-2LTT (λ x → j (i x)) ℓ
∘-is-cofib-2LTT (cofI ,ᵉ rfI) (cofJ ,ᵉ rfJ) =
∘-is-cofib cofI cofJ ,ᵉ ∘-satisfies-rel-funext cofI cofJ rfI rfJ
--------------------------------------------------------------------------------
-- §3 The bridge: `isCofibrant B` = "⊥ᵉ → B is a full 2LTT cofibration".
--
-- The strict fibre of restriction along any z : ⊥ᵉ → B over any boundary is
-- the full section space Πᵉ B (C ∘ Y): boundary data over ⊥ᵉ carry no
-- information (the boundary component is a strict proposition, inhabited via
-- funextᵉ and ⊥ᵉ-elimination). So the fibration half of "z is a cofibration"
-- is the Π-fibrancy field of `isCofibrant`, and the trivial half is its
-- contractibility-preservation field.
--------------------------------------------------------------------------------
module _ {ℓB ℓ : Level} {B : UUᵉ ℓB} (z : ⊥ᵉ → B) where
private
empty-res-fib-iso : (Y : B → UU ℓ) (a : (φ : ⊥ᵉ) → C (Y (z φ)))
→ Πᵉ B (λ b → C (Y b)) ≅ fibᵉ (i* z Y) a
empty-res-fib-iso Y a = to ,ᵉ (from ,ᵉ (ft ,ᵉ tf))
where
to : Πᵉ B (λ b → C (Y b)) → fibᵉ (i* z Y) a
to h = h ,ᵉ funextᵉ (λ φ → ex-falsoᵉ φ)
from : fibᵉ (i* z Y) a → Πᵉ B (λ b → C (Y b))
from w = pr1ᵉ w
ft : (h : Πᵉ B (λ b → C (Y b))) → from (to h) =ᵉ h
ft h = reflᵉ
tf : (w : fibᵉ (i* z Y) a) → to (from w) =ᵉ w
tf (h ,ᵉ p) = dep-pair-=ᵉ _ _ (reflᵉ ,ᵉ UIPᵉ _ _)
-- the fibration half ...
initial-is-cofib : isCofibrant B ℓ → is-cofib z ℓ
initial-is-cofib cofB Y a =
isFibrant-iso (empty-res-fib-iso Y a) (Π-fibrant-witness (cofB Y))
-- ... and the full cofibration: the trivial half is the
-- contractibility-preservation field of `isCofibrant` (the fibrant match of
-- the fibre is the match of the section space, definitionally).
isCofibrant→initial-cofib : isCofibrant B ℓ → is-cofib-2LTT z ℓ
isCofibrant→initial-cofib cofB =
initial-is-cofib cofB ,ᵉ
(λ Y cY a → contr-preserve-witness (cofB Y) cY)
-- Conversely, a full cofibration ⊥ᵉ → B makes B cofibrant: the fibration
-- half gives Π-fibrancy (over the empty boundary), the trivial half gives
-- preservation of contractibility.
initial-cofib→isCofibrant : is-cofib-2LTT z ℓ → isCofibrant B ℓ
initial-cofib→isCofibrant (cof∅ ,ᵉ rf∅) Y =
iscofibrant-at
(isFibrant-iso (≅-sym (empty-res-fib-iso Y a₀)) (cof∅ Y a₀))
(λ cY → rf∅ Y cY a₀)
where
a₀ : (φ : ⊥ᵉ) → C (Y (z φ))
a₀ φ = ex-falsoᵉ φ
--------------------------------------------------------------------------------
-- §4 The closure lemma (paper: proof of Lemma 2.3, "Since B is
-- the codomain of the cofibration i : A ↪ B from cofibrant A, B is
-- cofibrant"). Assembled by the composition route:
--
-- A cofibrant ⇒ ⊥ᵉ → A is a full cofibration (bridge)
-- ⇒ ⊥ᵉ → A → B is a full cofibration (composition)
-- ⇒ B cofibrant (bridge back).
--
-- The bridge is stated for an arbitrary map out of ⊥ᵉ, so the composite
-- λ x → i (ex-falsoᵉ x) needs no realignment to ex-falsoᵉ.
--------------------------------------------------------------------------------
cofib-codomain-cofibrant : {ℓS ℓ : Level} {A B : UUᵉ ℓS} {i : A → B}
→ is-cofib-2LTT i ℓ → isCofibrant A ℓ
→ isCofibrant B ℓ
cofib-codomain-cofibrant {i = i} c2 cofA =
initial-cofib→isCofibrant (λ x → i (ex-falsoᵉ x))
(∘-is-cofib-2LTT (isCofibrant→initial-cofib ex-falsoᵉ cofA) c2)