-- Limitations of Standard Agda (and also of standard MLTT):
-- 1. We don't have function extensionality.
-- 2. We don't have effective quotients.
-- 3. The equality type is underspecified.
-- 4. We cannot express mere existence (and hence also not the axiom of choice).
-- 5. We only have zero-dimensional types available, not higher-dimensional ones.
--
-- Amazingly, all of these limitations are resolved by Cubical Agda (or
-- Cubical Type Theory or Homotopy Type Theory), where we embrace
-- higher-dimensional types (like the one-dimensional circle, or
-- the two-dimensional sphere, or even higher-dimensional types).

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base


------ Issue 1

example₁ : Bool → Bool
example₁ x = x

example₂ : Bool → Bool
example₂ false = false
example₂ true  = true

example₃ : Bool → Bool
example₃ false = false
example₃ true  = true

lemma₁₂ : (x : Bool) → example₁ x ≡ example₂ x
lemma₁₂ false = refl
lemma₁₂ true  = refl

lemma₂₃ : (x : Bool) → example₂ x ≡ example₃ x
lemma₂₃ false = refl
lemma₂₃ true  = refl

-- So far so good. However, the following holes can NOT be filled in Standard Agda.
theorem₁₂ : example₁ ≡ example₂
theorem₁₂ = {!!}

theorem₂₃ : example₂ ≡ example₃
theorem₂₃ = {!!}

-- Standard Agda is lacking function extensionality. This is the following
-- principle:

