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

module Cardinality.Finite.SplitEnumerable where

open import Prelude
open import Container
open import Data.Fin
open import Data.Sigma.Properties
open import Function.Surjective.Properties
open import Data.Fin.Properties

import Cardinality.Finite.SplitEnumerable.Container as ℒ
import Cardinality.Finite.SplitEnumerable.Inductive as 𝕃
open import Cardinality.Finite.SplitEnumerable.Isomorphism

open import Data.Nat.Literals
open import Data.Fin.Literals
open import Literals.Number

private
  variable
    u : Level
    U : A → Type u

module _ {a} {A : Type a} where
 open ℒ
 open import Container.List
 open import Container.Membership (ℕ , Fin)
 open import Relation.Binary.Equivalence.Reasoning (⇔-equiv {a})

\end{code}
%<*split-enum-is-split-surj-short>
\begin{code}
 split-enum-is-split-surj : ℰ! A ⇔ Σ[ n ⦂ ℕ ] (Fin n ↠! A)
 split-enum-is-split-surj = reassoc
\end{code}
%</split-enum-is-split-surj-short>
\begin{code}

 ℰ!⇔Fin↠! :
\end{code}
%<*is-split-inj-type>
\begin{code}
   ℰ! A ⇔ Σ[ n ⦂ ℕ ] (Fin n ↠! A)
\end{code}
%</is-split-inj-type>
\begin{code}
 ℰ!⇔Fin↠! =
\end{code}
%<*is-split-inj>
\begin{code}
   ℰ! A                                                       ≋⟨⟩
   Σ[ xs ⦂ List A ] ((x : A) → x ∈ xs)                        ≋⟨⟩
   Σ[ xs ⦂ List A ] ((x : A) → fiber (snd xs) x)              ≋⟨⟩
   Σ[ xs ⦂ List A ] SplitSurjective (snd xs)                  ≋⟨⟩
   Σ[ xs ⦂ ⟦ ℕ , Fin ⟧ A ] SplitSurjective (snd xs)           ≋⟨⟩
   Σ[ xs ⦂ Σ[ n ⦂ ℕ ] (Fin n → A) ] SplitSurjective (snd xs)  ≋⟨ reassoc ⟩
   Σ[ n ⦂ ℕ ] Σ[ f ⦂ (Fin n → A) ] SplitSurjective f          ≋⟨⟩
   Σ[ n ⦂ ℕ ] (Fin n ↠! A) ∎
\end{code}
%</is-split-inj>
%<*split-is-discrete>
\begin{code}
 ℰ!⇒Discrete : ℰ! A → Discrete A
 ℰ!⇒Discrete  = flip Discrete-distrib-surj discreteFin
              ∘ snd
              ∘ ℰ!⇔Fin↠! .fun
\end{code}
%</split-is-discrete>
\begin{code}
module _ where
 open 𝕃
 open import Data.List.Sugar hiding ([_])
 open import Data.List.Syntax
 open import Data.List.Membership

 module BoolSlop where
\end{code}
%<*bool-slop>
\begin{code}
   ℰ!⟨2⟩ : ℰ! Bool
   ℰ!⟨2⟩ .fst = [ false , true , false ]
   ℰ!⟨2⟩ .snd false  =   , refl
   ℰ!⟨2⟩ .snd true   =   , refl
\end{code}
%</bool-slop>
\begin{code}
\end{code}
%<*bool-rev>
\begin{code}
 ℰ!⟨2⟩′ : ℰ! Bool
 ℰ!⟨2⟩′ .fst = [ true , false ]
 ℰ!⟨2⟩′ .snd false  =   , refl
 ℰ!⟨2⟩′ .snd true   =   , refl
\end{code}
%</bool-rev>
%<*bool-inst>
\begin{code}
 ℰ!⟨2⟩ : ℰ! Bool
 ℰ!⟨2⟩ .fst = [ false , true ]
 ℰ!⟨2⟩ .snd false  =   , refl
 ℰ!⟨2⟩ .snd true   =   , refl
\end{code}
%</bool-inst>
%<*top-bot-inst>
\begin{code}
 ℰ!⟨⊤⟩ : ℰ! ⊤
 ℰ!⟨⊤⟩ .fst = [ tt ]
 ℰ!⟨⊤⟩ .snd _ =  , refl

 ℰ!⟨⊥⟩ : ℰ! ⊥
 ℰ!⟨⊥⟩ = [] , λ ()
\end{code}
%</top-bot-inst>
%<*sup-sigma>
\begin{code}
 sup-Σ :  List A →
          ((x : A) → List (U x)) →
          List (Σ A U)
 sup-Σ xs ys = do  x ← xs
                   y ← ys x
                   [ x , y ]
