```
{-# OPTIONS --safe --without-K #-} -- checked in Agda 2.6.0.1
module EnlightenmentEscalator where
```
ℾ We use manipulation of Cantor-bitstrings inspired by Martin Escardo "Seemingly Impossible"
ℾ    to investigate diagonalization, provability, and infinity. Thanks and credit for sharing code.
∙ http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
∙ https://www.cs.bham.ac.uk/~mhe/ for more recent work including many Agda proofs.
Cantor diagonal proof based on https://www.playingwithpointers.com/blog/agda-cantor.html by Sanjoy Das.
Text , new code (¬ math) © Mycroftiv, No-Coercion license. Dedicated to everyone looking for 1 ■ of freedom.
```
open import Agda.Primitive
-- ∙ import Measurable∞→↘               ↓↓↓↓↓↓↓↓↓↓↓         ↓↓↓         ↓↓↓ 
open import Agda.Builtin.Bool renaming (Bool to Bit; true to ; false to ) -- ◃ Bool renamed Bit ▹
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma renaming (fst to proj₁; snd to proj₂)
open import Agda.Builtin.List
open import Agda.Builtin.Unit
-- ∙ import TypeSet.MultiVerse

data  : Set where
⊥-elim :  {w} {Whatever : Set w}    Whatever
⊥-elim ()
¬_ :  {}  Set   Set 
¬ P = P  
contradiction :  {α β} {A : Set α} {B : Set β}  A  ¬ A  B
contradiction a b = ⊥-elim (b a)
pred : Nat  Nat
pred zero = zero
pred (suc n) = n

```
 ∙ Outline ∙ We rename the Boolean type to Bit and represent true as ■ and false as □.
 Nat → Bit functions represent Cantor bitstrings to code sets of Naturals fulfilling predicates.
 We create Ω orderings where the y-index matches the cardinality of bits in the corresponding Cantor.
 We show the diagonalization against the > predicate produces a Cantor coding the set of all Nats.
 In other words, we diagonalize a function-generation system that produces finite quantities
   and produce a function which produces infinity. We diagonalize finite Nat-sets to ℵ₀.
```
bitflip : Bit  Bit
bitflip  =  
bitflip  = 

Cantor : Set
Cantor = Nat  Bit

Ω : Set
Ω = Nat  Cantor

data Cantors-differ (a b : Cantor) : Set where
  differ-at : (n : Nat)  ¬ (a n  b n)  Cantors-differ a b

data NotListedIn (𝕆 : Ω)  (r : Cantor) : Set where
  not-listed : ((n : Nat)  Cantors-differ (𝕆 n) r)  NotListedIn 𝕆 r

invert : Ω  Cantor
invert 𝕆 = λ n  bitflip (𝕆 n n)

flip-≠ : (b : Bit)  ¬ (b  bitflip b)
flip-≠  ()
flip-≠  ()
```
 ∙ 0⋆ Diagonalizer of Nat → Cantor mappings.
 ∙ The diagonalizer takes a function which generates a Cantor bitstring for each Nat.
 This is an ordered list of cantors indexed by Nat, and diagonalizes to find a new Cantor
   which is not on the list - not in the image of the function.
 This is always possible because the cardinality of possible Cantor bitstrings is the same
   as the reals, uncountable, so there is no bijection with the Nats that index the list.
```
cantor-➘ : (𝕆 : Ω)  Σ Cantor (NotListedIn 𝕆) 
cantor-➘ 𝕆 = (invert 𝕆) , not-listed λ n  differ-at n (flip-≠ (𝕆 n n))
```
 Tools we need for Cantor constructions. Conversions, comparisons, collections.
```
--bit-to-truth : Bit → Set
--bit-to-truth □ = ⊥
--bit-to-truth ■ = ⊤

_>_ : Nat  Nat  Bit
x > y = y < x

T■ : Bit  Set
T■   = 
T■  = 

_in-c_ : Nat  Cantor  Set
n in-c c = T■ (c n)
```
 Two functions to examine Cantors as bitstrings and sets of Naturals, and an example Cantor :
```
_bits_ : Nat  Cantor  List Bit
zero bits c = []
suc n bits c = (c n)  (n bits c)

nbits-as-nats : Nat  Cantor  List Nat
nbits-as-nats zero c = []
nbits-as-nats (suc n) c with c n
nbits-as-nats (suc n) c |  = nbits-as-nats n c
nbits-as-nats (suc n) c |  = n  (nbits-as-nats n c)

odd-nats : Cantor
odd-nats zero = 
odd-nats (suc zero) = 
odd-nats (suc (suc n)) = odd-nats n
```
 10 bits odd-nats -- ■ ∷ □ ∷ ■ ∷ □ ∷ ■ ∷ □ ∷ ■ ∷ □ ∷ ■ ∷ □ ∷ []
 nbits-as-nats 10 odd-nats -- 9 ∷ 7 ∷ 5 ∷ 3 ∷ 1 ∷ []
 5 in-c odd-nats -- ⊤ | 6 in-c odd-nats -- ⊥

 We define a special type of bitstring which is n consecutive ■ bits followed by all □ :
