Derivative.Properties

{-# OPTIONS --safe #-}
module Derivative.Properties where

open import Derivative.Prelude
open import Derivative.Basics.Decidable as Dec
open import Derivative.Basics.Maybe
open import Derivative.Basics.Sum as Sum using (_⊎_ ; inl ; inr)
open import Derivative.Basics.Unit

open import Derivative.Isolated
open import Derivative.Remove

open import Derivative.Container
open import Derivative.Derivative

open import Cubical.Foundations.Equiv.Properties
open import Cubical.Data.Sigma
open import Cubical.Data.Empty using (uninhabEquiv)

private
  variable
    ℓ ℓS ℓP : Level

open Container
open Cart

∂-Const : (S : Type ℓ) → Equiv (∂ (Const S)) (Const 𝟘*)
∂-Const S .Equiv.shape = uninhabEquiv (λ ()) (λ ())
∂-Const S .Equiv.pos ()

∂-prop-trunc : (S : Type ℓ) {P : S → Type ℓ} → (∀ s → isProp (P s))
  → Equiv (∂ (S ◁ P)) (Σ S P ◁ const 𝟘*)
∂-prop-trunc S {P} is-prop-P =
  ∂ (S ◁ P)
    ⊸≃⟨⟩
  [ (s , p , _) ∈ Σ[ s ∈ S ] (P s) ° ]◁ (P s ∖ p)
    ⊸≃⟨ Equiv-fst $ Σ-cong-equiv-snd (λ s → isProp→IsolatedEquiv (is-prop-P s)) ⟩
  [ (s , p) ∈ Σ S P ]◁ (P s ∖ p)
    ⊸≃⟨ Equiv-snd (λ (s , p) → uninhabEquiv (λ ()) (isProp→isEmptyRemove (is-prop-P s) p)) ⟩
  [ (s , p) ∈ Σ S P ]◁ 𝟘*
    ⊸≃∎

∂-prop : (P : Type ℓ) → isProp P → Equiv (∂ (𝟙* {ℓ} ◁ const P)) (P ◁ const 𝟘*)
∂-prop {ℓ} P is-prop-P =
  ∂ (𝟙* {ℓ} ◁ const P)
    ⊸≃⟨ ∂-prop-trunc 𝟙* {P = const P} (const is-prop-P) ⟩
  ((𝟙* × P) ◁ const 𝟘*)
    ⊸≃⟨ Equiv-fst 𝟙*-unit-×-left-equiv ⟩
  (P ◁ const 𝟘*)
    ⊸≃∎

∂-Id : Equiv (∂ Id) (Const (𝟙* {ℓ}))
∂-Id = ∂-prop 𝟙* isProp-𝟙*

𝕂 : (A : Type ℓ) → Container ℓ ℓ
𝕂 A .Shape = A
𝕂 A .Pos = const 𝟘*

𝕪[_] : (A : Type ℓ) → Container ℓ ℓ
𝕪[ A ] .Shape = 𝟙*
𝕪[ A ] .Pos = const A

∂-𝕪° : (A : Type ℓ) → (a° : A °) → Equiv (∂ 𝕪[ A ]) ([ a ∈ A ° ]◁ (A ∖° a))
∂-𝕪° {ℓ} A a°@(a₀ , a₀≟_) =
  ∂ (𝟙* ◁ const A)
    ⊸≃⟨⟩
  ([ (_ , a) ∈ 𝟙* × (A °) ]◁ (A ∖° a))
    ⊸≃⟨ Equiv-fst 𝟙*-unit-×-left-equiv ⟩
  ([ a ∈ A ° ]◁ (A ∖° a))
    ⊸≃∎

∂-𝕪 : (A : Type ℓ) → Discrete A → Equiv (∂ 𝕪[ A ⊎ 𝟙* ]) (𝕂 (A ⊎ 𝟙*) ⊗ 𝕪[ A ])
∂-𝕪 {ℓ} A discrete-A = [ isoToEquiv shape-Iso ◁≃ invEquiv ∘ pos-equiv ] where
  shape-Iso : Iso _ _
  shape-Iso .Iso.fun (_ , x , _) = x , _
  shape-Iso .Iso.inv (just a , _) = _ , just° (a , discrete-A a)
  shape-Iso .Iso.inv (nothing , _) = _ , nothing°
  shape-Iso .Iso.rightInv (just a , _) = refl
  shape-Iso .Iso.rightInv (nothing , _) = refl
  shape-Iso .Iso.leftInv (_ , just a , _) = ≡-× refl (Isolated≡ $ refl′ $ just a)
  shape-Iso .Iso.leftInv (_ , nothing , _) = ≡-× refl (Isolated≡ $ refl′ nothing)

  pos-equiv : ((_ , x) : _ × (Maybe A °)) → ((Maybe A) ∖° x) ≃ (𝟘* ⊎ A)
  pos-equiv (_ , x) = e x ∙ₑ (Sum.⊎-empty-left λ ()) where
    e : (x : Maybe A °) → ((Maybe A) ∖° x) ≃ A
    e (nothing , _) = removeNothingEquiv
    e (just a , isolated-just-a) = removeJustEquiv a $ isIsolatedFromJust isolated-just-a

module _ (F G : Container ℓ ℓ) where
  open Container F renaming (Shape to S ; Pos to P)
  open Container G renaming (Shape to T ; Pos to Q)

  sum-shape : (Σ[ x ∈ S ⊎ T ] Pos (F ⊕ G) x °) ≃ ((Σ[ s ∈ S ] P s °) ⊎ (Σ[ t ∈ T ] Q t °))
  sum-shape = Sum.Σ-⊎-fst-≃

  sum-rule : Equiv (∂ (F ⊕ G)) (∂ F ⊕ ∂ G)
  sum-rule .Equiv.shape = sum-shape
  sum-rule .Equiv.pos = uncurry (Sum.elim (λ s p → idEquiv (P s ∖ p .fst)) (λ t q → idEquiv (Q t ∖ q .fst)))

module _ (F G : Container ℓ ℓ) where
  open Container F renaming (Shape to S ; Pos to P)
  open Container G renaming (Shape to T ; Pos to Q)

  prod-shape :
    (Σ[ (s , t) ∈ S × T ] (P s ⊎ Q t) °)
      ≃
    (((Σ[ s ∈ S ] P s °) × T) ⊎ (S × (Σ[ t ∈ T ] Q t °)))
  prod-shape =
    (Σ[ (s , t) ∈ S × T ] (P s ⊎ Q t) °)
      ≃⟨ Σ-cong-equiv-snd (λ _ → IsolatedSumEquiv) ⟩
    (Σ[ (s , t) ∈ S × T ] (P s °) ⊎ (Q t °))
      ≃⟨ Sum.Σ-⊎-snd-≃ ⟩
    ((Σ[ (s , _) ∈ S × T ] P s °) ⊎ (Σ[ (_ , t) ∈ S × T ] (Q t °)))
      ≃⟨ Sum.⊎-equiv shuffle-left shuffle-right ⟩
    (((Σ[ s ∈ S ] P s °) × T) ⊎ (S × (Σ[ t ∈ T ] Q t °)))
      ≃∎
      where
        shuffle-left : _ ≃ _
        shuffle-left = strictEquiv (λ ((s , t) , p) → ((s , p) , t)) (λ ((s , p) , t) → ((s , t) , p))

        shuffle-right : _ ≃ _
        shuffle-right = strictEquiv (λ ((s , t) , q) → (s , (t , q))) (λ (s , (t , q)) → ((s , t) , q))

  prod-rule : Equiv (∂ (F ⊗ G)) ((∂ F ⊗ G) ⊕ (F ⊗ ∂ G))
  prod-rule .Equiv.shape = prod-shape
  prod-rule .Equiv.pos = uncurry λ where
    (s , t) (inl p , _) → remove-left-equiv
    (s , t) (inr q , _) → remove-right-equiv

module _ {Ix : Type ℓ} (F : Ix → Container ℓ ℓ) where
  ∑ : Container ℓ ℓ
  ∑ .Shape = Σ[ ix ∈ Ix ] F ix .Shape
  ∑ .Pos (ix , s) = F ix .Pos s

module _ {Ix : Type ℓ} (F : Ix → Container ℓ ℓ) where
  sum'-rule : Equiv (∂ (∑ F)) (∑ (∂ ∘ F))
  sum'-rule .Equiv.shape = Σ-assoc-≃
  sum'-rule .Equiv.pos ((ix , s) , p , _) = idEquiv $ F ix .Pos s ∖ p