\end{code}
%</sup-sigma>
\begin{code}
 cov-Σ : (x : A)
       → (y : U x)
       → (xs : List A)
       → (ys : ∀ x → List (U x))
       → x ∈ xs
       → y ∈ ys x
       → (x , y) ∈ sup-Σ xs ys
 cov-Σ xᵢ yᵢ (x ∷ xs) ys (fs n , x∈xs) y∈ys =
   map (x ,_) (ys x) ++◇ cov-Σ xᵢ yᵢ xs ys (n , x∈xs) y∈ys
 cov-Σ xᵢ yᵢ (x ∷ xs) ys (f0  , x∈xs) y∈ys =
   subst (λ x′ → (xᵢ , yᵢ) ∈ sup-Σ (x′ ∷ xs) ys) (sym x∈xs)
   (map (xᵢ ,_) (ys xᵢ) ◇++ cong-∈ (xᵢ ,_) (ys xᵢ) y∈ys)
\end{code}
%<*split-enum-sigma>
\begin{code}
 _|Σ|_ : ℰ! A → (∀ x → ℰ! (U x)) → ℰ! (Σ A U)
\end{code}
%</split-enum-sigma>
\begin{code}
 (xs |Σ| ys) .fst = sup-Σ (xs .fst) (fst ∘ ys)
 (xs |Σ| ys) .snd (x , y) = cov-Σ x y (xs .fst) (fst ∘ ys) (xs .snd x) (ys x .snd y)

 ℰ!⟨Fin⟩ : ∀ {n} → ℰ! (Fin n)
 ℰ!⟨Fin⟩ .fst = tabulate _ id
 ℰ!⟨Fin⟩ .snd = fin∈tabulate id

 _|×|_ : ℰ! A → ℰ! B → ℰ! (A × B)
 xs |×| ys = xs |Σ| const ys

 _|⊎|_ : ℰ! A → ℰ! B → ℰ! (A ⊎ B)
 (xs |⊎| ys) .fst = map inl (xs .fst) ++ map inr (ys .fst)
 (xs |⊎| ys) .snd (inl x) = map inl (xs .fst) ◇++ cong-∈ inl (xs .fst) (xs .snd x)
 (xs |⊎| ys) .snd (inr y) = map inl (xs .fst) ++◇ cong-∈ inr (ys .fst) (ys .snd y)

 _|+|_ : ℰ! A → ℰ! B → ℰ! (Σ[ t ⦂ Bool ] (if t then A else B))
 xs |+| ys = ℰ!⟨2⟩ |Σ| bool ys xs

 module TupleUniverseMonomorphic where
   open import Data.Tuple.UniverseMonomorphic

   ℰ!⟨Tuple⟩ : ∀ {n} {U : Fin n → Type₀} → (∀ i → ℰ! (U i)) → ℰ! (Tuple n U)
   ℰ!⟨Tuple⟩ {n = zero}  f = (_ ∷ []) , λ _ → f0 , refl
   ℰ!⟨Tuple⟩ {n = suc n} f = f f0 |×| ℰ!⟨Tuple⟩ (f ∘ fs)

 open import Data.Tuple

 ℰ!⟨Tuple⟩ : ∀ {n u} {U : Lift a (Fin n) → Type u} → (∀ i → ℰ! (U i)) → ℰ! (Tuple n U)
 ℰ!⟨Tuple⟩ {n = zero}  f = (_ ∷ []) , λ _ → f0 , refl
 ℰ!⟨Tuple⟩ {n = suc n} f = f (lift f0) |×| ℰ!⟨Tuple⟩ (f ∘ lift ∘ fs ∘ lower)

 ℰ!⟨Lift⟩ : ℰ! A → ℰ! (Lift b A)
 ℰ!⟨Lift⟩ xs .fst = map lift (xs .fst)
 ℰ!⟨Lift⟩ xs .snd x = cong-∈ lift (xs .fst) (xs .snd (x .lower))

 ℰ!⟨≡⟩ : (x y : A) → ℰ! A → ℰ! (x ≡ y)
 ℰ!⟨≡⟩ x y e with ℰ!⇒Discrete (𝕃⇔ℒ⟨ℰ!⟩ .fun e) x y
 ℰ!⟨≡⟩ x y e | yes p = (p ∷ []) , λ q → (f0 , Discrete→isSet (ℰ!⇒Discrete (𝕃⇔ℒ⟨ℰ!⟩ .fun e)) x y p q)
 ℰ!⟨≡⟩ x y e | no ¬p = [] , (⊥-elim ∘ ¬p)

 open import Data.List.Filter
 open import Cardinality.Finite.SplitEnumerable.Inductive

 module _ {p} {P : A → Type p} where

\end{code}
%<*subobject>
\begin{code}
  filter-subobject :
    (∀ x → isProp (P x)) →
    (∀ x → Dec (P x)) →
    ℰ! A →
    ℰ! (Σ[ x ⦂ A ] P x)
\end{code}
%</subobject>
\begin{code}
  filter-subobject isPropP P? xs .fst = filter P? (xs .fst)
  filter-subobject isPropP P? xs .snd (x , v) = filter-preserves isPropP P? (xs .fst) x v (xs .snd x)
\end{code}