-- Whirlwind tour to forcing :-)
-- (Invented by Paul Cohen in 1963, got the Fields Medal.)

{-
  In algebra and analysis, we are accustomed to extending
  mathematical structures:
  -- ℚ has holes, hence pass to ℝ.
     Every real number is a limit of better and better approximations
     by rational numbers: 3, 3.1, 3.14, ...
  -- ℝ doesn't contain a square root of -1, hence pass to ℂ
     (note: ℝ ∪ { i } is also a nice set, but not a field)
  -- From ℂ, pass to ℂ[X] which contains the new "generic number" X
  -- ...

  In set theory, we extend the base mathematical universe.
  The extended universes are called forcing extensions of the
  base universe.
  -- There is a forcing extension containing a new function ℕ → ℕ,
     the so-called "generic function ℕ → ℕ".
  -- There is a forcing extension containing a new set X.
  -- There is a forcing extension containing a new maximal ideal
     for a given commutative ring.
  -- There is a forcing extension containing a new surjection ℕ → X,
     the so-called "generic surjection ℕ → X". This construction
     works and is nontrivial and has applications for any inhabited set X
     of the base universe (including uncountable sets).
-}

module _ (X : Set) (x₀ : X) where
-- "Let a set X be given. Let an element x₀ be given."

-- What should an approximation to a surjection ℕ → X be?
-- Answer: Finite lists of elements of X.
-- For instance the finite list a ∷ b ∷ c ∷ [] can be regarded
-- as the following partially-defined partially-surjective function f : ℕ → X:
-- f zero = a
-- f one  = b
-- f two  = c

-- Over time, approximations may evolve to better approximations.

-- Let "f₀ : ℕ → X" be our name for the generic surjection living in
-- the forcing extension. Unfortunately, Agda does not support a "forcing mode"
-- by which we could switch to the forcing extension. In the forcing extension,
-- f₀ would be an actual function, and given n : ℕ and an element x : X,
-- the assertion "f₀ n ≡ x" would be an ordinary assertion.

-- Instead, we need to use the language of the base universe to talk about
-- the forcing extension.

open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProgrammingBasics.Naturals.Base

L : Set
L = List X
-- the type of approximations

-- Let us now define "f₀ n ≡ x". We will write this as "f₀[ n ]≡ x".
f₀[_]≡_ : ℕ → X → (L → Set)
f₀[ n ]≡ x = λ xs → {!...the n'th element in the list xs is equal to x....!}

-- Given an approximation-depending proposition P : L → Set,
-- ∇ P xs will express the following: "No matter how xs evolves over time to
-- a better approximation ys, eventually P ys will hold."
data ∇ (P : L → Set) : L → Set where
  now    : {xs : L} → P xs → ∇ P xs
  later₁ : {xs : L} → ((x : X) → ∇ P (xs ∷ʳ x)) → ∇ P xs
  later₂ : {xs : L} → (y : X)
    → ((ys : L) → {!...y occurs somewhere in xs ++ ys.....!} → ∇ P (xs ++ ys)) → ∇ P xs