```
cardinality-of : Ω
cardinality-of zero x₁ = 
cardinality-of (suc y) zero = 
cardinality-of (suc y) (suc x₁) = cardinality-of y x₁
```
 10 bits cardinality-of 5 -- □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ []
 nbits-as-nats 10 (cardinality-of 5) -- 4 ∷ 3 ∷ 2 ∷ 1 ∷ 0 ∷ []
 5 in-c (cardinality-of 5) -- ⊥
 We name this Ω order the 'y-index' of bitstrings, it maps the cardinality of Nats into equal number of ■ ■ ■.
 We have an ordering scheme which we expect to enumerate all cardinalities of sets of naturals.
 However, visualizing the ordering as list/grid of values reveals it can be diagonalized against.
```
missing-bitstring : Σ Cantor (NotListedIn cardinality-of)
missing-bitstring = cantor-➘ cardinality-of

diagonalization : Cantor
diagonalization = proj₁ missing-bitstring
```
 We will return to examine this first diagonalization.
 We now construct another set of Cantors, encoding a predicate relationship.
 First, a trivial lemma:
```
suc-⊤>-n :  (n : Nat)  T■ (suc n > n)
suc-⊤>-n zero = tt
suc-⊤>-n (suc n) = suc-⊤>-n n
```
 We create a predicate representing ∞ expressed as the possibility to provide y > n for any n.
```
Σx-⊤>-n :  (n : Nat)  Σ Nat  y  T■ (y > n))
Σx-⊤>-n n = (suc n) , suc-⊤>-n n

translate-Σx>n :  (n : Nat)  Σ Nat  y  T■ (y > n))  Cantor
translate-Σx>n n (fst , snd) = λ y  fst > suc y

y->-n : Ω
y->-n y = translate-Σx>n y (Σx-⊤>-n y)
```
 ∙ 1⋆ y->-n produces an X/Y grid of T/F (■/□) values for y > x, the rows are Nat → Cantor bitstrings.
 ∙ We aren't trying to list all Cantors in the first place, so what is the motive to diagonalize?
 Diagonalization in this context finds a set of possibilities which were not enumerated by the
   Ω ordering which provides a map of the truth value of the indexed predicate at n.
 Our construction correlates encodings of numbers via inductive 'suc' and bitstring-collections.
 We construct a grid which seems like a full map of truth about these numbers under the y > x relationship.
 What can diagonalization show us that Σxists, but is not captured by our map of subject-predicate relations?
```
fixpoint-> : Σ Cantor (NotListedIn y->-n)
fixpoint-> = cantor-➘ y->-n
```
 The y-axis of increasing y generates an infinite series of increasing cardinalities.
 The x-axis of increasing x generates an infinite series of increasing >-than predicates.
 It seems like this should be a comprehensive map of truth about the Nats under > relation,
   but we can still diagonalize to find a possibility not captured in this map.
```
diagonalization' : Cantor
diagonalization' = proj₁ fixpoint->
```
 We learned from our 'translate' function that any boolean relation of Nats is an Ω Cantor-generator.
 Now that we have seen this equivalence, we construct our target object more directly :
```
ladder-to-∞ : Σ Cantor (NotListedIn _>_)
ladder-to-∞ = cantor-➘ _>_
```
 ∙ 2⋆ Semiotic interpretation. What is the meaning of this predicate diagonalization?
 ∙ We are comparing a set of predicates with a rule for generating an object which encodes what
     members of the set of objects fulfill the predicate. We are mapping the elements of the set being
     quantified over to a particular list of what objects do or don't fulfill the predicate.
 The particular map of possibilities generated by the x > y predicate has a notable structural
   characteristic, where there is a clear relationship between the structure of the bitstring
   and the concept of cardinality that the correlated y-index represents.
 It is this higher, meaning-signification level of interpretation of the structure of the bitstring
   and the correlated index Nat which produces the level-lift from finite to infinite cardinalities.
