module WISC where

open import AlgebraicSignature public
open import Axioms  public
open import Prelude public

----------------------------------------------------------------------
-- Families of sets
----------------------------------------------------------------------
Fam : (l : Level) → Set (lsuc l)
Fam l = ∑ C ∶ Set l , (C → Set l)

-- Families are signatures
sig : Fam ℓ₀ → Sig
Op (sig (C , E)) = C
Ar (sig (C , E)) = E

-- Family of kernels
Ker : {l : Level} → Fam l → Set l → Fam l
π₁ (Ker (A , B) X)         = ∑ a ∶ A , (B a → X)
π₂ (Ker (A , B) X) (a , f) = ker f

----------------------------------------------------------------------
-- WISC property of a family W for a set A
----------------------------------------------------------------------
wisc : {l : Level} → Set l → Fam l → ∀ m → Prop (l ⊔ lsuc m)
wisc A (C , D) m =
  (X : Set m)
  (e : X → A)
  (_ : surjection e)
  → --------------------------------------------
  ∃ c ∶ C , ∃ f ∶ (D c → X) , surjection (e ∘ f)

----------------------------------------------------------------------
-- A weak form of choice derived from wisc
----------------------------------------------------------------------
wAC :
  {l : Level}
  {A : Set l}
  ((C , D) : Fam l)
  (_ : wisc A (C , D) l)
  (B : A → Set l)
  (P : (x : A) → B x → Prop l)
  (_ : ∀ x → ∃ (B x) (P x))
  → ------------------------------------
  ∃ c ∶ C ,
  ∃ p ∶ (D c → A),
  ∃ q ∶ ((z : D c) → B (p z)),
    (surjection p ∧ ∀ z → P (p z) (q z))
wAC {l} {A} (C , D) w B P e = wac
  where
  E : Set l
  E = set (x , y) ∶ (∑ A B), P x y

  p' : E → A
  p' ((x , _) ∣ _) = x

  surjectionp' : surjection p'
  surjectionp' x with e x
  ... | ∃i y u = ∃i ((x , y) ∣ u) refl

  q' : (z : E) → B (p' z)
  q' ((_ , y) ∣ _) = y

  r : ∀ z → P (p' z) (q' z)
  r ((_ , _) ∣ p) = p

  wac : ∃ c ∶ C , ∃ p ∶ (D c → A), ∃ q ∶ ((z : D c) → B (p z)),
    (surjection p ∧ ∀ z → P (p z) (q z))
  wac with w E p' surjectionp'
  ... | ∃i c (∃i k u) =
    ∃i c (
    ∃i (p' ∘ k) (
    ∃i (q' ∘ k) (
    ∧i u λ z → r (k z))))

----------------------------------------------------------------------
-- The WISC AXiom
----------------------------------------------------------------------
postulate
  WISC : ∀{l}(A : Set l) → ∀ m → ∃ F ∶ Fam l , wisc A F m

----------------------------------------------------------------------
-- WISC implies existence of wisc for indexed families of sets
----------------------------------------------------------------------
IWISC :
  {l : Level}
  ((A , B) : Fam l)
  (m : Level)
  → --------------------------------
  ∃ F ∶ Fam l , ∀ a → wisc (B a) F m
IWISC {l} (A , B) m with WISC A (lsuc l ⊔ lsuc m)
... | ∃i (C , D) w = match (w E p sp) (\ where
  (∃i c (∃i e q)) →
    let
       C' : Set l
       C' = ∑ z ∶ D c , π₁ (el (π₂ (e z)))
       D' : C' → Set l
       D' u  = π₂ (el (π₂ (e (π₁ u)))) (π₂ u)
       w' : (a : A) → wisc (B a) (C' , D') m
       w' a X g gs = match (q a) (\ where
         (∃i z refl) → match (pf (π₂ (e z)) X g gs) (\ where
           (∃i y (∃i h hs)) →
             ∃i (z , y) ((∃i {P = λ f → surjection (g ∘ f)} h hs))))
    in
    ∃i (C' , D') w')
  where
  E : Set (lsuc l ⊔ lsuc m)
  E = ∑ x ∶ A , set F ∶ Fam l , wisc (B x) F m
  p : E → A
  p = π₁
  sp : surjection p
  sp a with WISC (B a) m
  ... | ∃i F w = ∃i (a , (F ∣ w)) refl