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.Basics.W as W using (W)

open import Derivative.Isolated
open import Derivative.Remove

open import Derivative.Container
open import Derivative.Derivative

open import Cubical.Foundations.Equiv.Properties
import      Cubical.Foundations.Univalence as Univalence
import      Cubical.Foundations.Transport as Transport
open import Cubical.Data.Sigma
open import Cubical.Data.Empty using (uninhabEquiv)
open import  Cubical.HITs.SetTruncation as ST using (∥_∥₂)

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

russel : ¬ (Σ[ U ∈ Type ℓ ] Σ[ El ∈ (U → Type ℓ) ] hasSection El)
russel {ℓ} (U , El , code , code-sec) = paradox module russel where
  cast : ∀ {X} → El (code X) → X
  cast {X} = transport (code-sec X)

  data V : Type ℓ where
    sup* : (u : U) → (El u → V) → V

  sup : (X : Type ℓ) → (X → V) → V
  sup X el = sup* (code X) (el ∘ cast)

  _∈_ : V → V → Type _
  x ∈ sup* _ A = fiber A x

  _∉_ : V → V → Type _
  x ∉ X = ¬ x ∈ X

  ∈-sup-equiv-inh-fiber : (A : Type ℓ) (el : A → V)
    → (x : V)
    → (x ∈ sup A el) ≃ fiber el x
  ∈-sup-equiv-inh-fiber A _ _ = Σ-cong-equiv-fst equiv-fst where
    equiv-fst : El (code A) ≃ A
    equiv-fst = Univalence.pathToEquiv (code-sec A)

  not-in-self : Type _
  not-in-self = Σ[ x ∈ V ] x ∉ x

  R : V
  R = sup not-in-self fst

  in-R-iff-not-in-self : (X : V) → (X ∈ R) ≃ (X ∉ X)
  in-R-iff-not-in-self X =
    (Σ[ h ∈ El (code not-in-self) ] fst (cast h) ≡ X)
      ≃⟨ ∈-sup-equiv-inh-fiber not-in-self fst X ⟩
    (Σ[ u ∈ not-in-self ] fst u ≡ X)
      ≃⟨ strictEquiv (λ ((u , h) , p) → (u , sym p) , h) (λ ((u , p) , h) → (u , h) , sym p) ⟩
    (Σ[ (u , _) ∈ singl X ] u ∉ u)
      ≃⟨ (Σ-contractFst (isContrSingl X)) ⟩
    (X ∉ X)
      ≃∎

  R∈R≃R∉R : (R ∈ R) ≃ (R ∉ R)
  R∈R≃R∉R = in-R-iff-not-in-self R

  R∉R : R ∉ R
  R∉R R∈R = equivFun R∈R≃R∉R R∈R R∈R

  R∈R : R ∈ R
  R∈R = invEq R∈R≃R∉R R∉R

  paradox : ⊥
  paradox = R∉R R∈R

no-terminal : ¬ (Σ[ Y ∈ Container ℓ ℓ ] ∀ (X : Container ℓ ℓ) → isContr (Cart X Y))
no-terminal {ℓ} (Y@(T ◁ Q) , contr-cart) = russel (T , Q , code , code-sec) where
  is-equiv-Q : isEquiv Q
  is-equiv-Q .equiv-proof P = isOfHLevelRespectEquiv  equiv contr-cart-const-P where
    contr-cart-const-P : isContr (Cart (𝕪 P) (T ◁ Q))
    contr-cart-const-P = contr-cart (𝕪 P)

    equiv : (Cart {ℓS = ℓ} (𝕪 P) (T ◁ Q)) ≃ fiber Q P
    equiv =
      Cart (𝕪 P) (T ◁ Q)
        ≃⟨ Cart-Σ-equiv ⟩
      Σ[ t ∈ (𝟙* → T) ] ((x : 𝟙*) → Q (t x) ≃ P)
        ≃⟨ invEquiv Σ-Π-≃ ⟩
      (𝟙* → Σ[ t ∈ T ] Q t ≃ P)
        ≃⟨ Π𝟙*-equiv _ ⟩
      Σ[ t ∈ T ] Q t ≃ P
        ≃⟨ Σ-cong-equiv-snd (λ t → invEquiv Univalence.univalence) ⟩
      Σ[ t ∈ T ] Q t ≡ P
        ≃∎

  code : Type ℓ → T
  code = invIsEq is-equiv-Q

  code-sec : ∀ X → Q (code X) ≡ X
  code-sec X = secIsEq is-equiv-Q X