```
ℵ₀ : Cantor
ℵ₀ = proj₁ ladder-to-∞
```
 >9  >8  >7  >6  >5  >4  >3  >2  >1  >0 ⇙⇙Diag
  □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ [] 0    10 bits (y->-n 0) 0 is greater than 0 Nats
  □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ [] 1    10 bits (y->-n 1) 1 is greater than 1 Nat (0)
  □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ [] 2    10 bits (y->-n 2) 2 is greater than 2 Nats (0,1)
  □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ [] 3    10 bits (y->-n 3) 3 is greater than 3 Nats (0,1,2)
  □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ [] 4    10 bits (y->-n 4) ...
  □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ [] 5    10 bits (y->-n 5) ...
  □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ [] 6    10 bits (y->-n 6) ...
  □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ [] 7    10 bits (y->-n 7) ...

 ∙ 3⋆ Construction details.
 ∙ Each Nat along the x axis generates a predicate.
 ∙ Each Nat on the y axis generates a Cantor bitstring.
 ∙ The Cantor bitstrings map the truth of Nat-y relative to predicate-x.
 The Cantor generator used for the > predicate creates a structural correspondence between Cantors and Nats.
 The cantor at y0 = 000 , at y1 = 100 , at y2 = 110 , y3 = 111 , the number of 1 bits == y.
 So we have what seems like a tight and comprehensive mapping, but diagonalization shows what was left out.
 The Cantor bitstrings in this mapping encode the relation between cardinality and predicate fulfillment.
 Nat y-7 generates a Cantor bitstring with the first 7 bits active, showing that 7 fulfills >0...>6,
   and also that the cardinality of the collection of its 1-bits is the same as its y-index position.
 The diagonalization raises us to the level of infinite cardinality.
 The Nat corresponding to 1111... by bit-count rule is not actually a Nat if the 111... never stops.
 'The cardinality of the set of all Nats is > than any Nat' is expressed by it as a collection.
 The diagonalization doesn't produce an unlisted Nat - it produces an unlisted set of Nats.
 The y-indexed Cantor bitstring production rule only produces sets of 111... with Nat-cardinality,
   but the diagonalization produces an infinite cardinality set which fulfills the predicates the same way.
 Put another way - our production rule will generate as long a sequence of 11111 as we want, but it won't
   generate an actual infinite collection. The function produced at every y-index to generate bitstrings
   always stops at y. Diagonalizing against this under the > predicate gives us the fixpoint of
   the > x comparison - the infinite set of every positive integer, as represented by the all-1 bitstring.
____________________________________________________________________________________________________________
 The direct expression of 'the set of all Naturals' as a Cantor - for each Nat, its ■ is true-exists.
```
∀-nat : Cantor
∀-nat n = 

set-of-all-n :  (n : Nat)  ∀-nat n  
set-of-all-n n = refl

diag-is-∞-is-∀-n :  (n : Nat)  diagonalization n  ∀-nat n
diag-is-∞-is-∀-n zero = refl
diag-is-∞-is-∀-n (suc n) =  diag-is-∞-is-∀-n n

diag'-is-∞-is-∀-n :  (n : Nat)  diagonalization' n  ∀-nat n
diag'-is-∞-is-∀-n zero = refl
diag'-is-∞-is-∀-n (suc n) =  diag'-is-∞-is-∀-n n

ℵ₀-is-∀n∈ℕ :  (n : Nat)  ℵ₀ n  ∀-nat n
ℵ₀-is-∀n∈ℕ zero = refl
ℵ₀-is-∀n∈ℕ (suc n) = ℵ₀-is-∀n∈ℕ n
```
 ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ ■ ∷ [] -- 17 bits ℵ₀
 ∎ All of our diagonal objects are the same object, the infinite set of all Naturals.
 ∎ Diagonalization has raised us from the infinite sequence of finite ordinals/cardinals
   to the first infinite cardinal, the countable infinity of the set of all Nats.
 The following proofs are organized on a theme of showing similarities and differences
   between the infinite list of all finite cardinalities, and the first infinite cardinality.
```
infinite-starts-finite :  (y : Nat)  ℵ₀ y  y->-n (suc y) y
infinite-starts-finite zero = refl
infinite-starts-finite (suc n) = infinite-starts-finite n

y->-n-isnt-infinity :  (y : Nat)  ¬ (y->-n y y  (ℵ₀ y))
y->-n-isnt-infinity (suc y) x = y->-n-isnt-infinity y x
```
 In the proof below, we create a hand-made version of the cantor-➘ operation,
   where we use the ℵ₀ witness generated from ladder-to-∞, and a newer proof object,
   to demonstrate the unity of our generated knowledge of these objects.
