HoTT-mm-ADT.txt

HoTT and Sweaty with mm-ADT
---------------------------
   http://mm-adt.org/vm

In homotopy type theory,

there is a space U,  (universal set)
a is a point in U,          (object)
b is a point in U.          (object)

...written a:U and b:U.

Assume two "deformations" of U called f and g (functions) such that:

  f(a)=b
  g(b)=a
  
Given these mappings, a and b are equivalent (a bijection exists). 

What is f and g? They denote paths through the space U.

  a--f->b
  a<-g--b

What is a path? 
  A _continuous_ mutation of the source obj that yields the target obj (a "puddy" interpretation of objects).

Lets say that f and g are too course cause they imply a single step to go from a-->b and b-->a. 
Assume f and g are composed of smaller functions...to the limit of the base operations of the underlying machine.
  - instruction set architecture of a hardware machine
  - unitary functions applied to a wave function on the physical reality machine.

Using the first machine: 
  Let [x] denote an instruction such that f and g can be further decomposed into a linear sequence of such instructions:

f = [f1][f2][f3]
g = [g1][g2]

Now,   a--f->b   and  a<-g--b    become

 a--[f1][f2][f3]-->b
 a<----[g2][g1]----b

These are paths in U.

A "homotopy" is a path between paths. Graphically, the path [h1][h2][h3] below is a homotopy.

 a-[f1][f2][f3]->b
    \___    __/
        [h1]
        [h2]
        [h3]
       /    \
 a<---[g2][g1]---b


Thus, the paths

 a--[f1][f2][f3]-->b
 a<----[g2][g1]----b 
 
are now thought of as points in the higher dimensional space U'. Lets write them more succinctly and unambiguously as:
 
 (a[f1][f2][f3]b)
 (a[g2][g1]b)
 
 such that the homotopy is denoted
 
 (a[f1][f2][f3]b)--[h1][h2][h3]-->(a[g2][g1]b)
 
 Assume another homotopy.
 
 (a[f1][f2][f3]b)--[i1][i2][i3][i4]-->(a[g2][g1]b)

Then there is new even higher dimensional space U'' with a homotopy.

 (a[f1][f2][f3]b)--[h1][h2[h3]-->(a[g2][g1]b)
                    \__   __/
                       [j1]
                     __[j2]______
                    /            \
 (a[f1][f2][f3]b)--[i1][i2][i3][i4]-->(a[g2][g1]b)

Hold your breath and keep repeating this process.

We are now in the world of higher dimensional algebra: higher dimensional category theory and the oo-groupoid (oo = infinity).
What makes this an algebra? Homotopies are algebraic groups. (A group-oid is just a group whose operation is a partial function).

A group has an identity element, 
               inverse elements for each element, 
               a multiplication operator, 
               and is associative.

The identity is [noop].                     (empty instruction)
The inverse is [x'].                        ([f][f'] = [noop])
The multiplication is path concatenation.   ([f1][f2][f3]*[f4][f5] = [f1][f2][f3][f4][f5])
The associativity is provable.              ([f1][f2])*[f3] = [f1]*([f2]f3])

The group(oid) provides the algebraic structure for manipulating the space U, U', U'', U''', 
   ... their points, and the paths the connect them.

========== mm-ADT: From HoTT to Sweaty

The above is naturally captured (coincidentally) by the free algebra poly objects of mm-ADT.

     https://www.mm-adt.org/vm/#_poly_types

In mm-ADT there are values (points) and there are types (paths). 
Given the running example above, in mmlang (the assembly language of mm-ADT), the a->b->a paths are written:

b<=a[f1][f2][f3]
b<=a[g2][g1]

      https://www.mm-adt.org/vm/#_type_structure
 
The homotopy is denoted using poly lifting:

      https://www.mm-adt.org/vm/#_poly_lifting

(b<=a[g2][g1])<=(b<=a[f1][f2][f3])[h1][h2][h3]
  codomain            domain       continuous deformation

There are 3 distinct polys -- ,-poly (abelian groupoidal), ;-poly (monoidal), |-poly (near-ring-oidal). 
Together, they denote the lifted encoding of the underlying algebraic ring of mm-ADT.

       https://www.mm-adt.org/vm/#_poly_embedding (old part, may be super ghetto)
       
mm-ADT uses poly as collection data structures, data flow structures (i.e. path fibrations via sum), 
metaprogramming/reflection/introspection/etc., type rewriting (homotopies!), and if you act now, you get a coupon for 50% off...

The free obj polys provide the oo-groupid 'tower' of path to point projections to higher dimensional spaces.

Thank you.
Billy Boy McCroy and the All Star Jug Band