Derivative.Basics.W
{-# OPTIONS -WnoUnsupportedIndexedMatch --safe #-}
module Derivative.Basics.W where
open import Derivative.Prelude
open import Derivative.Basics.Decidable
open import Derivative.Basics.Embedding
open import Derivative.Basics.Sigma
open import Derivative.Basics.Sum
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Equiv.Dependent
open import Cubical.Foundations.Path
open import Cubical.Data.Nat.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Relation.Nullary.Properties using (EquivPresDiscrete)
open import Cubical.Functions.Embedding
private
variable
ℓS ℓP ℓQ : Level
private
module impl (S : Type ℓS) (P : S → Type ℓP) where
data W : Type (ℓ-max ℓS ℓP) where
sup : (s : S) (f : P s → W) → W
module implᴰ (S : Type ℓS) (P : S → Type ℓP) (Q : S → Type ℓQ) where
open impl S P
data Wᴰ : W → Type (ℓ-max ℓQ (ℓ-of W)) where
top : {s : S} {f : P s → W} → (q : Q s) → Wᴰ (sup s f)
below : {s : S} {f : P s → W} → (p : P s) → (wᴰ : Wᴰ (f p)) → Wᴰ (sup s f)
module _ {S : Type ℓS} {P : S → Type ℓP} where
open impl S P
W-elim : ∀ {ℓ} {B : W → Type ℓ}
→ (sup* : (s : S) (f : P s → W) → (sup* : (p : P s) → B (f p)) → B (sup s f))
→ (w : W) → B w
W-elim {B} sup* (sup s f) = sup* s f λ p → W-elim {B = B} sup* (f p)
W-elim2 : ∀ {ℓ} {B : W → W → Type ℓ}
→ (sup* : (s₀ s₁ : S) (f₀ : P s₀ → W) (f₁ : P s₁ → W)
→ (sup* : (p₀ : P s₀) → (p₁ : P s₁) → B (f₀ p₀) (f₁ p₁))
→ B (sup s₀ f₀) (sup s₁ f₁)
)
→ (w₀ w₁ : W) → B w₀ w₁
W-elim2 {B} sup* (sup s₀ f₀) (sup s₁ f₁) = sup* s₀ s₁ f₀ f₁ λ p₀ p₁ → W-elim2 {B = B} sup* (f₀ p₀) (f₁ p₁)
W-out : W → (Σ[ s ∈ S ] (P s → W))
W-out (sup s f) = s , f
W-shape : W → S
W-shape = fst ∘ W-out
W-branch : (w : W) → P (W-shape w) → W
W-branch = snd ∘ W-out
W-in : (Σ[ s ∈ S ] (P s → W)) → W
W-in = uncurry sup
W-in-equiv : (Σ[ s ∈ S ] (P s → W)) ≃ W
W-in-equiv = isoToEquiv iso module W-in-equiv where
iso : Iso (Σ[ s ∈ S ] (P s → W)) W
iso .Iso.fun = W-in
iso .Iso.inv = W-out
iso .Iso.rightInv (sup s f) = refl
iso .Iso.leftInv _ = refl
W-rec : ∀ {ℓ} {A : Type ℓ}
→ (sup* : (Σ[ s ∈ S ] (P s → A)) → A)
→ W → A
W-rec {A} sup* (sup s f) = sup* (s , λ p → W-rec sup* (f p))
W-rec-β : ∀ {ℓ} {A : Type ℓ}
→ (sup* : (Σ[ s ∈ S ] (P s → A)) → A)
→ W-rec sup* ≡ W-out ⨟ Σ-map-snd (λ _ → W-rec sup* ∘_) ⨟ sup*
W-rec-β sup* = funExt λ { (sup _ _ ) → refl }
W-out-equiv : W ≃ (Σ[ s ∈ S ] (P s → W))
W-out-equiv = isoToEquiv (invIso W-in-equiv.iso)
W-out-unique : ∀ {ℓ} {A : Type ℓ} (f : (Σ[ s ∈ S ] (P s → A)) → A) → ∃![ f* ∈ (W → A) ] f* ≡ W-out ⨟ Σ-map-snd (λ s → f* ∘_) ⨟ f
W-out-unique f .fst = W-rec f , W-rec-β f
W-out-unique f .snd (f* , comm*) = ΣPathP (goal , goal-coh) module W-out-unique where
goal-ext : ∀ w → W-rec f w ≡ f* w
goal-ext (sup s x) = p ∙ q
module goal-ext where
p = cong (λ - → f (s , - )) (funExt (goal-ext ∘ x))
q = sym (comm* ≡$ sup s x)
filler = compPath-filler p q
goal : W-rec f ≡ f*
goal = funExt goal-ext
goal-coh-ext : ∀ w → PathP (λ i → goal i w ≡ (W-out ⨟ Σ-map-snd (λ _ → (goal i) ∘_) ⨟ f) w) (W-rec-β f ≡$ w) (comm* ≡$ w)
goal-coh-ext (sup s x) i j = goal-ext.filler s x (~ j) i
goal-coh : PathP (λ i → goal i ≡ W-out ⨟ Σ-map-snd (λ _ → (goal i) ∘_) ⨟ f) (W-rec-β f) comm*
goal-coh i j x = goal-coh-ext x i j
module _ {S : Type ℓS} {P : S → Type ℓP} where
open impl
WPath : (x y : W S P) → Type (ℓ-max ℓS ℓP)
WPath (sup s₀ f₀) (sup s₁ f₁) = Σ (s₀ ≡ s₁) λ p → PathP (λ i → P (p i) → W S P) f₀ f₁
≡→WPath : (x y : W S P) → x ≡ y → WPath x y
≡→WPath (sup s₀ f₀) (sup s₁ f₁) x≡y .fst = cong W-shape x≡y
≡→WPath (sup s₀ f₀) (sup s₁ f₁) x≡y .snd = cong W-branch x≡y
WPath→≡ : (x y : W S P) → WPath x y → x ≡ y
WPath→≡ (sup s₀ f₀) (sup s₁ f₁) (s₀≡s₁ , f₀≡f₁) = cong₂ sup s₀≡s₁ f₀≡f₁
WPath-linv-refl : (x : W S P) → WPath→≡ x x (≡→WPath x x refl) ≡ refl
WPath-linv-refl (sup s f) = refl
WPath-linv : (x y : W S P) (p : x ≡ y) → WPath→≡ _ _ (≡→WPath _ _ p) ≡ p
WPath-linv x y = J (λ y p → WPath→≡ _ _ (≡→WPath _ _ p) ≡ p) $ WPath-linv-refl x
WPath-rinv : (x y : W S P) (p : WPath x y) → ≡→WPath _ _ (WPath→≡ _ _ p) ≡ p
WPath-rinv (sup s₀ f₀) (sup s₁ f₁) _ = refl
WPathIso : (x y : W S P) → Iso (x ≡ y) (WPath x y)
WPathIso x y .Iso.fun = ≡→WPath _ _
WPathIso x y .Iso.inv = WPath→≡ _ _
WPathIso x y .Iso.rightInv = WPath-rinv _ _
WPathIso x y .Iso.leftInv = WPath-linv _ _
WPath-≃ : (x y : W S P) → (x ≡ y) ≃ (WPath x y)
WPath-≃ x y = isoToEquiv $ WPathIso x y
isOfHLevelSucW :
∀ (n : HLevel)
→ isOfHLevel (1 + n) S
→ isOfHLevel (1 + n) (W S P)
isOfHLevelSucW zero trunc-S = W-elim2 λ s₀ s₁ f₀ f₁ hyp → cong₂ sup (trunc-S s₀ s₁) (funExtNonDep λ {p₀} {p₁} _ → hyp p₀ p₁)
isOfHLevelSucW n@(suc _) trunc-S = W-elim2 goal where
goal : (s₀ s₁ : S) (f₀ : P s₀ → W S P) (f₁ : P s₁ → W S P)
→ (∀ p₀ p₁ → isOfHLevel n (f₀ p₀ ≡ f₁ p₁))
→ isOfHLevel n (sup s₀ f₀ ≡ sup s₁ f₁)
goal s₀ s₁ f₀ f₁ hyp = isOfHLevelRespectEquiv n (invEquiv $ WPath-≃ _ _)
$ isOfHLevelΣ n (trunc-S s₀ s₁) λ s₀≡s₁ → lemma s₀ s₁ s₀≡s₁ f₀ f₁ hyp
where
Motive : (s₀ s₁ : S) → s₀ ≡ s₁ → Type _
Motive s₀ s₁ s₀≡s₁ =
∀ (f₀ : P s₀ → W S P)
→ (f₁ : P s₁ → W S P)
→ (∀ p₀ p₁ → isOfHLevel n (f₀ p₀ ≡ f₁ p₁))
→ isOfHLevel n (PathP (λ i → P (s₀≡s₁ i) → W S P) f₀ f₁)
motive-refl : ∀ s₀
→ (f₀ f₁ : P s₀ → W S P)
→ ((p₀ p₁ : P s₀) → isOfHLevel n (f₀ p₀ ≡ f₁ p₁))
→ isOfHLevel n (f₀ ≡ f₁)
motive-refl s₀ f₀ f₁ hyp = isOfHLevelRespectEquiv n funExtEquiv $ isOfHLevelΠ n
λ (p : P s₀) → hyp p p
lemma : ∀ (s₀ s₁ : S) → (s₀≡s₁ : s₀ ≡ s₁) → Motive s₀ s₁ s₀≡s₁
lemma s₀ s₁ = J (Motive s₀) (motive-refl s₀)
isPropW : isProp S → isProp (W S P)
isPropW = isOfHLevelSucW 0
isSetW : isSet S → isSet (W S P)
isSetW = isOfHLevelSucW 1
module _ (S : Type ℓS) (P : S → Type ℓP) (Q : S → Type ℓQ) where
open impl S P
open implᴰ S P Q
module _ (s : S) (f : P s → W) where
Wᴰ-out : Wᴰ (sup s f) → Q s ⊎ (Σ[ p ∈ P s ] (Wᴰ (f p)))
Wᴰ-out (top q) = inl q
Wᴰ-out (below p wᴰ) = inr (p , wᴰ)
Wᴰ-in : Q s ⊎ (Σ[ p ∈ P s ] (Wᴰ (f p))) → Wᴰ (sup s f)
Wᴰ-in (inl q) = top q
Wᴰ-in (inr (p , wᴰ)) = below p wᴰ
Wᴰ-out-equiv : Wᴰ (sup s f) ≃ Q s ⊎ (Σ[ p ∈ P s ] (Wᴰ (f p)))
Wᴰ-out-equiv = isoToEquiv iso module Wᴰ-out-equiv where
iso : Iso _ _
iso .Iso.fun = Wᴰ-out
iso .Iso.inv = Wᴰ-in
iso .Iso.rightInv (inl _) = refl
iso .Iso.rightInv (inr _) = refl
iso .Iso.leftInv (top _) = refl
iso .Iso.leftInv (below _ _) = refl
Wᴰ-in-equiv : Q s ⊎ (Σ[ p ∈ P s ] (Wᴰ (f p))) ≃ Wᴰ (sup s f)
Wᴰ-in-equiv = isoToEquiv (invIso Wᴰ-out-equiv.iso)
isEquiv-Wᴰ-in : isEquiv Wᴰ-in
isEquiv-Wᴰ-in = equivIsEquiv Wᴰ-in-equiv
module _ (disc-P : ∀ s → Discrete (P s)) (disc-Q : ∀ s → Discrete (Q s)) where
discrete-Wᴰ : ∀ w → Discrete (Wᴰ w)
discrete-Wᴰ (sup s f) = EquivPresDiscrete (Wᴰ-in-equiv s f) $
discrete⊎
(disc-Q s)
(discreteΣ (disc-P s) (discrete-Wᴰ ∘ f))
Wᴰ-Path : ∀ {w₀ w₁} (h : WPath w₀ w₁) → (x : Wᴰ w₀) → (y : Wᴰ w₁) → Type (ℓ-max ℓS (ℓ-max ℓP ℓQ))
Wᴰ-Path (s₀≡s₁ , f₀≡f₁) (top q₀) (top q₁) = Lift {j = ℓ-max ℓS ℓP} $ PathP (λ i → Q (s₀≡s₁ i)) q₀ q₁
Wᴰ-Path (s₀≡s₁ , f₀≡f₁) (top q₀) (below p₁ y) = 𝟘*
Wᴰ-Path (s₀≡s₁ , f₀≡f₁) (below p₀ x) (top q₁) = 𝟘*
Wᴰ-Path (s₀≡s₁ , f₀≡f₁) (below p₀ x) (below p₁ y)
= Σ[ p₀≡p₁ ∈ PathP (λ i → P (s₀≡s₁ i)) p₀ p₁ ] PathP (λ i → Wᴰ (f₀≡f₁ i (p₀≡p₁ i))) x y
Wᴰ-Path→≡ : ∀ {w₀ w₁} {p : WPath w₀ w₁} {x : Wᴰ w₀} {y : Wᴰ w₁} → Wᴰ-Path p x y → PathP (λ i → Wᴰ (WPath→≡ _ _ p i)) x y
Wᴰ-Path→≡ {x = top q₀} {y = top q₁} (lift q) i = top (q i)
Wᴰ-Path→≡ {x = below p₀ x} {y = below p₁ y} (p₀≡p₁ , x≡y) i = below (p₀≡p₁ i) (x≡y i)
open impl public using (W ; sup)
open implᴰ public using (Wᴰ ; top ; below)
W-map : ∀ {S S′ : Type ℓS} {P : S → Type ℓP} {P′ : S′ → Type ℓP}
→ (f : S → S′)
→ (fᴰ : ∀ s → P′ (f s) → P s)
→ W S P → W S′ P′
W-map f fᴰ = W-elim λ s x map → sup (f s) (map ∘ fᴰ s)
W-fiber-equiv : ∀ {ℓ} {S : Type ℓS} {P : S → Type ℓP} {Y : Type ℓ}
→ {f : W S P → Y}
→ (y : Y) → fiber f y ≃ (Σ[ s ∈ S ] fiber (f ∘ sup s) y)
W-fiber-equiv {S} {P} {Y} {f} y =
Σ[ x ∈ W S P ] f x ≡ y
≃⟨ invEquiv $ Σ-cong-equiv-fst W-in-equiv ⟩
Σ[ (s , x) ∈ Σ[ s ∈ S ] (P s → W S P) ] f (sup s x) ≡ y
≃⟨ Σ-assoc-≃ ⟩
Σ[ s ∈ S ] Σ[ x ∈ (P s → W S P) ] f (sup s x) ≡ y
≃∎
isEmbedding→W-rec-fiber-equiv : ∀ {ℓ} {S : Type ℓS} {P : S → Type ℓP} {A : Type ℓ}
→ (sup* : (Σ[ s ∈ S ] (P s → A)) → A)
→ isEmbedding sup*
→ (s : S) (f : P s → W S P)
→ fiber (W-rec sup*) (W-rec sup* (sup s f)) ≃ ((p : P s) → fiber (W-rec sup*) (W-rec sup* (f p)))
isEmbedding→W-rec-fiber-equiv {S} {P} {A} sup* is-emb-sup* s f =
Σ[ x ∈ W S P ] W-rec sup* x ≡ sup* (s , W-rec sup* ∘ f)
≃⟨ invEquiv $ Σ-cong-equiv-fst W-in-equiv ⟩
Σ[ (s′ , f′) ∈ (Σ[ s ∈ S ] (P s → W S P)) ] W-rec sup* (sup s′ f′) ≡ sup* (s , W-rec sup* ∘ f)
≃⟨⟩
Σ[ (s′ , f′) ∈ (Σ[ s ∈ S ] (P s → W S P)) ] sup* (s′ , W-rec sup* ∘ f′) ≡ sup* (s , W-rec sup* ∘ f)
≃⟨ Σ-cong-equiv-snd (λ x → invEquiv $ cong sup* , is-emb-sup* _ _) ⟩
Σ[ (s′ , f′) ∈ (Σ[ s ∈ S ] (P s → W S P)) ] (s′ , W-rec sup* ∘ f′) ≡ (s , W-rec sup* ∘ f)
≃⟨ Σ-cong-equiv-snd (λ _ → invEquiv ΣPathP≃PathPΣ) ⟩
Σ[ (s′ , f′) ∈ (Σ[ s ∈ S ] (P s → W S P)) ] Σ _ _
≃⟨ strictEquiv
(λ { ((s′ , f′) , s′≡s , f≡f′) → ((s′ , sym s′≡s) , (f′ , f≡f′)) })
(λ { ((s′ , s≡s′) , (f′ , f≡f′)) → ((s′ , f′) , sym s≡s′ , f≡f′) })
⟩
Σ[ (s′ , s≡s′) ∈ singl s ] Σ[ f′ ∈ (P s′ → W S P) ] PathP (λ i → P (s≡s′ (~ i)) → A) (W-rec sup* ∘ f′) (W-rec sup* ∘ f)
≃⟨ Σ-contractFst (isContrSingl s) ⟩
Σ[ f′ ∈ (P s → W S P) ] (W-rec sup* ∘ f′) ≡ (W-rec sup* ∘ f)
≃⟨ Σ-cong-equiv-snd (λ f′ → invEquiv funExtEquiv) ⟩
Σ[ f′ ∈ (P s → W S P) ] ((p : P s) → W-rec sup* (f′ p) ≡ W-rec sup* (f p))
≃⟨ invEquiv Σ-Π-≃ ⟩
((p : P s) → fiber (W-rec sup*) (W-rec sup* (f p)))
≃∎
isEmbedding-W-rec : ∀ {ℓ} {S : Type ℓS} {P : S → Type ℓP} {A : Type ℓ}
→ (sup* : (Σ[ s ∈ S ] (P s → A)) → A)
→ isEmbedding sup*
→ isEmbedding (W-rec sup*)
isEmbedding-W-rec {S} {P} {A} sup* is-emb-sup* = hasPropFibersOfImage→isEmbedding prop-fibers where
fiber-equiv : ∀ s f → fiber (W-rec sup*) (W-rec sup* (sup s f)) ≃ ((p : P s) → fiber (W-rec sup*) (W-rec sup* (f p)))
fiber-equiv = isEmbedding→W-rec-fiber-equiv sup* is-emb-sup*
prop-fibers : ∀ w → isProp (fiber (W-rec sup*) (W-rec sup* w))
prop-fibers = W-elim goal where module _ (s : S) (f : P s → W S P) (ind : ∀ p → isProp (fiber (W-rec sup*) (W-rec sup* (f p)))) where
is-prop-fibers' : isProp (∀ p → fiber (W-rec sup*) (W-rec sup* (f p)))
is-prop-fibers' = isPropΠ ind
goal : isProp (fiber (W-rec sup*) (sup* (s , W-rec sup* ∘ f)))
goal = isOfHLevelRespectEquiv 1 (invEquiv $ fiber-equiv s f) is-prop-fibers'