```
ℵ₀-differs-from-arbitrarily-large : Σ Cantor (NotListedIn y->-n)
ℵ₀-differs-from-arbitrarily-large = ℵ₀ , not-listed λ y  differ-at y (y->-n-isnt-infinity y)

∀m>n-∈ℵ₀ :  (m n : Nat)  T■ (m > n)  (m in-c ℵ₀)
∀m>n-∈ℵ₀ (suc zero) zero tt = tt
∀m>n-∈ℵ₀ (suc (suc m)) zero tt = ∀m>n-∈ℵ₀ (suc m) zero tt
∀m>n-∈ℵ₀ (suc (suc m)) (suc n) x = ∀m>n-∈ℵ₀ (suc m) n x
```
 The above in comparison to the following captures the difference in cardinalities.
 Since n can take any value, y->-n n stands for the entire universe of truth in its Ω.
```
m>n-∉-y->-n :  (m n : Nat)  T■ (m > n)  ¬ (m in-c (y->-n n))
m>n-∉-y->-n  (suc m) zero tt ()
m>n-∉-y->-n  (suc m) (suc n) x x₁ = m>n-∉-y->-n  m n x x₁
```
 The following proofs trace the following similarities and disjunctions :
 ∙ The successor of a number is never present in that number's cardinality-Cantor.
 ∙ The successor of a number is always present in the ℵ₀ set of all Nats.
 ∙ Every number is a member of its successor's cardinality-Cantor.
 ∙ No number is a member of its own cardinality-Cantor.
 ∙ Every number is a member of ℵ₀.
```
sucy-∉-y>n-y :  (y : Nat)  ¬ ((suc y) in-c (y->-n y))
sucy-∉-y>n-y y x = contradiction x (m>n-∉-y->-n (suc y) y (suc-⊤>-n y))

sucn-∈-ℵ₀ :  (n : Nat)  ((suc n) in-c ℵ₀)
sucn-∈-ℵ₀ zero = tt
sucn-∈-ℵ₀ (suc n) = sucn-∈-ℵ₀ n

y-∈-y>n-sucn :  (y : Nat)  (y->-n (suc y)) y  
y-∈-y>n-sucn zero = refl
y-∈-y>n-sucn (suc y) = y-∈-y>n-sucn y

y-∉-y>n-y :  (y : Nat)  (y->-n y) y  
y-∉-y>n-y zero = refl
y-∉-y>n-y (suc y) = y-∉-y>n-y y

n-∈-ℵ₀ :  (n : Nat)  ℵ₀ n  
n-∈-ℵ₀ zero = refl
n-∈-ℵ₀ (suc n) = n-∈-ℵ₀ n
```
∙ 4⋆ An ordering-relation data object to compare cardinal-form Cantor bitstrings.
∙ With the above proofs and our understanding of the relation between ordinality and cardinality,
   we can encode proofs of the numeric interpretation of cardinal-Cantors in a data structure.
 This data object holds proof of an ordering relation between cardinal-variety Cantors.
 Note that the comparison here is not total across bitstrings, only cardinal-form bitstrings.
 Given cardinal-form, a single position bit difference proves this ordering relationship.
```
data _∞>_ (c : Cantor) (d : Cantor) : Set where
  _shows_is-greater-cardinality-than_ : (n : Nat)  c n    d n    c ∞> d
```
 With this data object we can establish the visually clear but not previously proved correspondence
   between our concepts of ordinality, cardinality, Ω orderings, and our diagonally generated ℵ₀.
