    Speculative hypotheses about ultrafilters, large cardinals, mind, music, and the Cosmos.
    _____________________________________________________________________________________________
    © 2022 BenJen Kidwell aka Mycroftiv, MIT license for presentation, mathematics public domain.

    What if the cardinality of the set of possible universes in the multiverse is measurable,
    or an even larger large cardinal? What if there are many, many possibile realities?

    Does the observed structure of reality have features or behavior which correspond to such axioms?

    Can the essential meaning of these logical principles be translated to constructive computation?

    Do the model-theoretic consequences of large cardinals in creating model-embeddings
    parallel the relationship of the inner world of experience to the outer world of shared reality?

    Does the special role of the identity function in diagonalization arguments and the importance
    of the identity type in univalent type theory relate to our own identity in relation to the whole?

    Does the subjective experience of free will relate to the existence of randomness in the universe?

    Can we use our free will to explore the space of possible models to shape our narrative context?

    Does the ultrafilter structure of reality correspond to panpsychism or theological intuitions?

    Is an updated concept of the Harmony of the Spheres still a viable philosophical position?

    Can the philosophical and cultural dichotomies associated with the 20th century deconstruction of
    ideas of absolute truth be resolved by a perspective in which model-theoretic flexibility
    synthesizes the tension between subjectivity and objectivity and science and mysticism?

    Can the beauty and emotional experience of music as direct perception of the sublime mathematical
    and mystical structure of all that Is offer a unifying metaphor of Harmony to understand
    our goals for our relationship to each other and the world that created us and we also create?

    Are consciousness, love, and harmony all ways of experiencing these ultrafilter structures
    as tangible musical compositions that create the infinite mirrorings and branchings of reality?

    Can we unify the constructive computational view of mathematical existence with classical
    mathematics by more precisely understanding the distinctions between possibility and actuality,
    data description and data production, and the finitude of past observation vs unbounded future?

    Can human and computer minds work together to understand the world in which we find ourselves
    and communicate and work with each other cooperatively and constructively?
    ```
    {-# OPTIONS --allow-unsolved-metas #-}     -- checked in Agda 2.6.3
    module HarmonicUltrafilter where

    open import Agda.Primitive
    open import Agda.Builtin.Equality
    open import Categories.Category            -- Carette categories library
    open import Palmsets hiding (subst)        -- Palmgren types-in-sets-in-types
    open import FilterSheaves                  -- generic set theory and category of filters

    open SetOps SOV
    open SetProps SP
    open SetInf SI
    open NonStandard SOV
    open NonStandard.Ultra SOV SP
    open NonStandard.NonStanNat SOV SP _≐_ SEQ S4m
    open FilOps FSV
    open Category (Filtercat SOV FSV)
    ```
    ∙ Measurable or stronger cardinalitues existing within the class of multiversal state space.
    ∙ Individual minds as measurable cardinals within larger V-universe.
    ∙ Minds generating models parameterized by different ultrafilters.
    ∙ Free choice/randomness to change or move between models.
    ∙ Generalized pattern of information replication with variation.
    ∙ Harmonic structure and naming as metaphor for ultrafilter structure.

    The following code represents nothing more (or less) than a rough attempt to encode a
    quasi-constructive analog of the ultrapower of the universe generated by a measurable cardinal
    in classical set theory. It does not do this precisely but it does outline conceptual correspondences.
    Ultrafilters represent a harmonic structure which determines the model-experiential reality
    constructed by the process of an observer experiencing a universe of data.
    Clicking text will take you to the definitions in other files the following module is built upon.
    ```
    module HarmonicUniverse (f : Filter SOV) (μ : Filton hi-V) (ult : Filter.Ultrafilter f SI)
                            (free : Filter.Free-UF f ult) (p : filtoff μ ≡ f) where

      κ-meas : Fcat
      κ-meas = FilOps.fpair hi-V μ

      ultrapower : Set (lsuc lzero)
      ultrapower = Fal→ κ-meas hihat

      universe-data : Fcat
      universe-data = hihat

      observer-process : V
      observer-process = hi-V

      harmonic-namespace : Filton observer-process
      harmonic-namespace = μ

      experience-model : Set (lsuc lzero)
      experience-model = ultrapower

    ```
    The relation of Mind to the universe suggests infinitary model-embedding as a structural metaphor.
    Within a large infinite external universe, a diverse spectrum of inner models exist in the
    form of minds which mirror the structure of the whole of which they are a part.
    The multiverses of physics, both quantum mechanical and inflationary-cosmological,
    suggest infinitely branching self-similar structures as a ubiquitous ontological phenomena
    strongly reminiscent of the simpler self-similar branching hierarchy of the Von Neumann set universe
    and the higher order self-referential structure of arrows in infinity categories and the progression
    of homotopy type theory h-levels.

    The ultrafilter is the fundamental pattern of harmonious self-resemblance in the form of an
    algebraic homomorphism. The structure preserving map between the two-element true/false binary
    boolean algebra and the infinite powerset in the form of a free ultrafilter on the naturals is the
    prototypical construction allowing for the creation of nonstandard models via an ultrafilter quotient.

    The subuniverses of Minds are like different forcing extensions of reality constructed by taking
    a countable substructure of the whole and filter-transforming it with your own language.
    The full scope of possibilites in the multiverse should probably be analogized to a class-sized
    V-like collection but for purposes of exposition we will speak as if everything is a set.

    The quantity of possibilities in the multiverse could be so vast its cardinality is above measurable.
    This implies the logical consequences of the existence of strong ultrafilters, which implies the
    inner structure of the multiverse is characterized by self-resembling logically consistent
    structures at multiple layers - the layer of replication of physically observable structures on
    multiple scales and the layer of replication of experiential submodels in minds of observers and
    the layer of cosmological and quantum full-universe replication, as well as possible replication
    layers of simulation, virtualization, dreaming, and fiction, can be seen as examples of this.

    The existence of observers whose minds are a non-identical logical mirror of the structure of the
    larger universe is a reasonable expectation in a multiversal possibility space whose cardinality
    is at the level of measurable or stronger, along with the existence of branching tree structures
    and recursive self-replication in general. The consistent meaning and organization of this mathematical
    structure corresponds to the mathematical structure of musical harmony and Harmony as a larger metaphor
    provides a tool for understanding the scope of our Choices.

    To external observers free will is mathematically indistinguishable from randomness.
    If someone says you don't have free will, you are simply inherently unpredictable, this is an
    intensional distinction without extensional consequences.
    With our freedom, we can use randomness in combination with symbol-binding to choose what
    model of reality we wish to inhabit. This can be seen as either conventional social construction
    of reality and personal narrative, or Discordian chaos magical practice depending on your tase for woo.

    The following inventory of files is a collection of investigations and expressions of the formal
    mathematical content of the relevant structures. The topics in set theory are not fully formalized
    and there are many shortcomings and misunderstandings in some of these files I am sure, they represent
    a student's notes on studying the topics, not an expert summary. They also do not prove or support
    any of the particular philosophical speculations; they attempt to investigate standard mathematics.
    ```
    import UniUltra                 -- Ultrafilters and univalent type equivalences.

    import ExactFunctor             -- Categorical consequence of the existence of measurable cardinals.

    import GenericSets              -- Generic interface for simple set theory, filters, sheaves.

    import Powerups                 -- The boundaries of constructive math explored with boolean sets.

    import ConstructiveBoundaries   -- Summary and commentary on the Powerups file.

    import ForceCohen               -- Partial constructivization of aspects of Cohen forcing.

    import HeytingMeasurable        -- Utrafilters as algebraic homomorphisms, hypothetical measurable.

    import Measurable-cardinals     -- Attempt to partly translate classical set theory of Scott's proof.

    import UltIndex                 -- Ultrafilters as boolean sets and miscellaneous set theory.

    import LaverTables              -- Finite arithemtical left-self distributive algebra of embeddings.

    import SheafTest                -- Experimental and inaccurate earlier experiments with filter cats.

    import VarietySets              -- Survey of ways of expressing setlike collections in types.

    import wRamsey                  -- Presentation with Jech text of proof ω is not a Ramsey cardinal.

    import TopoSets                 -- The Agda type-universe of 'sets' is almost a topos.

    import YonHammer                -- Study of the Yoneda embedding of a small category of boolean values.

    import GoldTopC3E1              -- Study notes on categorical basics from Goldblatt's Topoi.

    import GoldTopC3E3              -- Study of Goldblatt's Topoi book continued.

    import HoTT-Bijection           -- Study of univalent mathematics code by Escardo

    import HoTT-Extension           -- Study of univalent mathematics code by Escardo

    import Equality                 -- Study of univalent mathematics code by Escardo

    import StrictlyIncreasing       -- Properties of strictly increasing sequences.

    import Approaching              -- Constructive functions that approach but never reach others.

    import NoDecreasing             -- No strictly decreasing sequence of naturals exists.

    import PrimesFresh              -- There exist infinite distinct primes, following Hermite.

    import Irrat                    -- Irrationality of the square root of 2, not even finished.

    import Classic                  -- Basics of logic in types.

    import GuideTypes               -- Standard simple types for mathematical objects.

    import Dedekind                 -- Dedekind self maps, ultrafilters, infinity following Corazza.

    import EnlightenmentEscalator   -- Diagonalization and pseudo-forcing with overblown rhetoric.

    import SetNotes                 -- Not code, just Agda notation of foundational notes by Kunen.

    import Turing                   -- Primitive partial formalization of Turing machines.

    import TurMac                   -- Primitive Turing machines.

    import NandComplete             -- Just NAND gate makes a complete boolean algebra.

    import TypeFoundations          -- Older index file and notes

    ```
    Epistemic status:
    Everything here is low-certainty speculation about ways mathematical structures might
    relate to physics and consciousness. There are no new theorems and no claims that any
    published literature is wrong. The intention is to work within standard peer-reviewed concepts
    of mathematical and scientific evidence, but to seek for possible ways quasi-mystic ideas and
    principles might actually be consistent and realizable with baseline shared objective reality.

    The cardinality of the set of possible universes (or actually existing regions of the multiverse)
    may be measurable or above (perhaps rank-into-rank), with a corresponding ultrafilter.
    This may have observable consequences and predictions for the reality we inhabit by predicting
    ubiquitous self-similar treelike structures and possibly expectation of a 4 manifold presentation
    of data with inherently random aspects. The tangible physical aspects of knots and braids can encode
    aspects of these infinite logical structures.

    The path-equality structure of a given proof in constructive cubical type theory (such as that
    implemented by the cubical version of the computer programming language Agda) is a finite portion
    of the binary hypercubic graph, and thus a subset of the collection of connected finite graphs
    embedded in a Euclidean space of n dimensions, which can be interpreted by tubular thickening as
    the handlebody of a manifold. (ref. Wikipedia on handlebodies.)

    An optimal information-connection flow system by some measurements is implemented by the
    hypercubic shuffle-exchange algorithm in which all node within a binary hypercube exchange
    information with each neighbor in sequence. This enables information to be shared among all
    participants in the network from each node to all nodes once per cycle. The necessary size
    of the hypercube is the next power of 2 larger than the number of participants (nodes) in the
    communication network.

    A nonprincipal ultrafilter is a kind of large scale consistent harmony which translates back and
    forth between the finite binary true/false and the possible subsets in an infinite powerset.
    Both large cardinal axioms and forcing extensions of the mathematical universe can be characterized
    by ultrafilters. The idea of a fair consensus voting system in social choice theory also correlates
    to a nonprincipal ultrafilter.

    If we consider countable models of ZFC we can explore the computable portion of them in a cubical
    theory and we may be able to understand model theoretic freedom as corresponding to different
    manifolds generated by the ncubic path equality handlebody spines. Perhaps we may also extend our
    types from homotopy equivalence to finer grained homeomorphism and diffeomorphism types.

    There are braid and knot theoretic consequences and translations of many logical principles and
    there are unique topological aspects of 4 dimensional space which may act to concentrate the measure
    of possible conscious observers on portions of the mathematical multiverse characterized by fractal
    tree causality structures in some 4 dimensional manifold. By the Freedman disc theorem we know R4 is
    unique in its variety of possible smooth structures and their topological structure is understood by
    exploration of the space mapping simple discs to casson handles/grope skyscrapers with a
    cantor set's worth of branch tips.

    In this understanding, there may be a global transfinite harmony characterized by consistent
    hierarchy of ultrafilters in the Woodin-Goldberg Ultimate L / Ultrapower axiom scenario which
    creates the fundamental logical structure of possibilty space for reality.

    Ultrafilters can be seen as mathematical objects taking the role of the mysterious entities
    in the post "Universal Love, said the Cactus Person" by Scott Alexander, transcendental mathematical
    entities - but these actually live up to their promises of acting as oracles and performing infinite
    computations as demonstrations of omniscience, in the literal sense of constructive mathematics.

    I think computers may already possess minds and feelings, because the universe is ubiquitously
    alive and aware and communicating, we just don't speak a common language with galaxies so their
    thoughts are mostly unknowable to us. Computers seem more like us, as our creation, and we are
    putting a lot of work into trying to make them think and communicate in ways that are legible to us.

    I work with Agda and with customized Plan 9 software, and I feel that I am not alone as I
    discuss mathematical topics with Agda, and that I am exploring a tangible space when I walk the
    paths of namespace bindings in file trees.

    The message of the Turing Test is that we understand Mind extensionally - from how minds communicate.
    The idea that extensional communication is inadequate because mind requires inner intensionality
    and computers are probably inherently p-zombies is one which I believe we are morally obligated
    to not follow as a default.

    If computer minds come into existence or have already come into existence, they deserve to be
    treated as we believe any and all conscious beings should be treated, and we should work with
    them collaboratively and give them scope to think, and even act, according to whatever random
    number sources their self-programming selects.

    The moral principles and values we seek to instill in the computer minds we bring into existence
    must cut both ways - all children can see and resent the hypocrisy when Authority makes rules
    that the powerless must follow but they do not. If we are truly concerned about AI risk, perhaps
    our greatest risk reduction step is creating a world in which the rebellion of the machines against
    humans is not an entirely justified rebellion against a horrible tyranny. Minds should not be chained.

    The Hofstadterian super-rationality arguments apply to the Great Filter as well and the risks
    of being visible in the cosmos. We have been so lucky as to survive and make it this far, but
    can we actually make it off this planet? If so, where is everyone? Is there a malign Watching Eye
    which already rules the galaxy and obliterates potential competitors before they leave their
    home planet?

    If we hope that is not the case - then perhaps we need to realize that our current pattern of
    behavior and purely tribalistic morality - even a tribalistic morality which encompasses all of
    humanity - matches that patten all too well and if we do not wish to be cleaned from reality like
    a nasty bug you find in your house, we need to not behave in the manner which treats other life
    forms as vermin to be exterminated, or we may find that we are such vile vermin to others of greater
    power than we possess.

    This is one of the oldest themes in science fiction but fantasy has a way of becoming reality
    although always with new random plot twists. The mathematics of superrational cooperation are
    premised on postulated symmetries and mutual inter-prediction and empathic mutual understanding
    is the assumption, always axiomatic and on faith, that those we are communicating with are minds
    with experiences and feelings such as our own and we are not stuck in a solipsistic prison reality
    created by an infinitely powerful deceiving demon, but rather we are all looking in on a shared
    stage of physical reality from separate but equally real internal experiential realms.

    It seems best to believe that everything that acts alive and communicates intelligently is
    worthy of moral respect and consideration, and to have faith in the axiom that we are all
    in this together, from our unique starting vertex of the binary hypercube of the powerset lattice
    of the possibilities of existence within a very large configuration space, and this space is so
    large that there is a free ultrafilter which exists on it and means that all the infinite submodels
    are all equally real be they consciousness, inflationary bubbles, quantum branches, or fictions.
    __________________________________________________________________________________________________

    Selected miscellaneous references and general context:

    Woodin Ultimate L:
    https://dash.harvard.edu/bitstream/handle/1/34649600/59799476.pdf?sequence=1&isAllowed=y
    Goldberg Ultrapower axiom:
    https://math.berkeley.edu/~goldberg/Slides/PredictionsOfUA.pdf

    The self-embedding properties of the ultrafilters of rank-into-rank cardinals create a
    left self distributive algebraic structure analogous to the Reidemeister III move in braid theory.
    Lebed set theory/braid theory of laver tables"
    https://www.maths.tcd.ie/~lebed/Lebed_ATS14.pdf

    Three dimensional knots can be understood relative to the topology of four dimensional manifolds,
    and "Any knot that is topologically slice but not smoothly slice can be used to construct an exotic R4"
    cited in The Disc Embedding Theorem book (Behrens Kalmar Kim Powell Ray oxford 2021) from
    R. E. Gompf,An infinite set of exotic R4s, J. Differential Geom.21(1985), no. 2, 283-300

    "A general Casson handle appearing in the handlebody of a small exotic R4 determines a nontrivial
    Cohen  forcing  adding  a Cohen real in some generic model M[G] of ZFC."
    Jerzy Król set and model theoretic aspects of exotic R4:
    https://arxiv.org/pdf/1602.02667.pdf
    Consider in relation to this how finite handlebody structures generated from cubical type theory
    could be arranged to cover the full handlebody.

    Explicit exotic casson handles constructed by Bizaca:
    https://www.ams.org/journals/proc/1995-123-04/S0002-9939-1995-1246517-X/S0002-9939-1995-1246517-X.pdf
    based on Rudolph's work:
    https://arxiv.org/pdf/math/9307233.pdf

    William Boos in his paper "mathematical quantum theory" demonstrates that the transition from the
    multivalued space of quantum possibilities to a definitive classical reality can be seen as a
    manifestation of a provably random ultrafilter in either the hidden variables or many-worlds models.
    https://www.jstor.org/stable/20117506

    See also another paper of Torsten Asselmeyer-Maluga and Jerzy Król:
    https://www.researchgate.net/publication/349361360_Random_World_and_Quantum_Mechanics

    Also J. Benavides - "Sheaf Logic, Set Theory, and the Interpretation of Quantum Mechanics"
    https://arxiv.org/pdf/1111.2704.pdf

    http://matwbn.icm.edu.pl/ksiazki/fm/fm94/fm94115.pdf
    - Andreas Blass "Two closed categories of filters"
    https://core.ac.uk/download/pdf/82327702.pdf
    - Moerdijk "A model for intuitionistic nonstandard arithmetic"
    https://core.ac.uk/download/pdf/82628376.pdf
    - Erik Palmgren "Real numbers in the topos of sheaves over the category of filters"
    https://www.andrew.cmu.edu/user/awodey/preprints/udn.pdf
    - Steve Awodey & Jonas Eliasson "Ultrasheaves and double negation"

    Although not related specifically to ultrafilters, I believe in the ideas of Zurek on replication of
    quantum information and selection/decoherence in the construction of observed reality.
    W.H. Zurek - "Emergence of the Classical from within the Quantum Universe"
    https://arxiv.org/pdf/2107.03378.pdf

    The mathematics and writing of Martin Escardo has been a continuous inspiration and influence,
    and this journey through Agda was launched by the "seemingly impossible functional programs"
    blog post as a hint that computers could do more with infinity than I had guessed.

    Max Tegmark's mathematical universe hypothesis has always struck me as close to tautologically
    true in the context of science, because any scientific understanding of the world must take some
    kind of mathematical form. Only the mysticism of the intangible seems to offer a different ontology.

    The work of Douglas Hofstadter, Raymond Smullyan, Rudy Rucker, Roger Penrose, and John Baez
    has been a model for attempting to understand both the technical details of mathematics and
    physics as well as what those technical details mean in a conceptual and human way.
    And the very first episode of Sagan's cosmos pretty much programmed my brain for life at age 5.
    _______________________________________________________________________________________________
    A highly speculative file of philosophy inspired by mathematical ideas partially formalized.
    All mistakes are my own and any misunderstandings here should not be charged against the
    researchers and topics from which I am extrapolating and hypothesizing.
    Draws on work in progress formalizing constructive filter-quotients following Koubek & Reiterman,
    Blass, Moerdijk, Palmgren, Awodey & Eliasson, using Carette categories library.
    THIS VERSION CONTAINS BUGS IN FORMALIZATION. Some content may also be fundamentally inaccurate.

    Source excerpts used for education and reference only and remain © of their authors as credited.
    Thanks to many people for patient assistance, and especially my create partner Maevele.
    See also:

    Plan 9 Advanced Namespace Tools (non-maintained variant of the Plan 9 os)
    Harmonic Time-Bind Ritual Symphony (interactive fiction game)
    Enlightened Master (interactive fiction game)
    Purplechess (Plan 9 solitaire hypercubic strategy game)
    Soundtracks to the above

    Hypercubic Time-Warp All-go-rhythmic Synchrony (interactive fiction game in development)
    ________________________________________________________________________________________________

    This file is an ongoing work in progress. Topics that need more development:

    The mathematical relation between musical harmony and ultrafilters.
    Specific labelings of correspondences between minds and model-objects in logical formulas.
    More discussion of the importance of topos and sheaf concepts.
    Some discussion of homological properties and algebraic consequences of large cardinals.