{-# OPTIONS --cubical --no-import-sorts -WnoUnsupportedIndexedMatch --allow-unsolved-metas #-}
module AFF2024.Basics where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.Data.Empty
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Nat
open import Cubical.Relation.Nullary.Base
open import Data.List
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.AllPairs

module _ {ℓ ℓ' : Level} (X : Type ℓ) (R : X → X → Type ℓ') where
  Infinite : Type (ℓ-max ℓ ℓ')
  Infinite = (xs : List X) → ∃[ y ∈ X ] All (R y) xs

module _ {ℓ ℓ' : Level} {X : Type ℓ} {R : X → X → Type ℓ'} where
  module _ (inf : Infinite X R) where
    takeFrom∞ : (n : ℕ) → ∃[ xs ∈ List X ] ((length xs ≡ n) × AllPairs R xs)
    takeFrom∞ zero    = ∣ [] , refl , [] ∣₁
    takeFrom∞ (suc n) = do
      (xs , len , p) ← takeFrom∞ n
      (y , q)        ← inf xs
      return (y ∷ xs , cong suc len , q ∷ p)

allP : {ℓ ℓ' : Level} {X : Type ℓ} {P : X → Type ℓ'} → ((x : X) → P x) → (xs : List X) → All P xs
allP f []       = []
allP f (x ∷ xs) = f x ∷ allP f xs

∅ : {ℓ : Level} {X : Type ℓ} → ℙ X
∅ x = ⊥* , isProp⊥*

_∪_ : {ℓ : Level} {X : Type ℓ} → ℙ X → ℙ X → ℙ X
A ∪ B = λ x → ∥ fst (A x) ⊎ fst (B x) ∥₁ , isPropPropTrunc

module _ {ℓ : Level} {X : Type ℓ} where
  _≢_ : X → X → Type ℓ
  a ≢ b = ¬ (a ≡ b)

module _ {ℓ : Level} {X : Type ℓ} where
  IsExploding : (A : ℙ X) → Type ℓ
  IsExploding A = ∃[ n ∈ ℕ ] ((xs : List X) → length xs ≡ n → All (_∈ A) xs → AllPairs _≢_ xs → (x : X) → x ∈ A)

  ∅-isExploding : IsExploding ∅
  ∅-isExploding = ∣ suc zero , (λ { [] eq p q → Cubical.Data.Empty.rec (znots eq) ; (x ∷ xs) eq (px ∷ p) q → Cubical.Data.Empty.rec* px }) ∣₁

  ∪-isExploding : {A B : ℙ X} → IsExploding A → IsExploding B → IsExploding (A ∪ B)
  ∪-isExploding f g = do
    (n , p) ← f
    (m , q) ← g
    {!!}