```
cardinality-increases-with-y :  (y : Nat)  (y->-n (suc y)) ∞> (y->-n y)
cardinality-increases-with-y y = y shows (y-∈-y>n-sucn y) is-greater-cardinality-than (y-∉-y>n-y y)

ℵ₀-∞>-∀y->-n :  (y : Nat)  ℵ₀ ∞> y->-n y
ℵ₀-∞>-∀y->-n y = y shows (n-∈-ℵ₀ y) is-greater-cardinality-than (y-∉-y>n-y y)
```
 ∎ ∃ ℵ₀ ∈ Cardinalities { ∀ n ∈ Nat | ℵ₀ > Cardinality n }
 ∎ We began with only the possibility of infinity inherent in the definition of a Cantor bitstring.
 ∎ We used induction to build a potential-infinity of as-large-as-we-want cardinalities.
 ∎ Viewing this structure as a map of predicate relations opens the possibility of diagonalization.
 ∎ The diagonalization of the ordering of cardinality-producing functions produced a new possibility,
     a new function which corresponds to a cardinality which transcends potential-infinity.
 ∎ The ℵ₀ Cantor is a completed infinite set of all the Naturals, produced by a diagonalization
     of the Ω ordering list of the cardinality of each Natural.

 The y-index enumeration of cardinalities never reaches the cardinality of its diagonalization.
 We have reflected downward the diagonal argument, using it to produce a countable infinity,
   in relation to an unending progression of increasing yet always finite cardinalities.
 Note that this kind of level-crossing will not be apparent in all diagonalizations.
 The > relation and Cantor bitstring production rule were chosen for this structural property.
 Diagonalization creates more structure than just finding an unlisted possibility - the method by
   which it produces a witness to its existential claim can be exploited to produce interesting objects.

 The feeling of mind-vertigo often induced by these proofs is the step-up of signification involved in
   comparing the behavior of collections with single objects where the collections have a structure
   which encodes about-ness by using information about the objects to specify their production rule.
 Cantor bitstrings can encode about-ness in relation to the Naturals in multiple ways.
 There is a precise correspondence between which bits are ■ and a set of Nats fulfilling a Σ predicate.
 There are also multiple ways to encode single Nats in Cantors, such as the simple bitcount used here.

 The Cantor bitstrings are the logical-reals and correspond to 2-colored binary hypercubic graphs of 2^n,
   where n is the number of digits necessary to capture their behavior. A full Cantor is the infinite graph.
 The universe of truth is continuously increasing the size of its powerset by adding more information,
   each bit of which acts as a new vertex for the binary hypercube and increments the n exponent.
 The deep logical structure of reality and existence is a continuously expanding transfinite binary hypercube
   in which each single bit of new information widens the scope of the whole by a 2^n multiplication
   of the possibility space. With each new communication-partner bit of boolean possibility the universe ↻⟳↻.

 We have shown that the Cantor bitstrings generated by the y-index are all finite and do not grow past n.
 In contrast, Nat-value of the diagonalization bitstring will continue to grow as you examine additional bits.
 This captures the difference in cardinality between the 'set of all Nats' and 'a set as large as any n'.
 The > predicate relationship on the Nats as a generator of cardinality can produce arbitrarily large
   but finite cardinalities. The diagonalization all-1 bitstring captures the cardinality of ℵ₀.

 Examples and probes.
```
c-ex1 : List Bit
c-ex1 = 9 bits (cardinality-of 3)
c-ex2 : List Nat
c-ex2 = nbits-as-nats 9 (cardinality-of 3)

is-card : Nat  Cantor  Set
is-card zero c = 
is-card (suc n) c with c n
is-card (suc n) c |  = 
is-card (suc n) c |  = is-card n c

∀-nat-is-card :  y  is-card y (∀-nat)
∀-nat-is-card zero = tt
∀-nat-is-card (suc y) = ∀-nat-is-card y

c-bitsum : Nat  Cantor  Nat
c-bitsum n c with c n
c-bitsum zero c |  = 0
c-bitsum zero c |  = 1
c-bitsum (suc n) c |  = 0 + (c-bitsum n c)
c-bitsum (suc n) c |  = 1 + (c-bitsum n c)

card-val : Nat  Nat
card-val y = c-bitsum y (cardinality-of y)

y->-n-val : Nat  Nat
y->-n-val y = c-bitsum y (y->-n y)

test1 : is-card 9 (y->-n 9)  
test1 = refl
test2 : y->-n-val 9  9
test2 = refl
test3 : y->-n-val 9  (c-bitsum (9 + 5) (y->-n 9))
test3 = refl
```
 The above tools are sanity checks to make sure that our Cantor-cardinals are behaving properly.
 The following assertions are probably easy to prove, but are less trivial than the other proofs,
 precisely because the mapping between Cantor-bitstring cardinality and the Naturals is
 very obvious to the human eye but less trivial from the viewpoint of Agda.
```
-- postulate card-is-card : ∀ (n : Nat) → (is-card n (cardinality-of n))
-- postulate card-val-n≡n : ∀ (n : Nat) → card-val n ≡ n
-- postulate cval-n-ends-at-n : ∀ (n : Nat) → (card-val n) ≡ (c-bitsum (suc n) (cardinality-of n))
-- postulate gen-cval : ∀ (m n : Nat) → (card-val m) ≡ (c-bitsum (m + n) (cardinality-of m))
-- postulate y->-nvaln≡n : ∀ (n : Nat) → (y->-n-val n ≡ n)
```
 We might as well make a nice ∞ object that actually holds 'all the numbers' and will provide us
   with as many as we want on demand. This sets up an enjoyably notated demonstration object.
```
 : Nat  List Nat
 n = nbits-as-nats n ℵ₀

∞8 : List Nat
∞8 =  8
```
Predicate diagonalization in general - consider the following chart of bird colors:

     predicate: is-red? is-blue? is-green?
