{-# OPTIONS --without-K --exact-split --two-level #-}
--------------------------------------------------------------------------------
-- Definition 4.1: the seven displayed CCHM operations, on sections.
--
-- (1) formation `Glue` (5) boundary of glue `glue-bdry`
-- (2) type boundary `Glue-bdry` (6) η `glue-η`
-- (3) unglue `unglue`, `unglue-bdry`
-- (4) glue `glue` (7) β `glue-β`
--
-- `satisfies-literal-glue-rules i 𝓤` fixes the cofibration, `CCHMGlue 𝓤`
-- quantifies over full cofibrations at arbitrary levels. Like the paper's
-- displayed structure, this asserts no slice-wise reindexing coherence, so it
-- is weaker than a primitive contextual type former.
--
-- The paper suppresses the coercion along p : Glue ∘ i ≐ T. Since UU is not
-- an exotype we transport at the family level: `res-p` carries a restricted
-- section into T along p, and items (5) and (6) are stated with it. Item (7)
-- compares the underlying sections, which by UIPᵉ implies the realigned
-- equality of extension-type elements. The only proof obligation is
-- `unglue-comp-bdry`, that unglue ⊙ b carries the boundary witness item (4)
-- asks for.
--------------------------------------------------------------------------------
module Extension.GlueLiteralRules where
open import Extension.Prelude
open import Extension.Core using (Ext ; restrict)
open import Extension.RelFunext using (is-cofib-2LTT)
private
variable
ℓφ ℓΨ : Level
--------------------------------------------------------------------------------
-- The boundary of the composite unglue ⊙ b, derived from the generic strict
-- boundary of item (3). Proof by exo-J on the type boundary p (item (2)); at
-- p = reflᵉ both transports disappear and the statement is the pointwise
-- application of item (3)'s boundary to b(iφ).
--------------------------------------------------------------------------------
unglue-comp-bdry :
{Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {𝓤 : Level}
(A : Ψ → UU 𝓤) (G : Ψ → UU 𝓤) (T : Φ → UU 𝓤)
(f : (φ : Φ) → C (T φ ≃ A (i φ)))
(p : (λ φ → G (i φ)) =ᵉ T)
(ung : (ψ : Ψ) → G ψ → A ψ)
(ubd : (φ : Φ) → c (ung (i φ)) =ᵉ
exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
(λ ξ → c (pr1 (ic (f ξ)))) φ)
(b : (ψ : Ψ) → C (G ψ))
→ (λ φ → c (ung (i φ) (ic (b (i φ)))))
=ᵉ (λ φ → c (pr1 (ic (f φ))
(ic (exo-tr (λ H → (ξ : Φ) → C (H ξ)) p (λ ξ → b (i ξ)) φ))))
unglue-comp-bdry i A G .(λ φ → G (i φ)) f reflᵉ ung ubd b =
funextᵉ (λ φ →
exo-ap (λ (h : C (G (i φ) → A (i φ))) → c (ic h (ic (b (i φ))))) (ubd φ))
--------------------------------------------------------------------------------
-- Notation shared by the items (4)-(7) and by Lemma 4.2: for
-- fixed input (A, T, f) and items (1)-(3) data (G, p, ung, ubd) we get
-- * f∙ t: the composite boundary λφ. f_φ(t φ) (the paper's f·t);
-- * res-p b: b ∘ i regarded in Π_Φ T via p;
-- * GlueInputTm: the domain Σ(t : Π_Φ T). Ext_i(A, f∙ t) of glue;
-- * unglue⊙ b: the composite with its strict boundary witness, an
-- element of Ext_i(A, f∙ (res-p b));
-- * Θ: the restriction-unglue comparison map of Lemma 4.2.
--------------------------------------------------------------------------------
module GlueNotation
{Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
(A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
(G : Ψ → UU 𝓤) (p : (λ φ → G (i φ)) =ᵉ T)
(ung : (ψ : Ψ) → G ψ → A ψ)
(ubd : (φ : Φ) → c (ung (i φ)) =ᵉ
exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
(λ ξ → c (pr1 (ic (f ξ)))) φ)
where
-- f · t (pointwise application of the equivalence family to a section of T)
f∙ : ((φ : Φ) → C (T φ)) → ((φ : Φ) → C (A (i φ)))
f∙ t φ = c (pr1 (ic (f φ)) (ic (t φ)))
-- b ∘ i, regarded as an element of Π_Φ T via the type boundary p
res-p : ((ψ : Ψ) → C (G ψ)) → ((φ : Φ) → C (T φ))
res-p b = exo-tr (λ H → (ξ : Φ) → C (H ξ)) p (λ φ → b (i φ))
-- the input type of the glue constructor: a partial section t together with
-- a strict extension a of A along the boundary f∙ t
GlueInputTm : UUᵉ (ℓφ ⊔ ℓΨ ⊔ 𝓤)
GlueInputTm = Σᵉ ((φ : Φ) → C (T φ)) (λ t → Ext i (λ ψ → C (A ψ)) (f∙ t))
-- unglue ⊙ b with its strict boundary witness (item (3), "consequently")
unglue⊙ : (b : (ψ : Ψ) → C (G ψ)) → Ext i (λ ψ → C (A ψ)) (f∙ (res-p b))
unglue⊙ b = (λ ψ → c (ung ψ (ic (b ψ))))
,ᵉ unglue-comp-bdry i A G T f p ung ubd b
-- the restriction-unglue comparison map (Lemma 4.2)
Θ : ((ψ : Ψ) → C (G ψ)) → GlueInputTm
Θ b = res-p b ,ᵉ unglue⊙ b
-- Items (4)-(7), packaged over the fixed items (1)-(3) data: the
-- "constructor package" of Lemma 4.2. The field types are those of items
-- (4)-(7) of `literal-glue-rules` below (certified by the converters
-- `literal-package` / `literal-of-package`).
record ConstructorPackage : UUᵉ (ℓφ ⊔ ℓΨ ⊔ 𝓤) where
field
-- (4) glue
glue : (t : (φ : Φ) → C (T φ)) (a : Ext i (λ ψ → C (A ψ)) (f∙ t))
→ (ψ : Ψ) → C (G ψ)
-- (5) term boundary: glue(t,a) ∘ i ≐ t (via p)
glue-bdry : (t : (φ : Φ) → C (T φ)) (a : Ext i (λ ψ → C (A ψ)) (f∙ t))
→ res-p (glue t a) =ᵉ t
-- (6) η: b ≐ glue(b ∘ i, unglue ⊙ b)
glue-η : (b : (ψ : Ψ) → C (G ψ)) → b =ᵉ glue (res-p b) (unglue⊙ b)
-- (7) β: unglue ⊙ glue(t,a) ≐ a₀ (underlying sections)
glue-β : (t : (φ : Φ) → C (T φ)) (a : Ext i (λ ψ → C (A ψ)) (f∙ t))
→ pr1ᵉ (unglue⊙ (glue t a)) =ᵉ pr1ᵉ a
--------------------------------------------------------------------------------
-- Definition 4.1, items (1)-(7), for one input datum.
--------------------------------------------------------------------------------
record literal-glue-rules
{Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
(A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
: UUᵉ (ℓφ ⊔ ℓΨ ⊔ lsuc 𝓤) where
field
-- (1) formation
Glue : Ψ → UU 𝓤
-- (2) type boundary: Glue ∘ i ≐ T
Glue-bdry : (λ φ → Glue (i φ)) =ᵉ T
-- (3) unglue, generic (stated in the context extended by g : Glue ψ) ...
unglue : (ψ : Ψ) → Glue ψ → A ψ
-- ... with its strict boundary unglue_{iφ} ≐ f_φ (f_φ coerced along p,
-- at the family level as explained in the header)
unglue-bdry : (φ : Φ) → c (unglue (i φ)) =ᵉ
exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ)))
(exo-inv Glue-bdry)
(λ ξ → c (pr1 (ic (f ξ)))) φ
-- derived notation over the items (1)-(3) just declared
open GlueNotation i 𝓤 A T f Glue Glue-bdry unglue unglue-bdry public
field
-- (4) the glue term constructor
glue : (t : (φ : Φ) → C (T φ)) (a : Ext i (λ ψ → C (A ψ)) (f∙ t))
→ (ψ : Ψ) → C (Glue ψ)
-- (5) boundary of glue: glue(t,a) ∘ i ≐ t (via p)
glue-bdry : (t : (φ : Φ) → C (T φ)) (a : Ext i (λ ψ → C (A ψ)) (f∙ t))
→ res-p (glue t a) =ᵉ t
-- (6) η: b ≐ glue(b ∘ i, unglue ⊙ b)
glue-η : (b : (ψ : Ψ) → C (Glue ψ)) → b =ᵉ glue (res-p b) (unglue⊙ b)
-- (7) β: unglue ⊙ glue(t,a) ≐ a₀
glue-β : (t : (φ : Φ) → C (T φ)) (a : Ext i (λ ψ → C (A ψ)) (f∙ t))
→ pr1ᵉ (unglue⊙ (glue t a)) =ᵉ pr1ᵉ a
--------------------------------------------------------------------------------
-- "𝓤 has Glue" along i: the operations for every input datum (A, T, f).
--------------------------------------------------------------------------------
satisfies-literal-glue-rules :
{Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level)
→ UUᵉ (ℓφ ⊔ ℓΨ ⊔ lsuc 𝓤)
satisfies-literal-glue-rules {Φ = Φ} {Ψ = Ψ} i 𝓤 =
(A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
→ literal-glue-rules i 𝓤 A T f
-- The paper's universe-wide scheme, quantified over cofibrations at arbitrary
-- shape levels. It lives in SSetω because it quantifies over Level.
CCHMGlue : (𝓤 : Level) → SSetω
CCHMGlue 𝓤 =
{ℓΦ ℓΨ : Level} {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} →
(i : Φ → Ψ) → is-cofib-2LTT i (lsuc 𝓤) →
satisfies-literal-glue-rules i 𝓤
--------------------------------------------------------------------------------
-- Certifications.
--------------------------------------------------------------------------------
module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) {𝓤 : Level}
(A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
where
-- Items (4)-(7) of the record are a ConstructorPackage over its items
-- (1)-(3); the two directions below typecheck only because the field types
-- agree verbatim.
literal-package : (r : literal-glue-rules i 𝓤 A T f)
→ GlueNotation.ConstructorPackage i 𝓤 A T f
(literal-glue-rules.Glue r) (literal-glue-rules.Glue-bdry r)
(literal-glue-rules.unglue r) (literal-glue-rules.unglue-bdry r)
literal-package r = record
{ glue = literal-glue-rules.glue r
; glue-bdry = literal-glue-rules.glue-bdry r
; glue-η = literal-glue-rules.glue-η r
; glue-β = literal-glue-rules.glue-β r
}
literal-of-package :
(G : Ψ → UU 𝓤) (p : (λ φ → G (i φ)) =ᵉ T)
(ung : (ψ : Ψ) → G ψ → A ψ)
(ubd : (φ : Φ) → c (ung (i φ)) =ᵉ
exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
(λ ξ → c (pr1 (ic (f ξ)))) φ)
→ GlueNotation.ConstructorPackage i 𝓤 A T f G p ung ubd
→ literal-glue-rules i 𝓤 A T f
literal-of-package G p ung ubd pkg = record
{ Glue = G
; Glue-bdry = p
; unglue = ung
; unglue-bdry = ubd
; glue = Pkg.glue
; glue-bdry = Pkg.glue-bdry
; glue-η = Pkg.glue-η
; glue-β = Pkg.glue-β
}
where
module Pkg = GlueNotation.ConstructorPackage pkg
-- Items (1)-(3) of the literal rules, together with pointwise invertibility
-- of unglue, are the tuple of the existing
-- `GlueRules.satisfies-homotopy-glue-rules` (Remark 4.4): the
-- Σᵉ-tuple below typechecks against that definition unchanged.
literal-to-homotopy-rules-at : (r : literal-glue-rules i 𝓤 A T f)
→ ((ψ : Ψ) → C (isEquiv (literal-glue-rules.unglue r ψ)))
→ Σᵉ (Ψ → UU 𝓤) (λ Gl →
Σᵉ ((λ φ → Gl (i φ)) =ᵉ T) (λ p →
Σᵉ ((ψ : Ψ) → Gl ψ → A ψ) (λ ung →
Σᵉ ((φ : Φ) → c (ung (i φ))
=ᵉ exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
(λ ξ → c (pr1 (ic (f ξ)))) φ)
(λ _ → (ψ : Ψ) → C (isEquiv (ung ψ))))))
literal-to-homotopy-rules-at r inv =
literal-glue-rules.Glue r
,ᵉ (literal-glue-rules.Glue-bdry r
,ᵉ (literal-glue-rules.unglue r
,ᵉ (literal-glue-rules.unglue-bdry r
,ᵉ inv)))
{- References:
[CCHM] Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg.
Cubical type theory: a constructive interpretation of the univalence
axiom. TYPES 2015, LIPIcs 69, 5:1-5:34, 2018.
doi:10.4230/LIPIcs.TYPES.2015.5
-}