Jon Sterling, 25th March 2023.

Proof of Cantor's theorem stated for embeddings from the powerset of A
onto A. This proof uses function extensionality, propositional
extensionality, and propositional resizing. Our argument follows
Taylor's Practical Foundations of Mathematics, via the nLab:
https://ncatlab.org/nlab/show/Cantor%27s+theorem.

This applies Cantor's theorem for surjections, proved in
Various.LawvereFPT.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Various.CantorTheoremForEmbeddings where

open import MLTT.Spartan


open import UF.Base
open import UF.Embeddings
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.FunExt
open import UF.Size
open import Various.LawvereFPT
open import UF.SubtypeClassifier

open retract-version

cantor-theorem-for-embeddings
 : FunExt
 → PropExt
 → Propositional-Resizing
 → (A : 𝓤 ̇ )
 → (ϕ : (A → Ω₀) → A)
 → ¬ is-embedding ϕ
cantor-theorem-for-embeddings {𝓤} fe pe psz A ϕ ϕ-emb =
 cantor-theorem (fe _ _) A retr retr-has-section
 where

  retr-large : A → (A → Ω (𝓤₀ ⁺ ⊔ 𝓤))
  pr₁ (retr-large a b) = Π U ꞉ (A → Ω₀) , (ϕ U ＝ a → U b holds)
  pr₂ (retr-large a b) =
   Π-is-prop (fe _ _) λ U →
   Π-is-prop (fe _ _) λ _ →
   holds-is-prop (U b)

  retr : A → (A → Ω₀)
  pr₁ (retr a b) =
   resize psz
    (retr-large a b holds)
    (holds-is-prop (retr-large a b))
  pr₂ (retr a b) =
   resize-is-prop psz
    (retr-large a b holds)
    (holds-is-prop (retr-large a b))

  retr-has-section : has-section· retr
  pr₁ retr-has-section U = ϕ U
  pr₂ retr-has-section U a =
   to-Σ-＝ (lem·0 , being-prop-is-prop (fe 𝓤₀ 𝓤₀) _ _)
   where
    fwd : retr-large (ϕ U) a holds → U a holds
    fwd p = p U refl

    bwd : U a holds → retr-large (ϕ U) a holds
    bwd p V q =
     transport⁻¹
      (λ W → W a holds)
      (embeddings-are-lc ϕ ϕ-emb q)
      p

    lem·0 : resize psz (retr-large (ϕ U) a holds) _ ＝ U a holds
    lem·0 =
     pe 𝓤₀
      (resize-is-prop psz _ _)
      (holds-is-prop (U a))
      (fwd ∘ from-resize psz _ _)
      (to-resize psz _ _ ∘ bwd)

\end{code}