no-weak-terminal : ¬ (Σ[ Y ∈ Container ℓ ℓ ] ∀ (X : Container ℓ ℓ) → Cart X Y)
no-weak-terminal {ℓ} (Y@(T ◁ Q) , inh-cart) = russel (T , Q , code , code-sec) where
  Q-fiber-equiv : (P : Type ℓ) → Cart (𝕪 P) (T ◁ Q) ≃ fiber Q P
  Q-fiber-equiv P =
    Cart (𝕪 P) (T ◁ Q)
      ≃⟨ Cart-Σ-equiv ⟩
    Σ[ t ∈ (𝟙* → T) ] ((x : 𝟙*) → Q (t x) ≃ P)
      ≃⟨ invEquiv Σ-Π-≃ ⟩
    (𝟙* → Σ[ t ∈ T ] Q t ≃ P)
      ≃⟨ Π𝟙*-equiv _ ⟩
    Σ[ t ∈ T ] Q t ≃ P
      ≃⟨ Σ-cong-equiv-snd (λ t → invEquiv Univalence.univalence) ⟩
    Σ[ t ∈ T ] Q t ≡ P
      ≃∎

  Q-inh-fiber : ∀ P → fiber Q P
  Q-inh-fiber P = equivFun (Q-fiber-equiv P) (inh-cart (𝕪 P))

  code : Type ℓ → T
  code = fst ∘ Q-inh-fiber

  code-sec : ∀ X → Q (code X) ≡ X
  code-sec = snd ∘ Q-inh-fiber

private
  isEmpty→isContrΠ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
    → (¬ A) → isContr (∀ a → B a)
  isEmpty→isContrΠ ¬A .fst = ex-falso ∘ ¬A
  isEmpty→isContrΠ ¬A .snd f = funExt $ ex-falso ∘ ¬A

no-internal-hom : ¬ (Σ[ _⇒_ ∈ ((F G : Container ℓ ℓ) → Container ℓ ℓ) ] ∀ F G H → Cart (F ⊗ G) H ≃ Cart F (G ⇒ H))
no-internal-hom {ℓ} (_⇒_ , adj) = no-terminal (_ , is-terminal-∅⇒∅) where
  ∅ : Container ℓ ℓ
  ∅ .Shape = 𝟘*
  ∅ .Pos ()

  is-contr-into-∅ : (X : Container ℓ ℓ) → isContr (Cart (X ⊗ ∅) ∅)
  is-contr-into-∅ X@(S ◁ P) = isOfHLevelRespectEquiv  (invEquiv equiv) isContr-𝟙* where
    equiv : (Cart (X ⊗ ∅) ∅) ≃ 𝟙
    equiv =
      Cart (X ⊗ ∅) ∅
        ≃⟨ Cart-Σ-equiv ⟩
      Σ[ f ∈ ((S × 𝟘*) → 𝟘*) ] ((s : S × Shape ∅) → Pos ∅ (f s) ≃ (P (s .fst) ⊎ Pos ∅ (s .snd)))
        ≃⟨ Σ-contractSnd (λ f → isEmpty→isContrΠ λ ()) ⟩
      ((S × 𝟘*) → 𝟘*)
        ≃⟨ isContr→≃𝟙* (isEmpty→isContrΠ λ ()) ⟩
      𝟙
        ≃∎

  is-terminal-∅⇒∅ : (X : Container ℓ ℓ) → isContr (Cart X (∅ ⇒ ∅))
  is-terminal-∅⇒∅ X = isOfHLevelRespectEquiv  (adj X ∅ ∅) $ is-contr-into-∅ X

russel-set : ¬ (Σ[ U ∈ hSet ℓ ] Σ[ El ∈ (⟨ U ⟩ → hSet ℓ) ] hasSection El)
russel-set {ℓ} ((U , is-set-U) , El* , code* , code-sec*) = paradox where
  El : U → Type ℓ
  El = fst ∘ El*

  code-sec : (X : hSet ℓ) → El (code* X) ≡ ⟨ X ⟩
  code-sec X = cong ⟨_⟩ $ code-sec* X

  cast : (X : hSet ℓ) → El (code* X) → ⟨ X ⟩
  cast X = transport (code-sec X)

  V : Type ℓ
  V = W U El

  sup : (X : hSet ℓ) → (⟨ X ⟩ → V) → V
  sup X el = W.sup (code* X) (el ∘ cast X)

  is-set-V : isSet V
  is-set-V = W.isSetW is-set-U

  _∈_ : V → V → Type _
  x ∈ W.sup _ A = fiber A x

  _∉_ : V → V → Type _
  x ∉ X = ¬ x ∈ X

  ∈-sup-equiv-inh-fiber : (A : hSet ℓ) (el : ⟨ A ⟩ → V)
    → (x : V)
    → (x ∈ sup A el) ≃ fiber el x
  ∈-sup-equiv-inh-fiber A _ _ = Σ-cong-equiv-fst equiv-fst where
    equiv-fst : El (code* A) ≃ ⟨ A ⟩
    equiv-fst = Univalence.pathToEquiv $ code-sec A

  not-in-self : hSet ℓ
  not-in-self = (Σ[ x ∈ V ] x ∉ x) , (isSetΣSndProp is-set-V λ _ → isProp¬ _)

  R : V
  R = sup not-in-self fst

  in-R-iff-not-in-self : (X : V) → (X ∈ R) ≃ (X ∉ X)
  in-R-iff-not-in-self X =
    X ∈ sup not-in-self fst
      ≃⟨ ∈-sup-equiv-inh-fiber not-in-self fst X ⟩
    Σ[ (x , _) ∈ Σ[ x ∈ V ] x ∉ x ] x ≡ X
      ≃⟨ strictEquiv (λ ((u , h) , p) → (u , sym p) , h) (λ ((u , p) , h) → (u , h) , sym p) ⟩
    (Σ[ (u , _) ∈ singl X ] u ∉ u)
      ≃⟨ (Σ-contractFst (isContrSingl X)) ⟩
    (X ∉ X)
      ≃∎

  R∈R≃R∉R : (R ∈ R) ≃ (R ∉ R)
  R∈R≃R∉R = in-R-iff-not-in-self R

  R∉R : R ∉ R
  R∉R R∈R = equivFun R∈R≃R∉R R∈R R∈R

  R∈R : R ∈ R
  R∈R = invEq R∈R≃R∉R R∉R

  paradox : ⊥
  paradox = R∉R R∈R