postulate
  funext : {A B : Set} → {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
  -- "If two functions have the same values, then they are the same."

-- But take care: Postulates destroy normalization!
-- Without postulates, any term of type x ≡ y evaluates to refl.
-- With postulates, this can fail.

does-not-reduce-to-refl : example₁ ≡ example₂
does-not-reduce-to-refl = funext lemma₁₂

does-not-reduce-to-a-numeral : ℕ
does-not-reduce-to-a-numeral = check does-not-reduce-to-refl
  where
  check : {g : Bool → Bool} → example₁ ≡ g → ℕ
  check refl = zero

-- Milly's minimalist foundation has the premise that function extensionality
-- is great to have but hard to get. Hence her foundation operations on two levels.
-- On the upper level, we have function extensionality. This level is the level
-- which mathematicans are invited to use.
-- The upper level is compiled down to the lower level, which does not have
-- function extensionality (but then lots of other good type-theoretic properties
-- like decidability of type checking and strong normalization).


------ Issue 3

-- Gödel's incompleteness theorem states that every (reasonable) consistent
-- formal system is incomplete in that there are statements which are neither
-- provable nor refutable using that system.

-- Every provable statement is true, but there are true statements which
-- are not provable (in a given system).

-- Luckily, for many formal systems, this incompletenes phenomenon only
-- surfaces with slightly more advanced examples. But in Standard Agda,
-- we hit these issues already quite early:

-- We can neither prove nor refute the claim example₁ ≡ example₂.
-- The claim "example₁ ≡ example₂" is independent of Standard Agda (or of MLTT,
-- Martin-Löf type theory).


------ Issue 4

{-
  The axiom of choice can be phrased in several equivalent terms:
  1. For every set M of sets, if ∀a∈M ∃b∈a ⊤, then ∃f : M → ???. ∀a∈M. f(a) ∈ a.
     "For every set of inhabites sets, there is a choice function."
     (Example, NOT requiring the axiom of choice. Let M = the set of cities
     on earth. Then one possible choice function would be f(a) = the mayer of a.
     Another choice function is f(a) = the youngest person in a. Note that
     the following attempt does NOT define a function: "g(a) = some random
     inhabitant of a". This alleged function does not always return the
     same outputs on the same inputs. On one day, g(Padova) might be Milly,
     and on some other day g(Padova) might be Giovanni.
   2. (∀x∈P ∃y. A(x,y)) ⇒ (∃f:P→???. ∀x∈P. A(x,f(x)))
   3. For every surjection f : A → B, there is a map g : B → A such that
      f(g(x)) = x for all x ∈ B. "Every surjection splits."
-}

data ⊤ : Set where
  tt : ⊤

-- The following statement refers to a family of inhabited types,
-- namely the family of types called "P a", where a varies over the elements of I.
kinda-looking-like-the-axiom-of-choice
  : {I : Set} {P : I → Set}
  → ((a : I) → Σ[ x ∈ P a ] ⊤)    -- "all the types P a are inhabited"
  → Σ[ f ∈ ((a : I) → P a) ] ⊤    -- "there is a choice function"
kinda-looking-like-the-axiom-of-choice p = (λ a → fst (p a)) , tt

-- We have defined the type "Σ[ x ∈ A ] B x" of witnesses that there is
-- some element x : A such that B x. According to our definition, such
-- a witness is a pair (x , p) consisting of
-- - an element x : A and
-- - a witness p : B x.
-- From such a pair we can always extract its first component.
--
-- So a witness of type "Σ[ x ∈ A ] B x" does not only attest the fact
-- that there is an element x : A such that B x; instead, moreover, it
-- also supplies one possible such element x.
--
-- So our Σ expresses "specified existence", not "mere existence".
-- In Standard Agda, we cannot express mere existence.
-- In Standard Agda, we cannot squash types:
-- Given a type X, we would like to have a type ∥ X ∥ which contains
-- at most one element. More precisely, the type ∥ X ∥ should contain
-- an element if and only if X is inhabited. But an element of ∥ X ∥
-- should not disclose a particular value of X. An element of ∥ X ∥
-- should just be a witness that X is inhabited.

-- ∥ X ∥ should be a "proof-irrelevant" version of X.
-- We would the following three lines of code to work, but in Standard Agda
-- they don't.
{-
data ∥_∥ (X : Set) : Set where
  c     : X → ∥ X ∥
  trunc : (a b : ∥ X ∥) → a ≡ b
-}
-- For instance, if X contains the values p, q and r,
-- then ∥ X ∥ contains the values "c p", "c q" and "c r".
-- But these three values are all the same. So we achieve the goal that
-- an element of ∥ X ∥ does not disclose a specific value of X.

-- With squash types at hand, we can express mere existence as follows:
-- "there merely exists an element a : A such that B a" = ∥ Σ[ x ∈ A ] B a ∥

{-
the-actual-axiom-of-choice
  : {I : Set} {P : I → Set}
  → ((a : I) → ∥ Σ[ x ∈ P a ] ⊤ ∥)    -- "all the types P a are merely inhabited"
  → ∥ Σ[ f ∈ ((a : I) → P a) ] ⊤ ∥    -- "there merely is a choice function"
the-actual-axiom-of-choice p = ?  -- not provable without postulated
-}

{-
  Five fun facts about the axiom of choice (AC):
  1. AC ⇒ LEM. The axiom of choice implies the law of excluded middle.
  2. The axiom of choice can be used to concoct several mathematical monsters,
     like a subset of ℝ² which is so weird that any attempt to specify an area
     of this subset fails (including the attempt "the area is zero" or
     the attempt "the area is infinite").
  3. The axiom of choice can be safely contained in Gödel's sandbox
     ("Gödel's L").
  4. Many concrete consequences of the axiom of choice hold even if the
     axiom of choice is not available. But for many more abstract results
     (especially results of an infrastructural nature), we can prove
     that the axiom of choice is required.
  5. In a certain fun logic puzzle, the dwarves have a winning strategy
     against the evil monster if and only if the axiom of choice holds.
-}




{-
  Construction of the cumulative hierarchy:

      V₀ ≔ {}
      V₁ ≔ P(V₀) = { {} }
      V₂ ≔ P(V₁)
      ⋮
      V_ω ≔ V₀ ∪ V₁ ∪ V₂ ∪ ...
      V_{ω+1} ≔ P(V_ω)
      V_{ω+2} ≔ P(V_{ω+1})
      ⋮

  Finally, set V ≔ ⋃_α V_α.
  Fun fact: Every set is contained in one of the V_α's.
 
  Construction of Gödel's sandbox:

      L₀ ≔ {}
      L₁ ≔ P'(L₀) = { {} }
      L₂ ≔ P'(L₁)
      ⋮
      L_ω ≔ L₀ ∪ L₁ ∪ L₂ ∪ ...
      L_{ω+1} ≔ P'(L_ω)
      L_{ω+2} ≔ P'(L_{ω+1})
      ⋮

  Finally, set L ≔ ⋃_α L_α.

  Recall: P(X) = the set of all subsets of X.
          P'(X) = the set of those subsets of X, which are definable using a formula
                  on set theory with parameters from X.

  For instance, { n ∈ ℕ | n is prime } ∈ P'(ℕ).

  The axiom of choice holds in L roughly for the following reason:

     Given an inhabited set in L from which we would like to pick an element,
     we can just pick the unique element with the shortest definition.
     (In case there are several elements with the same shortest length of definition,
     we pick the element with the definition which lexicographically comes first.)
-}

data Formula : Set where
  top : Formula
  bot : Formula
  _∧_ : Formula → Formula → Formula
  _∨_ : Formula → Formula → Formula
  -- a couple more

-- It is possible, in mathematical Italian, in Agda, in ZFC to talk about
-- ZFC, ZF, CZF, the axiom of choice, provability, unprovability, ...

-- In particular, we could define in Agda what ZFC is and what ZF is, and then prove:
-- Every ZFC-proof on an arithmetical statement can be transformed into a ZF-proof of
-- the same statement.

-- \bN \alpha \_3
-- If Vi-mode is enabled (using C-z), then: C-k a *,  C-k 3 s