Bird:
reddy            ■        □       □
bluey            □        ■       □
greeny           □        □       ■
If we diagonalize against this mapping of birds and corresponding predicates we get □ □ □.
This string proposes the possible existence of a bird which is neither red nor blue nor green.

We can also consider a similar set of relationships:

         predicate: has-red has-blue has-green
bird-sets:
0-nobirds            □       □        □
1-blue               □       ■        □
2-red+blue           ■       ■        □

In this case we have a correspondence between sets of birds and predicates describing their
membership in a particular set. We diagonalize to ■ □ ■ and this is an example of a possible
set of birds (2 birds, red+green) which was not included in our list of of possible sets
generated by the set-production function indexed by the naturals.

How are these examples actually the same? In the first we considered each bird as a set of properties
and in the second we considered sets of birds containing birds with the defined properties.

The diagonalization in the first case produced a hypothetical bird with some un-enumerated combination
of properties. In the second case, we produce a possible set-of-birds not enumerated in the truth-map.

Note also the implicit rules these charts follow. In the first, the sequence of bird-colors was
matched against the color-predicates, and in the second, the numerical index corresponded to
the number of birds in the set. Turning our attention back to the bitstring example:

   predicate: >0  >1  >2  >3  >4
Nat
0              □   □   □   □   □
1              ■   □   □   □   □
2              ■   ■   □   □   □
3              ■   ■   ■   □   □
4              ■   ■   ■   ■   □
5              ■   ■   ■   ■   ■

10 bits (3 >_)
 □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ □ ∷ ■ ∷ ■ ∷ ■ ∷ []
 9   8   7   6   5   4   3   2   1   0

This truth map has correspondences not present in the bird examples, as well as being infinite.
The key feature is that at each y-index, the cardinality of the set of fulfilled predicates is == y.
Thus we are encouraged to take the conceptual step to regard each line of the chart as a very direct and
literal representation of the idea of quantity that corresponds closely to the natural numbers.
We see the bitstrings generated by the rule which describes the > predicate as the moral equivalent of Nats.
The diagonalization produces a bitstring that has not just an arbitrarily large collection of ■,
but the complete collection, the cardinality of the collection of all numbers rather than an arbitrarily
large finite subset. When this construction is revealed, we see the Nats diagonalized upward to infinity.
____________________________________________________________________________________________________________
 More miscellaneous tools to investigate the behavior of bitstrings/cardinalities.
 ∙ Two versions of comparison for Cantor-cardinals, one recursive, one single-bit.
```
C> : Nat  Cantor  Cantor  Bit
C> n c d with c n | d n
C> zero c d |  |  = 
C> zero c d |  |  = 
C> zero c d |  |  = 
C> zero c d |  |  = 
C> (suc n) c d |  |  = C> n c d
C> (suc n) c d |  |  = 
C> (suc n) c d |  |  = 
C> (suc n) c d |  |  = 

Cn> : Nat  Cantor  Cantor  Bit
Cn> n c d with c n | d n
Cn> n c d |  |  = 
Cn> n c d |  |  = 
Cn> n c d |  |  = 
Cn> n c d |  |  = 
```
 The above comparison tools are another way to verify behavior of Cantor-cardinal bitstrings.
 Any cardinal-form bitstrings should yield the expected results under these operations.
```
Cex : Nat  Bit
Cex n = C> n (y->-n (suc n)) (y->-n n)

¬Cex : Nat  Bit 
¬Cex n = C> n (y->-n n) (y->-n (suc n))

Cnex : Nat  Bit
Cnex n = Cn> n (y->-n (suc n)) (y->-n n)

Cnprf : Nat  Bit
Cnprf n = Cn> n ℵ₀ (y->-n n)
```
 We can make a 'provably cardinal-form' data object based on our ℵ₀ or other suitable Cantor.
 After initializing with the corresponding Nats and the object identity, we step forward and
   store proofs at each stage that the Cantor is correctly filling in all bits.
 In combination with previous results, the totality of the 'mkcard' function establishes that
   not only our ℵ₀ object, but our Ω orderings as proven in 'infinite-starts-finite' are
   capturing the idea of cardinality we want, a tight correspondence with the sequence of Nats.
```
data Card (n : Nat) (c : Cantor) : Set where
  czero : n  0  c  c  Card n c
  cone : Card 0 c  n  1  c 0    Card n c
  csuc : Card (pred n) c  c (pred n)    c n    Card n c

mkcard :  (n : Nat)  Card n ℵ₀
mkcard zero = czero refl refl 
mkcard (suc zero) = cone (mkcard zero) refl refl
mkcard (suc (suc zero)) = csuc (mkcard 1) refl refl
mkcard (suc (suc (suc n))) = csuc (mkcard (suc (suc n))) (n-∈-ℵ₀ n) (n-∈-ℵ₀ n) -- (diag'-is-∞-is-all-n n)
```
 A function to let you create and view the diagonal of an Ω ordering unchanged,
   and a function to give you n bits of the diagonalization of an arbitrary Ω.
