{-# OPTIONS --safe #-}
module Cubical.HITs.Nullification.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.PathSplit
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv
open import Cubical.Modalities.Modality
open import Cubical.Functions.FunExtEquiv
open import Cubical.HITs.Localization renaming (rec to Localize-rec)
open import Cubical.Data.Unit
open import Cubical.HITs.Nullification.Base
open Modality
open isPathSplitEquiv
private
variable
ℓα ℓs ℓ ℓ' : Level
isNull≡ : {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} (nX : isNull S X) {x y : X} → isNull S (x ≡ y)
isNull≡ {A = A} {S = S} nX {x = x} {y = y} α =
fromIsEquiv (λ p _ i → p i)
(isEquiv[equivFunA≃B∘f]→isEquiv[f] (λ p _ → p) funExtEquiv (isEquivCong (const , toIsEquiv _ (nX α))))
isNullΠ : {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : X → Type ℓ'} → ((x : X) → isNull S (Y x)) →
isNull S ((x : X) → Y x)
isNullΠ {S = S} {X = X} {Y = Y} nY α = fromIsEquiv _ (snd e)
where
flipIso : Iso ((x : X) → S α → Y x) (S α → (x : X) → Y x)
Iso.fun flipIso f = flip f
Iso.inv flipIso f = flip f
Iso.rightInv flipIso f = refl
Iso.leftInv flipIso f = refl
e : ((x : X) → Y x) ≃ (S α → ((x : X) → Y x))
e =
((x : X) → Y x)
≃⟨ equivΠCod (λ x → const , (toIsEquiv _ (nY x α))) ⟩
((x : X) → (S α → Y x))
≃⟨ isoToEquiv flipIso ⟩
(S α → ((x : X) → Y x))
■
rec : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'}
→ (nB : isNull S Y) → (X → Y) → Null S X → Y
rec nB g ∣ x ∣ = g x
rec nB g (hub α f) = fst (sec (nB α)) (λ s → rec nB g (f s))
rec nB g (spoke α f s i) = snd (sec (nB α)) (λ s → rec nB g (f s)) i s
rec nB g (≡hub {x} {y} {α} p i) = fst (secCong (nB α) (rec nB g x) (rec nB g y)) (λ i s → rec nB g (p s i)) i
rec nB g (≡spoke {x} {y} {α} p s i j) = snd (secCong (nB α) (rec nB g x) (rec nB g y)) (λ i s → rec nB g (p s i)) i j s
toPathP⁻ : ∀ {ℓ} (A : I → Type ℓ) {x : A i0} {y : A i1} → x ≡ transport⁻ (λ i → A i) y → PathP A x y
toPathP⁻ A p i = toPathP {A = λ i → A (~ i)} (sym p) (~ i)
toPathP⁻-sq : ∀ {ℓ} {A : Type ℓ} (x : A) → Square (toPathP⁻ (λ _ → A) (λ _ → transport refl x)) refl
(transportRefl x) refl
toPathP⁻-sq x j i = hcomp (λ l → λ { (i = i0) → transportRefl x j
; (i = i1) → x ; (j = i1) → x })
(transportRefl x (i ∨ j))
module _ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Null S X → Type ℓ'} where
private
secCongDep' : ∀ (nY : (x : Null S X) → isNull S (Y x)) {x y : Null S X} {α} (p : x ≡ y)
→ (∀ (bx : Y x) (by : Y y) → hasSection (cong₂ (λ x (b : Y x) (_ : S α) → b) p))
secCongDep' nY {α = α} p = secCongDep (λ _ → const) p (λ a → secCong (nY a α))
elim : (nY : (x : Null S X) → isNull S (Y x)) → ((a : X) → Y ∣ a ∣) → (x : Null S X) → Y x
elim nY g ∣ x ∣ = g x
elim nY g (hub α f)
= fst (sec (nY (hub α f) α))
(λ s → transport (λ i → Y (spoke α f s (~ i))) (elim nY g (f s)))
elim nY g (spoke α f s i)
= toPathP⁻ (λ i → Y (spoke α f s i))
(funExt⁻ ( snd (sec (nY (hub α f) α))
(λ s → transport (λ i → Y (spoke α f s (~ i))) (elim nY g (f s))) ) s) i
elim nY g (≡hub {x} {y} p i)
= hcomp (λ k → λ { (i = i0) → transportRefl (elim nY g x) k
; (i = i1) → transportRefl (elim nY g y) k })
(fst (secCongDep' nY (≡hub p) (transport refl (elim nY g x)) (transport refl (elim nY g y)))
(λ i s → transport (λ j → Y (≡spoke p s (~ j) i)) (elim nY g (p s i))) i)
elim nY g (≡spoke {x} {y} p s j i)
= hcomp (λ k → λ { (i = i0) → toPathP⁻-sq (elim nY g x) k j
; (i = i1) → toPathP⁻-sq (elim nY g y) k j
; (j = i1) → elim nY g (p s i) })
(q₂ j i)
where q₁ : Path (PathP (λ i → Y (≡hub p i)) (transport refl (elim nY g x)) (transport refl (elim nY g y)))
(fst (secCongDep' nY (≡hub p) (transport refl (elim nY g x)) (transport refl (elim nY g y)))
(λ i s → transport (λ j → Y (≡spoke p s (~ j) i)) (elim nY g (p s i))))
(λ i → transport (λ j → Y (≡spoke p s (~ j) i)) (elim nY g (p s i)))
q₁ j i = snd (secCongDep' nY (≡hub p) (transport refl (elim nY g x)) (transport refl (elim nY g y)))
(λ i s → transport (λ j → Y (≡spoke p s (~ j) i)) (elim nY g (p s i))) j i s
q₂ : PathP (λ j → PathP (λ i → Y (≡spoke p s j i)) (toPathP⁻ (λ _ → Y x) (λ _ → transport refl (elim nY g x)) j)
(toPathP⁻ (λ _ → Y y) (λ _ → transport refl (elim nY g y)) j))
(fst (secCongDep' nY (≡hub p) (transport refl (elim nY g x)) (transport refl (elim nY g y)))
(λ i s → transport (λ j → Y (≡spoke p s (~ j) i)) (elim nY g (p s i))))
(λ i → elim nY g (p s i))
q₂ j i = toPathP⁻ (λ j → Y (≡spoke p s j i)) (λ j → q₁ j i) j
NullRecIsPathSplitEquiv : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'} → (isNull S Y) →
isPathSplitEquiv {A = (Null S X) → Y} (λ f → f ∘ ∣_∣)
sec (NullRecIsPathSplitEquiv nY) = rec nY , λ _ → refl
secCong (NullRecIsPathSplitEquiv nY) f f' = (λ p → funExt (elim (λ _ → isNull≡ nY) (funExt⁻ p))) , λ _ → refl
NullRecIsEquiv : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'} → (isNull S Y) →
isEquiv {A = (Null S X) → Y} (λ f → f ∘ ∣_∣)
NullRecIsEquiv nY = toIsEquiv _ (NullRecIsPathSplitEquiv nY)
NullRecEquiv : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'} → (isNull S Y) →
((Null S X) → Y) ≃ (X → Y)
NullRecEquiv nY = (λ f → f ∘ ∣_∣) , (NullRecIsEquiv nY)
NullPreservesProp : ∀ {ℓα ℓs ℓ} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} →
(isProp X) → isProp (Null S X)
NullPreservesProp {S = S} pX u = elim (λ v' → isNull≡ (isNull-Null S))
(λ y → elim (λ u' → isNull≡ (isNull-Null S) {x = u'}) (λ x → cong ∣_∣ (pX x y)) u)
NullModality : ∀ {ℓα ℓs ℓ} {A : Type ℓα} (S : A → Type ℓs) → Modality (ℓ-max ℓ (ℓ-max ℓα ℓs))
isModal (NullModality S) = isNull S
isPropIsModal (NullModality S) = isPropΠ (λ α → isPropIsPathSplitEquiv _)
◯ (NullModality S) = Null S
◯-isModal (NullModality S) = isNull-Null S
η (NullModality S) = ∣_∣
◯-elim (NullModality S) = elim
◯-elim-β (NullModality S) = λ _ _ _ → refl
◯-=-isModal (NullModality S) x y α = fromIsEquiv _ e
where e : isEquiv (λ (p : x ≡ y) → const {B = S α} p)
e = transport (λ i → isEquiv {B = funExtPath {A = S α} {f = const x} {g = const y} (~ i)}
(λ p → ua-gluePath funExtEquiv {x = const p} {y = cong const p} refl (~ i)))
(isEquivCong (_ , toIsEquiv _ (isNull-Null S α)))
idemNull : ∀ {ℓa ℓs ℓ} {A : Type ℓa} (S : A → Type ℓs) (X : Type (ℓ-max ℓ (ℓ-max ℓa ℓs))) → isNull S X → X ≃ Null S X
idemNull {ℓ = ℓ} S A nA = ∣_∣ , isModalToIsEquiv (NullModality {ℓ = ℓ} S) nA
module Null-iso-Localize {ℓα ℓs ℓ} {A : Type ℓα} (S : A → Type ℓs) (X : Type ℓ) where
to : Null S X → Localize {A = A} (λ α → const {B = S α} tt) X
to ∣ x ∣ = ∣ x ∣
to (hub α f) = ext α (to ∘ f) tt
to (spoke α f s i) = isExt α (to ∘ f) s i
to (≡hub {x} {y} {α} p i) = ≡ext α (const (to x)) (const (to y)) (cong to ∘ p) tt i
to (≡spoke {x} {y} {α} p s i j) = ≡isExt α (const (to x)) (const (to y)) (cong to ∘ p) s i j
from : Localize {A = A} (λ α → const {B = S α} tt) X → Null S X
from ∣ x ∣ = ∣ x ∣
from (ext α f tt) = hub α (from ∘ f)
from (isExt α f s i) = spoke α (from ∘ f) s i
from (≡ext α g h p tt i) = ≡hub {x = from (g tt)} {from (h tt)} (cong from ∘ p) i
from (≡isExt α g h p s i j) = ≡spoke {x = from (g tt)} {from (h tt)} (cong from ∘ p) s i j
to-from : ∀ (x : Localize {A = A} (λ α → const {B = S α} tt) X) → to (from x) ≡ x
to-from ∣ x ∣ k = ∣ x ∣
to-from (ext α f tt) k = ext α (λ s → to-from (f s) k) tt
to-from (isExt α f s i) k = isExt α (λ s → to-from (f s) k) s i
to-from (≡ext α g h p tt i) k = ≡ext α (λ _ → to-from (g tt) k) (λ _ → to-from (h tt) k) (λ s j → to-from (p s j) k) tt i
to-from (≡isExt α g h p s i j) k = ≡isExt α (λ _ → to-from (g tt) k) (λ _ → to-from (h tt) k) (λ s j → to-from (p s j) k) s i j
from-to : ∀ (x : Null S X) → from (to x) ≡ x
from-to ∣ x ∣ k = ∣ x ∣
from-to (hub α f) k = hub α (λ s → from-to (f s) k)
from-to (spoke α f s i) k = spoke α (λ s → from-to (f s) k) s i
from-to (≡hub {x} {y} p i) k = ≡hub {x = from-to x k} {from-to y k} (λ s j → from-to (p s j) k) i
from-to (≡spoke {x} {y} p s i j) k = ≡spoke {x = from-to x k} {from-to y k} (λ s j → from-to (p s j) k) s i j
isom : Iso (Null S X) (Localize {A = A} (λ α → const {B = S α} tt) X)
isom = iso to from to-from from-to
Null≃Localize : ∀ {ℓα ℓs ℓ} {A : Type ℓα} (S : A → Type ℓs) (X : Type ℓ) → Null S X ≃ Localize (λ α → const {B = S α} tt) X
Null≃Localize S X = isoToEquiv (Null-iso-Localize.isom S X)