{-# OPTIONS --without-K --exact-split --two-level #-}
--------------------------------------------------------------------------------
-- The path interval of Definition 5.6, and the internal axiom schemes
-- named in the Conclusions of the accompanying paper.
--
-- `PathInterval` is Definition 5.6:
--
-- (1) an interval: a shape I, not assumed fibrant, with two points given as
-- a map i∂ : ∂I → I out of the strict two-point type, required to be a
-- full 2LTT cofibration;
-- (2) a line-to-identity structure: for every fibrant Y an operation sending
-- a line g : I → Y to an inner path g 0 = g 1, natural in Y up to inner
-- equality.
--
-- The codomain of `path` is the identity type of the endpoints, so endpoint
-- compatibility is part of its type and needs no separate field; no comparison
-- in the other direction, and no invertibility, is assumed. Degeneracy on
-- constant lines is not assumed either: it is derived from naturality at
-- Y = ⊤ in `Extension.CoercionLaws`, which is the paper's derivation of
-- Lemma 5.8 (c3).
--
-- The theory-level statements of the Conclusions (Definition 6.2, Theorem 6.3)
-- are about theories rather than in them and are not formalized; see the note
-- in `index.agda`. What is formalized here are the three axiom schemes as
-- closed types, so that the internal content of the comparison becomes a pair
-- of implications between them (`Extension.TheoryComparison`):
--
-- (ua) ⇒ (glue) Theorem 5.4
-- (int) ∧ (glue) ⇒ (ua) via `PathInterval-to-PathStructure` and
-- `CoercionLaws.general-weak-glue-implies-ua`
--------------------------------------------------------------------------------
module Extension.Conservativity where
open import Extension.Prelude
open import Extension.Core
open import Extension.GlueUA
open import Extension.RelFunext using (is-cofib-2LTT)
open import Extension.CoercionLaws using (PathStructure)
open import Extension.Univalence using (Univalence)
open import Extension.GlueStructure using (has-strictly-coherent-glue)
private
variable
ℓI 𝓤 : Level
--------------------------------------------------------------------------------
-- The strict two-point boundary ∂I = 1 + 1, and the path interval.
--------------------------------------------------------------------------------
∂I : (ℓ : Level) → UUᵉ ℓ
∂I ℓ = ⊤ᵉ {ℓ} +ᵉ ⊤ᵉ {ℓ}
-- Definition 5.6: clause (1), an interval, is the shape I together with
-- the boundary inclusion i∂ : ∂I → I, required to be a full 2LTT cofibration;
-- clause (2), a line-to-identity structure, is `path` with its naturality.
-- ("For every fibrant Y" is the internal quantification over Y : UU 𝓤; the
-- test level of the cofibration clause is the same 𝓤.)
record PathInterval (ℓI 𝓤 : Level) : UUᵉ (lsuc (ℓI ⊔ 𝓤)) where
field
I : UUᵉ ℓI
i∂ : ∂I ℓI → I
-- endpoints
0I : I
0I = i∂ (inlᵉ starᵉ)
1I : I
1I = i∂ (inrᵉ starᵉ)
field
-- clause (1): the boundary inclusion is a full 2LTT cofibration (fibration
-- half + trivial-fibration half / relative funext)
i∂-cofib : is-cofib-2LTT i∂ 𝓤
-- clause (2): line-to-identity, with endpoint compatibility built into the
-- codomain, and naturality in Y up to inner equality
path : {Y : UU 𝓤} (g : I → C Y) → Id (ic (g 0I)) (ic (g 1I))
path-nat : {Y Z : UU 𝓤} (h : Y → Z) (g : I → C Y)
→ Id (ap h (path g)) (path (λ t → c (h (ic (g t)))))
open PathInterval public
--------------------------------------------------------------------------------
-- Clause (2) alone, without the boundary-cofibration clause: the exact
-- hypothesis of Theorem 5.14.
record PathPresentation (ℓI 𝓤 : Level) : UUᵉ (lsuc (ℓI ⊔ 𝓤)) where
field
shape : UUᵉ ℓI
point0 point1 : shape
line-path : {Y : UU 𝓤} (g : shape → C Y) → Id (ic (g point0)) (ic (g point1))
line-path-nat : {Y Z : UU 𝓤} (h : Y → Z) (g : shape → C Y) →
Id (ap h (line-path g))
(line-path (λ t → c (h (ic (g t)))))
path-interval-presentation : PathInterval ℓI 𝓤 → PathPresentation ℓI 𝓤
path-interval-presentation 𝕀 = record
{ shape = I 𝕀
; point0 = 0I 𝕀
; point1 = 1I 𝕀
; line-path = path 𝕀
; line-path-nat = path-nat 𝕀
}
-- The bridges (Lemma 5.8, input side): clause (2), at the level the
-- coercion laws need, is already the interface `CoercionLaws.PathStructure`,
-- which asks for nothing beyond `path` and its naturality. Degeneracy on
-- constant lines is derived there, not required here.
--
-- (The level bookkeeping: the coercion
-- laws instantiate the operation at Y = 𝓤, U→ and ⊤, one level above the small
-- types, so the bridges consume the structure at level `lsuc 𝓤`.)
--------------------------------------------------------------------------------
PathPresentation-to-PathStructure :
PathPresentation ℓI (lsuc 𝓤) → PathStructure ℓI 𝓤
PathPresentation-to-PathStructure P = record
{ I = PathPresentation.shape P
; 0I = PathPresentation.point0 P
; 1I = PathPresentation.point1 P
; path = PathPresentation.line-path P
; path-nat = PathPresentation.line-path-nat P
}
PathInterval-to-PathStructure : PathInterval ℓI (lsuc 𝓤) → PathStructure ℓI 𝓤
PathInterval-to-PathStructure 𝕀 = record
{ I = I 𝕀
; 0I = 0I 𝕀
; 1I = 1I 𝕀
; path = path 𝕀
; path-nat = path-nat 𝕀
}
--------------------------------------------------------------------------------
-- The three axiom schemes of the Conclusions, as closed types. Extending a
-- theory by an axiom is postulating a constant of that type, so the internal
-- content of the comparison is a pair of implications between these types.
--------------------------------------------------------------------------------
-- (int): there is a path interval at the given levels.
Axiom-int : (ℓI 𝓤 : Level) → UUᵉ (lsuc (ℓI ⊔ 𝓤))
Axiom-int = PathInterval
-- (ua): univalence is kept as an explicit hypothesis.
Axiom-ua : (𝓤 : Level) → UU (lsuc 𝓤)
Axiom-ua = Univalence
-- (glue): every full cofibration with cofibrant domain has a strictly
-- coherent Glue structure. Domain cofibrancy is included because it is a
-- premise of the scheme in the Conclusions, although Theorem 5.4 does not need it.
Axiom-glue : (ℓΦ ℓΨ 𝓤 : Level) →
UUᵉ (lsuc (ℓΦ ⊔ ℓΨ ⊔ lsuc 𝓤))
Axiom-glue ℓΦ ℓΨ 𝓤 =
(Φ : UUᵉ ℓΦ) (Ψ : UUᵉ ℓΨ) (i : Φ → Ψ) →
is-cofib-2LTT i (lsuc 𝓤) →
isCofibrant Φ (lsuc 𝓤) →
has-strictly-coherent-glue i 𝓤
--------------------------------------------------------------------------------
-- The flagship example (Introduction / Section 5.2): a cubical path is
-- an extension type. Given a path interval and a fibrant Y with two
-- endpoints, the type of maps I → Y restricting to those endpoints on ∂I is
-- the extension type along the boundary inclusion i∂ : ∂I ↪ I.
--------------------------------------------------------------------------------
module _ (𝕀 : PathInterval ℓI 𝓤) where
private
endpoints : (Y : UU 𝓤) → C Y → C Y → ∂I ℓI → C Y
endpoints Y y₀ y₁ (inlᵉ starᵉ) = y₀
endpoints Y y₀ y₁ (inrᵉ starᵉ) = y₁
-- Cubical path from y₀ to y₁ in Y = extension of the endpoint data along i∂.
CubicalPath : (Y : UU 𝓤) (y₀ y₁ : C Y) → UUᵉ (ℓI ⊔ 𝓤)
CubicalPath Y y₀ y₁ = Ext (i∂ 𝕀) (λ _ → C Y) (endpoints Y y₀ y₁)