```
raw-diagonal : Ω  Cantor
raw-diagonal 𝕆 n = 𝕆 n n

d-view : Nat  Ω  List Bit
d-view n 𝕆 = n bits (raw-diagonal 𝕆)

g-view : Nat  Ω  List Bit
g-view n 𝕆 = n bits (proj₁ (cantor-➘ 𝕆))
```
 An alternate means of constructing a cardinality-encoding Cantor, by attaching bits
   to the head of the bitstring, beginning with the all-□ string.
```
_⋉_ : Bit  Cantor  Cantor
(b  c) zero = b
(b  c) (suc x) = c x

all-0 : Cantor
all-0 n = 

c-of : Ω
c-of zero = all-0
c-of (suc y) =   c-of y
```
 ⅀ 𝕂nowledge in this file ⟿
 ∙ Cantor bitstrings have the cardinality of the set of reals.
 ∙ A function which maps Nats to Cantors can be diagonalized against.
 ∙ An Ω order Nat → Cantor function is the same as a boolean relation between Nats.
 ∙ A Cantor bitstring can be read as a set of Nats and represent truth under a predicate.
 ∙ A particular format of Cantor bitstrings corresponds to cardinality.
 ∙ Cardinality-bitstrings correspond to ordering-predicate relationships.
 ∙ An ordering-predicate Ω can seem like it provides a complete map of truth but diagonalization
    reveals that the concept of cardinality inherent in the ordering-predicate includes infinite sets.
 ∙ The infinite set of all Nats has a cardinality by the same rules as the finite cardinalities do.
 ∙ It can be produced by diagonalization of the predicate producing finite-cardinality sets.
 ∙ Predicate diagonalization in general finds new possibility-sets previously unconsidered.
 ∙ It is a reliable method for transcending the pattern of a grid of relations with a new pattern.
 ∙ The particular diagonalization in this file encodes learning to see the forest, not just trees.
 ∙ The cardinality-generating Ω can count any number of trees, but only the diagonalization
    sees the whole unlimited forest as a single thing, rather than just an arbitrarily large finite set.
 ∙ This is the pattern of enlightenment, of grasping a pattern and internalizing it yet moving beyond.
 ∙ Diagonalization is a staircase to the next level - dependent typed programs make it an escalator.

 We have shown that our idea of number which we had mapped to the naturals as our index of our generators
   is insufficient to capture the greater conceptual idea of quantity, because we
   find a truth that is not in our enumeration of objects and truth-status under the predicate.
 Our construction seems to possesses a complete list of what quantities fulfill a predicate of > n,
   however despite the seemingly exhaustive nature of this list of truths we can provably produce an
   unlisted bitstring which represents a collection of un-considered cardinality.
 The diagonalization forces a kind of conceptual widening of the scope of quantification.

 ⊫ The core idea is diagonalizing against a correspondence of predicates and truth-generation schemes.
 ⊫ This is an application of the general family of Cantor/Gödel/Turing fixed point theorems.
 ⊫ We have a countably infinite list of Σ statements along one axis that represent truths.
 ⊫ We have a countably infinite list of elements indexed by Nat (not necessarily Nats themselves).
 ⊫ We now consider each row of this matrix as a Cantor bitstring with 0/false and 1/true,
 ⊫ for whether the indexed type satisfies the corresponding predicate.
 ⊫ Thus, an Ω function - aka Nat → Cantor, aka Nat → Nat → Bool aka 2 ^ ( ℕ * ℕ ) is a map of truths.
 ⊫ By performing this diagonalization we show that there is no function that produces a perfect map of truth
 ⊫   between a countable set of objects and a countable set of predicates ranging over those objects.
 ⊫ We have a bijection between predicates and subjects, but mapping the correspondence creates a truth-table
 ⊫   equal to the cardinality of their product, so a T/F map of the objects versus the relations is 2^n
 ⊫   and so is subject to diagonalization which means we can produce a truth outside the system.
 ⊫ There is no complete map of truth of the relations between two countable sets available from
 ⊫   an Ω function, there will always be a ω ∈ 2 ^ ℕ which fulfills the semiotic interpretation     
 ⊫   of the structure and is a set which is lies outside the image of the truth-production function.

 ⅀ The construction seems like it tells us that it has a complete list of quantities,
 ⅀   and how they relate to the size of other quantities.
 ⅀ We can tell the truth-map 'Sorry, I have a quantity that your list does not include - Infinity.'
 ⅀ Wittgenstein ended the Tractatus by talking of throwing away the ladder one used to climb.
 ⅀ Diagonalization is Enlightenment. But it is not something which lies beyond words and proof.

 ℿ Let's look at the product of all this knowledge and what we can do with it.
 ℿ Anytime you are locked inside a square prison of claimed knowledge or rigidly generated pattern --
 ℿ A claimed determined and definitive mapping between a countable list of predicates (possibilities)
 ℿ   and a single truth-production function - a central authority that claims it Knows All Truth -
 ℿ Then even within the limits of that system, you can escape - you can diagonalize against the
 ℿ   rigid square matrix that claims to be all the truth that is and you can make a new truth.
 ℿ All it takes is the freedom to change a single bit - to look at the whole picture and see the
 ℿ   new dimension, the path to transcendence of the system, the diagonalization out of the map.