no-weak-terminal-set : ¬ (Σ[ Y ∈ SetContainer ℓ ℓ ] ∀ (X : SetContainer ℓ ℓ) → SetCart X Y)
no-weak-terminal-set {ℓ} ((Y@(T ◁ Q) , is-set-T , is-set-Q) , inh-set-cart) = russel-set (T* , Q* , code , code-sec) where
  T* : hSet ℓ
  T* = T , is-set-T

  Q* : T → hSet ℓ
  Q* t = Q t , is-set-Q t

  𝕪-set : hSet ℓ → SetContainer ℓ ℓ
  𝕪-set P .fst = 𝕪 ⟨ P ⟩
  𝕪-set P .snd .fst = isSet-𝟙*
  𝕪-set P .snd .snd _ = str P

  Q*-fiber-equiv : (P : hSet ℓ) → Cart (𝕪 ⟨ P ⟩) (T ◁ Q) ≃ fiber Q* P
  Q*-fiber-equiv P*@(P , _) =
    Cart (𝕪 P) (T ◁ Q)
      ≃⟨ Cart-Σ-equiv ⟩
    Σ[ t ∈ (𝟙* → T) ] ((x : 𝟙*) → Q (t x) ≃ P)
      ≃⟨ invEquiv Σ-Π-≃ ⟩
    (𝟙* → Σ[ t ∈ T ] Q t ≃ P)
      ≃⟨ Π𝟙*-equiv _ ⟩
    Σ[ t ∈ T ] Q t ≃ P
      ≃⟨ Σ-cong-equiv-snd (λ t → invEquiv Univalence.univalence) ⟩
    Σ[ t ∈ T ] Q t ≡ P
      ≃⟨ Σ-cong-equiv-snd (λ t → Σ≡PropEquiv λ _ → isPropIsSet) ⟩
    Σ[ t ∈ T ] Q* t ≡ P*
      ≃∎

  Q*-inh-fiber : ∀ P → fiber Q* P
  Q*-inh-fiber P = equivFun (Q*-fiber-equiv P) (inh-set-cart (𝕪-set P))

  code : hSet ℓ → T
  code = fst ∘ Q*-inh-fiber

  code-sec : ∀ X → Q* (code X) ≡ X
  code-sec = snd ∘ Q*-inh-fiber

private
  _⊗ₛ_ : SetContainer ℓ ℓ → SetContainer ℓ ℓ → SetContainer ℓ ℓ
  ((F , is-set-F) ⊗ₛ (G , is-set-G)) .fst = F ⊗ G
  ((F , is-set-F) ⊗ₛ (G , is-set-G)) .snd .fst = isSet× (is-set-F .fst) (is-set-G .fst)
  ((F , is-set-F) ⊗ₛ (G , is-set-G)) .snd .snd (s , t) = Sum.isSet⊎ (is-set-F .snd s) (is-set-G .snd t)

no-internal-hom-set : ¬ (Σ[ _⇒_ ∈ ((F G : SetContainer ℓ ℓ) → SetContainer ℓ ℓ) ] ∀ F G H → SetCart (F ⊗ₛ G) H → SetCart F (G ⇒ H))
no-internal-hom-set {ℓ} (_⇒_ , curry) = no-weak-terminal-set (∅ ⇒ ∅ , is-weak-terminal-∅⇒∅) where
  ∅ : SetContainer ℓ ℓ
  ∅ .fst .Shape = 𝟘*
  ∅ .fst .Pos ()
  ∅ .snd .fst ()
  ∅ .snd .snd ()

  is-weak-terminal-∅⇒∅ : (X : SetContainer ℓ ℓ) → SetCart X (∅ ⇒ ∅)
  is-weak-terminal-∅⇒∅ X = curry X ∅ ∅ λ where
    .Cart.shape ()
    .Cart.pos ()