\begin{code}
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Cardinality.Finite.Kuratowski where

open import Prelude
open import Algebra.Construct.Free.Semilattice
open import Algebra.Construct.Free.Semilattice.Relation.Unary

open import Cardinality.Finite.ManifestEnumerable
open import Cardinality.Finite.ManifestEnumerable.Inductive renaming (_∈_ to _L∈_)

open import HITs.PropositionalTruncation
import HITs.PropositionalTruncation as PropTrunc
open import HITs.PropositionalTruncation.Sugar
open import Data.Fin

𝒦ᶠ : Type a → Type a
\end{code}
%<*kuratowski-finite-def>
\begin{code}
𝒦ᶠ A = Σ[ xs ⦂ 𝒦 A ] ((x : A) → x ∈ xs)
\end{code}
%</kuratowski-finite-def>
\begin{code}

𝒦ᶠ⇒∥ℰ∥ : 𝒦ᶠ A → ∥ ℰ A ∥
𝒦ᶠ⇒∥ℰ∥ K = map₂ (λ p x → p x (K .snd x)) ∥$∥ ∥ enum ∥⇓ (K .fst)
  where
  enum : xs ∈𝒦 A ⇒∥ ∥ Σ[ ys ⦂ List A ] (∀ x → x ∈ xs → ∥ x L∈ ys ∥) ∥ ∥
  ∥ enum ∥-prop = squash
  ∥ enum ∥[] = ∣ [] , (λ _ ()) ∣
  ∥ enum ∥ x ∷ xs ⟨ Pxs ⟩ = cons ∥$∥ Pxs
    where
    cons : _
    cons (ys , p) .fst = x ∷ ys
    cons (ys , p) .snd z zs = zs >>= either′ (∣_∣ ∘ (f0 ,_)) ((push ∥$∥_) ∘ p z)

open import Algebra.Construct.Free.Semilattice.Extensionality
open import Algebra.Construct.Free.Semilattice.FromList
open import Data.Sigma.Properties

isProp𝒦ᶠ : isProp (𝒦ᶠ A)
isProp𝒦ᶠ Kˣ Kʸ =
  ΣProp≡
    (λ K p q i x → isProp-◇ {xs = K} (p x) (q x) i)
    {Kˣ} {Kʸ}
    (extensional (fst Kˣ) (fst Kʸ) λ x → const (Kʸ .snd x) iff const (Kˣ .snd x))

ℰ⇒𝒦 : ℰ A → 𝒦ᶠ A
ℰ⇒𝒦 E .fst = fromList (E .fst)
ℰ⇒𝒦 E .snd x = ∈List⇒∈𝒦 (E .fst) (E .snd x)

open import Cubical.HITs.S1 using (S¹)

𝒦ᶠ⟨S¹⟩ : 𝒦ᶠ S¹
𝒦ᶠ⟨S¹⟩ = ℰ⇒𝒦 ℰ⟨S¹⟩
∥ℰ∥⇔𝒦 :
\end{code}
%<*manifest-enum-kuratowski>
\begin{code}
 ∥ ℰ A ∥ ⇔ 𝒦ᶠ A
\end{code}
%</manifest-enum-kuratowski>
\begin{code}
∥ℰ∥⇔𝒦 .fun = PropTrunc.rec isProp𝒦ᶠ ℰ⇒𝒦
∥ℰ∥⇔𝒦 .inv = 𝒦ᶠ⇒∥ℰ∥
∥ℰ∥⇔𝒦 .leftInv x = squash _ x
∥ℰ∥⇔𝒦 .rightInv x = isProp𝒦ᶠ _ x

open import Cardinality.Finite.Cardinal using (𝒞; 𝒞⇒Discrete)
open import Cardinality.Finite.ManifestBishop using (ℬ⇒ℰ!; ℰ!⇒ℬ)
open import Cardinality.Finite.ManifestEnumerable using (ℰ!⇒ℰ; ℰ⇒ℰ!)
open import Relation.Nullary.Discrete.Properties

𝒞⇔𝒦×Discrete :
\end{code}
%<*card-iso-kuratowski>
\begin{code}
  𝒞 A ⇔ 𝒦ᶠ A × Discrete A
\end{code}
%</card-iso-kuratowski>
\begin{code}
𝒞⇔𝒦×Discrete .fun ca .fst = ∥ℰ∥⇔𝒦 .fun (ℰ!⇒ℰ ∘ ℬ⇒ℰ! ∥$∥ ca)
𝒞⇔𝒦×Discrete .fun ca .snd = 𝒞⇒Discrete ca
𝒞⇔𝒦×Discrete .inv (ka , d) = ℰ!⇒ℬ ∘ ℰ⇒ℰ! d ∥$∥ ∥ℰ∥⇔𝒦 .inv ka
𝒞⇔𝒦×Discrete .rightInv _ = isOfHLevelΣ  isProp𝒦ᶠ (λ _ → isPropDiscrete) _ _
𝒞⇔𝒦×Discrete .leftInv  _ = squash _ _

open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Omniscience
open import HITs.PropositionalTruncation.Properties

private variable p : Level

𝒦ᶠ⇒Exhaustible : 𝒦ᶠ A → Exhaustible p A
𝒦ᶠ⇒Exhaustible K P? =
  ∣ ◻? P? (K .fst)
    ∣yes⇒ (λ ◻Pxs x → recompute (P? x) (P∈◇ x (K .fst) (K .snd x) ◻Pxs))
    ∣no⇒ λ ¬◻Pxs ∀P → ¬◻Pxs (map-◻ ∀P (K .fst))

\end{code}
%<*kuratowski-prop-omniscient>
\begin{code}
𝒦ᶠ⇒Prop-Omniscient : 𝒦ᶠ A → Prop-Omniscient p A
𝒦ᶠ⇒Prop-Omniscient K P? =
  PropTrunc.rec
    (isPropDec squash)
    (map-dec ∣_∣ refute-trunc ∘ λ xs → ℰ⇒Omniscient xs P?)
    (𝒦ᶠ⇒∥ℰ∥ K)
\end{code}
%</kuratowski-prop-omniscient>