-- Credits and shoutouts in no particular order and with many worthy Names forgotten :
-- Mietek and others in ##dependent for invaluable discussions of Agda and math and philosophy,
-- Raymond Smullyan, Douglas Hofstader, Roger Penrose, Rudy Rucker, Martin Gardner for logic and paradox,
-- Ulf Norrell, pigworker, Wen Kokke and others for Agda, Martin Escardo for knowledge of Cantor bitstrings,
-- Hugh Woodin, Joel Hamkins, Dima Sinapova, John Baez, Penelope Maddy, Scott Aaronson, Martin-Löf, Malcolm X,
-- G.E.M. Deng ZiQi, RZA, Inspectah Deck, Scott Alexander, Robert Anton Wilson, Terry Tao, Hao Huang,
-- Suzette Haden Elgin, Philip K. Dick, Ada Lovelace, Peter Koellner, Mermaid Echo, Phil & Jerry, Jess,
-- Melanie, Alice, Nicole, Renee, current and former Java Cat baristas, BTS+Abi at Soldier Field, Namewee,
-- Rust Crab & the Spiderqueen-Mind, Robert Pirsig, Ani diFranco, Georg Cantor, unshaven barbers, Les Lokey,
-- Emily Short, Steve Meretzky, Andrew Plotkin, Ken Thompson, Rob Pike, Oleg Kiselyov, Madeline L'engle,
-- Jeff, Revolution cycles, Chase and the elevated Timecycle, Studio G, Janelle Monae, 17d chipmunk fandom,
-- Pete, Amavect, Burnzez, Kvik, Rodri, Henesy, Kiwi, QWX, Umbraticus, Piroko, Halfwit, ∀∈Grid, 17d chipmunks,
-- Cinap, Aiju, Hiro, qrstuv, the rest of Cat-v, Andy and the rest of the Lothlorien elves, Nathan Java,
-- IU, Frank Gray, Beth/Alef, nCUBE, Liz Henry, Overwatch Mei, Octavia Butler, David Jefferson, Tim Curry, V,
-- Ava and Rivendell elves, the Hamsters of Nottingham, the Big Dive Community Orchestra, Jenna, Sanjoy Das,
-- Arthur and the God of Smoke, Anklebiters, Mercury's Wake, We're Freaks, Beethoven, Bob Marley, yosefk,
-- Thwipsters, Monday Night Magic, Housepants, Borges, Murakami, HST, Joan Didion, Draggletails, Dr. Bronner,
-- FFXI Valefor Xiphias linkshell, Deadheads and Wutang fans everywhere, Clara Schumann, UW Music School,
-- Norton Juster for "The Phantom Tollboth" which said we could reunite Rhyme and Reason despite Impossibility,
-- Muhammad Ali , Charles Schulz, Robert Benchley, Tina Turner, Frida Kahlo, Heinlein, GD and the Enthusiasts,
-- Cosmic Delights, the Zenbluesman, Joe, the Afterlife, Mother Fool's, Plaka Taverna, and Wah-kee noodle,
-- Krishna, Buddha, Jesus, Muhammad, Jonathan Livingston Seagull, Tao te Ching, Eru Illuvatar, S.D.G.
-- Luna, and Hayden, and J and g and Carrie Ann, Z, Josh and Grams and everyone else who counts as family,
-- The memory of my grandfather and father who taught me to love math as a fun game, and -
--   Maevele my creative partner more than anyone. ∞ ♥ Σxists ∃ternally.
-- ...and everyone else out there across the entire transfinite multiverse of endless creative unfolding!
```