{-# OPTIONS --without-K --exact-split --two-level #-}
--------------------------------------------------------------------------------
-- RS 4.2, currying and the pushout-product (Lemma 3.5).
--
-- For i : Φ → Ψ and i' : Φ' → Ψ', let P be the pushout of Φ ×ᵉ Ψ' and Ψ ×ᵉ Φ'
-- over Φ ×ᵉ Φ', assumed to exist in the outer level with a strict UMP
-- (Extension.ExoPushout), as the paper assumes it. The pushout-product
-- i □ i' : P → Ψ ×ᵉ Ψ' comes from the recursor, and for a partial section cᴾ
-- over P we prove the two strict isomorphisms
--
-- Extᵢ(λψ. Ext_{i'}(A(ψ,–), c(ψ,–)), c₁) ≅ Ext_{i□i'}(A, cᴾ)
-- ≅ Ext_{i'}(λψ'. Extᵢ(A(–,ψ'), …))
--
-- The components and curried boundaries are induced from cᴾ by the UMP. The
-- assumed β-rules are pointwise strict rather than judgmental, so the
-- components carry a transport along β, discharged by UIPᵉ.
--
-- As in Extension.RS this is proved for a general exo family and arbitrary exo
-- maps; the fibrant statement of the paper is the case A = C ∘ A₀.
--------------------------------------------------------------------------------
module Extension.RS42 where
open import Extension.Prelude
open import Extension.Core
open import Extension.ExoPushout
private
variable
ℓΦ ℓΨ ℓΦ' ℓΨ' ℓP ℓA : Level
--------------------------------------------------------------------------------
-- The span of the pushout-product.
--------------------------------------------------------------------------------
module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {Φ' : UUᵉ ℓΦ'} {Ψ' : UUᵉ ℓΨ'}
(i : Φ → Ψ) (i' : Φ' → Ψ') where
-- idᵉ ×ᵉ i' : Φ ×ᵉ Φ' → Φ ×ᵉ Ψ'
pp-left : Φ ×ᵉ Φ' → Φ ×ᵉ Ψ'
pp-left w = pr1ᵉ w ,ᵉ i' (pr2ᵉ w)
-- i ×ᵉ idᵉ : Φ ×ᵉ Φ' → Ψ ×ᵉ Φ'
pp-right : Φ ×ᵉ Φ' → Ψ ×ᵉ Φ'
pp-right w = i (pr1ᵉ w) ,ᵉ pr2ᵉ w
--------------------------------------------------------------------------------
-- The lemma, relative to an assumed outer pushout of the span.
--------------------------------------------------------------------------------
module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {Φ' : UUᵉ ℓΦ'} {Ψ' : UUᵉ ℓΨ'}
(i : Φ → Ψ) (i' : Φ' → Ψ')
{P : UUᵉ ℓP}
(inlᴾ : Φ ×ᵉ Ψ' → P) (inrᴾ : Ψ ×ᵉ Φ' → P)
(glueᴾ : (w : Φ ×ᵉ Φ') → inlᴾ (pp-left i i' w) =ᵉ inrᴾ (pp-right i i' w))
(po : {ℓE : Level} → is-exo-pushout (pp-left i i') (pp-right i i') inlᴾ inrᴾ glueᴾ ℓE)
where
-- The pushout-product map, induced by the (non-dependent) UMP. The cocone
-- condition holds definitionally: both legs send (φ, φ') to (i φ, i' φ').
i□i' : P → Ψ ×ᵉ Ψ'
i□i' = po-rec po (λ u → i (pr1ᵉ u) ,ᵉ pr2ᵉ u) (λ v → pr1ᵉ v ,ᵉ i' (pr2ᵉ v))
(λ w → reflᵉ)
-- Its strict β-rules (pointwise, as supplied by the interface).
□-βl : (u : Φ ×ᵉ Ψ') → i□i' (inlᴾ u) =ᵉ (i (pr1ᵉ u) ,ᵉ pr2ᵉ u)
□-βl = po-rec-βl po (λ u → i (pr1ᵉ u) ,ᵉ pr2ᵉ u) (λ v → pr1ᵉ v ,ᵉ i' (pr2ᵉ v))
(λ w → reflᵉ)
□-βr : (v : Ψ ×ᵉ Φ') → i□i' (inrᴾ v) =ᵉ (pr1ᵉ v ,ᵉ i' (pr2ᵉ v))
□-βr = po-rec-βr po (λ u → i (pr1ᵉ u) ,ᵉ pr2ᵉ u) (λ v → pr1ᵉ v ,ᵉ i' (pr2ᵉ v))
(λ w → reflᵉ)
module _ (A : Ψ ×ᵉ Ψ' → UUᵉ ℓA) (cᴾ : (p : P) → A (i□i' p)) where
----------------------------------------------------------------------------
-- The two components of the partial section cᴾ, and their strict agreement
-- on Φ ×ᵉ Φ' (the cocone condition), all induced by the UMP. The
-- transports along □-βl/□-βr replace the judgmental computation rules an
-- actual pushout would have.
----------------------------------------------------------------------------
-- c on Φ ×ᵉ Ψ' ("c is total in the second argument over Φ × Ψ'").
c₁₀ : (φ : Φ) (ψ' : Ψ') → A (i φ ,ᵉ ψ')
c₁₀ φ ψ' = exo-tr A (□-βl (φ ,ᵉ ψ')) (cᴾ (inlᴾ (φ ,ᵉ ψ')))
-- c on Ψ ×ᵉ Φ' (the boundary datum c(ψ,–) of the inner extension type).
c₀₁ : (ψ : Ψ) (φ' : Φ') → A (ψ ,ᵉ i' φ')
c₀₁ ψ φ' = exo-tr A (□-βr (ψ ,ᵉ φ')) (cᴾ (inrᴾ (ψ ,ᵉ φ')))
-- strict agreement of the two components over Φ ×ᵉ Φ' (pushout cocone
-- condition, transported along glueᴾ; UIPᵉ kills all coherence).
c-agree : (φ : Φ) (φ' : Φ') → c₁₀ φ (i' φ') =ᵉ c₀₁ (i φ) φ'
c-agree φ φ' =
tr-section-compat i□i' A cᴾ (glueᴾ (φ ,ᵉ φ'))
(□-βl (φ ,ᵉ i' φ')) (□-βr (i φ ,ᵉ φ'))
----------------------------------------------------------------------------
-- The two iterated extension types and their induced outer boundaries.
----------------------------------------------------------------------------
-- λψ. Ext_{i'}(A(ψ,–), c(ψ,–))
E₁ : Ψ → UUᵉ (ℓΦ' ⊔ ℓΨ' ⊔ ℓA)
E₁ ψ = Ext i' (λ ψ' → A (ψ ,ᵉ ψ')) (c₀₁ ψ)
-- c₁(φ) := (λψ'. c(φ,ψ') , boundary witness from the cocone condition)
c₁ : (φ : Φ) → E₁ (i φ)
c₁ φ = (λ ψ' → c₁₀ φ ψ') ,ᵉ funextᵉ (λ φ' → c-agree φ φ')
-- λψ'. Extᵢ(A(–,ψ'), c(–,ψ'))
E₂ : Ψ' → UUᵉ (ℓΦ ⊔ ℓΨ ⊔ ℓA)
E₂ ψ' = Ext i (λ ψ → A (ψ ,ᵉ ψ')) (λ φ → c₁₀ φ ψ')
-- c₂(φ') := (λψ. c(ψ,φ') , boundary witness), symmetrically.
c₂ : (φ' : Φ') → E₂ (i' φ')
c₂ φ' = (λ ψ → c₀₁ ψ φ') ,ᵉ funextᵉ (λ φ → exo-inv (c-agree φ φ'))
----------------------------------------------------------------------------
-- Boundary bookkeeping: a total section h : Πx.A x strictly restricts to
-- cᴾ along i□i' iff it strictly agrees with c₁₀ on Φ×Ψ' and with c₀₁ on
-- Ψ×Φ'. Forward: transport the pointwise boundary along the β-rules.
-- Backward: eliminate into the strict-equality family over P (the glue
-- coherence is free by UIPᵉ).
----------------------------------------------------------------------------
module _ (h : (x : Ψ ×ᵉ Ψ') → A x) (ph : restrict i□i' h =ᵉ cᴾ) where
restr-l : (φ : Φ) (ψ' : Ψ') → h (i φ ,ᵉ ψ') =ᵉ c₁₀ φ ψ'
restr-l φ ψ' = exo-concat (exo-inv (exo-apd h (□-βl (φ ,ᵉ ψ'))))
(exo-tr-elim (happlyᵉ ph (inlᴾ (φ ,ᵉ ψ'))))
restr-r : (ψ : Ψ) (φ' : Φ') → h (ψ ,ᵉ i' φ') =ᵉ c₀₁ ψ φ'
restr-r ψ φ' = exo-concat (exo-inv (exo-apd h (□-βr (ψ ,ᵉ φ'))))
(exo-tr-elim (happlyᵉ ph (inrᴾ (ψ ,ᵉ φ'))))
module _ (h : (x : Ψ ×ᵉ Ψ') → A x)
(bl : (φ : Φ) (ψ' : Ψ') → h (i φ ,ᵉ ψ') =ᵉ c₁₀ φ ψ')
(br : (ψ : Ψ) (φ' : Φ') → h (ψ ,ᵉ i' φ') =ᵉ c₀₁ ψ φ') where
glue-bdry : restrict i□i' h =ᵉ cᴾ
glue-bdry = funextᵉ (po-elim po (λ p → h (i□i' p) =ᵉ cᴾ p)
(λ u → exo-tr-inj A (□-βl u)
(exo-concat (exo-apd h (□-βl u)) (bl (pr1ᵉ u) (pr2ᵉ u))))
(λ v → exo-tr-inj A (□-βr v)
(exo-concat (exo-apd h (□-βr v)) (br (pr1ᵉ v) (pr2ᵉ v))))
(λ w → UIPᵉ _ _))
----------------------------------------------------------------------------
-- Lemma 3.5, first isomorphism:
-- Extᵢ(λψ. Ext_{i'}(A(ψ,–), c(ψ,–)), c₁) ≅ Ext_{i□i'}(A, cᴾ).
----------------------------------------------------------------------------
RS42a : Ext i E₁ c₁ ≅ Ext i□i' A cᴾ
RS42a = to ,ᵉ (from ,ᵉ (linv ,ᵉ rinv))
where
to : Ext i E₁ c₁ → Ext i□i' A cᴾ
to (g ,ᵉ pg) = h ,ᵉ glue-bdry h bl br
where
h : (x : Ψ ×ᵉ Ψ') → A x
h x = pr1ᵉ (g (pr1ᵉ x)) (pr2ᵉ x)
-- on Φ×Ψ': from the outer boundary g ∘ i =ᵉ c₁
bl : (φ : Φ) (ψ' : Ψ') → h (i φ ,ᵉ ψ') =ᵉ c₁₀ φ ψ'
bl φ ψ' = exo-ap (λ z → pr1ᵉ z ψ') (happlyᵉ pg φ)
-- on Ψ×Φ': from the inner boundaries of the g ψ
br : (ψ : Ψ) (φ' : Φ') → h (ψ ,ᵉ i' φ') =ᵉ c₀₁ ψ φ'
br ψ φ' = ext-bdry (g ψ) φ'
from : Ext i□i' A cᴾ → Ext i E₁ c₁
from (h ,ᵉ ph) =
(λ ψ → (λ ψ' → h (ψ ,ᵉ ψ')) ,ᵉ funextᵉ (λ φ' → restr-r h ph ψ φ'))
,ᵉ funextᵉ (λ φ → ext-≡ (funextᵉ (λ ψ' → restr-l h ph φ ψ')))
-- Round trips: the underlying sections agree by β/η for Πᵉ and Σᵉ; the
-- boundary witnesses are strict props (UIPᵉ), so ext-≡ closes both.
linv : (z : Ext i E₁ c₁) → from (to z) =ᵉ z
linv (g ,ᵉ pg) = ext-≡ (funextᵉ (λ ψ → ext-≡ reflᵉ))
rinv : (z : Ext i□i' A cᴾ) → to (from z) =ᵉ z
rinv (h ,ᵉ ph) = ext-≡ reflᵉ
----------------------------------------------------------------------------
-- Lemma 3.5, second isomorphism (the symmetric order of iteration):
-- Ext_{i□i'}(A, cᴾ) ≅ Ext_{i'}(λψ'. Extᵢ(A(–,ψ'), c(–,ψ')), c₂).
----------------------------------------------------------------------------
RS42b : Ext i□i' A cᴾ ≅ Ext i' E₂ c₂
RS42b = to ,ᵉ (from ,ᵉ (linv ,ᵉ rinv))
where
to : Ext i□i' A cᴾ → Ext i' E₂ c₂
to (h ,ᵉ ph) =
(λ ψ' → (λ ψ → h (ψ ,ᵉ ψ')) ,ᵉ funextᵉ (λ φ → restr-l h ph φ ψ'))
,ᵉ funextᵉ (λ φ' → ext-≡ (funextᵉ (λ ψ → restr-r h ph ψ φ')))
from : Ext i' E₂ c₂ → Ext i□i' A cᴾ
from (g ,ᵉ pg) = h ,ᵉ glue-bdry h bl br
where
h : (x : Ψ ×ᵉ Ψ') → A x
h x = pr1ᵉ (g (pr2ᵉ x)) (pr1ᵉ x)
bl : (φ : Φ) (ψ' : Ψ') → h (i φ ,ᵉ ψ') =ᵉ c₁₀ φ ψ'
bl φ ψ' = ext-bdry (g ψ') φ
br : (ψ : Ψ) (φ' : Φ') → h (ψ ,ᵉ i' φ') =ᵉ c₀₁ ψ φ'
br ψ φ' = exo-ap (λ z → pr1ᵉ z ψ) (happlyᵉ pg φ')
linv : (z : Ext i□i' A cᴾ) → from (to z) =ᵉ z
linv (h ,ᵉ ph) = ext-≡ reflᵉ
rinv : (z : Ext i' E₂ c₂) → to (from z) =ᵉ z
rinv (g ,ᵉ pg) = ext-≡ (funextᵉ (λ ψ' → ext-≡ reflᵉ))
-- The composite of the two, as displayed in Lemma 3.5.
RS42 : Ext i E₁ c₁ ≅ Ext i' E₂ c₂
RS42 = ≅-trans RS42a RS42b
{- 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
-}