jcmckeown

/************ basic complex functions ***
* I once tried to implement "double" versions of these, too; something hung-up...
*/

float[] cOne = {1.0,0.0};
float[] cZro = {0.0,0.0};
float[] cmOne = { -1.0, 0.0 };

float[] cmul ( float[] c1 , float[] c2 ) {
    float ans[] = new float[2];

jcmckeown

// Parameter space for Cubic Newton-Raphson fractals --- review Stuff, it's probably helpful

/************ section for basic complex functions ****/

float[] cOne = {1.0,0.0};
float[] cZro = {0.0,0.0};
float[] cmOne = { -1.0, 0.0 };

float[] cmul ( float[] c1 , float[] c2 ) {
    float ans[] = new float[2];

jcmckeown

import interfascia.*;

float[][] angleGens =
  { /// fair approximately, where x is an oriented axis cycle matrix (x^(2n) = -1, or x^(2n+1) = 1), the coefficients a_k of a solution (log x) = Σ a_k x^k 
    {0}, // we could do these more precisely in code, but instead we got them from Maxima; five digits ought to be enough for anyone...
    {0, 1.0},
    {0,-1.00000, 1.00000},
    {0, 1.41421,-1.00000, 1.41421},
    {0,-0.85065, 0.52573,-0.52573, 0.85065},
    {0, 2.00000,-1.15470, 1.00000,-1.15470, 2.00000},

jcmckeown

/**
 We want to construct the set of order-ideals in
  the product partial-order on the binary n-cube (2^n);
  we want to do this in such a way that the containment order (I < J)
  is easy to calculate, and in particular such that the *atomic* moves
  are easily recognized.
  
  Now, an order-ideal in a *successor* binary cube (2^{n+1}) can be 
  construed as a pair (I and J) of order-ideals in the n-cube, such that J <= I.
  Then, two such pairs (I1 >= J1) and (I0 >= J0) are *ordered* (I1>=J1)<(I0>=J0)

jcmckeown

Require Import HoTT. (** the version from 2012... which was a while ago... *)

Open Scope path.
Open Scope equiv.
Open Scope type.

(** you see, back in the day, the hoqide was (by design) missing some things,
 and as a result, the "remember ... as ..." tactic was broken. *)

Ltac mmember X Y :=

jcmckeown

PImage nextFrame;

void rule30(){
  int j,k, midpt;
  background(255);
  loadPixels();
  midpt = floor(width/2);
  set(midpt,0,color(0));
  for ( j = 1 ; j < height ; j++ ) {
    for ( k = 1 ; k < width-1 ; k++) {

jcmckeown

/**
  PRELUDE: the names given in this initial comment are (in my own thinking) mostly fanciful, in that I don't mean that
  any of the particular people named particularly considered those particular things named for them in this note except
  perhaps Thurston; but they *are* meant to lend recognition to some names genuinely connected with the subject of this
  sketch.  Of course, the name that really makes any of this connect to that thing is Yoccoz, and none of these things
  is named for him...
  NOTATION: until further notice, capitals [W] indicate words and miniscules [x] indicate single letters. 
  length of a word is notated #[W].
  DEFINITION: given a word A of the form [WxY], where [x] is the n'th letter; the n'th SPLIT of A is the word
  [WxxYWxxY]

jcmckeown

Require Import Arith.

Open Scope list_scope.

(** Print le
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
    
*)

jcmckeown

(** 
Dybjer and Setzer provide a logical framework in which Induction-Recursion — 
mutual definition of an (A : Type) and a (B : A -> V), in which constructors for A can talk about values of B, and B is defined by case analysis on members of A — 
becomes equivalent to supposing initial algebras for certain functors on { X : Set & X -> V }.  However, this latter family is, up to equivalences over V, the same as ordinary maps V -> Set.  The universal case, in which V = Set, becomes somewhat trickier, for universe level reasons.

In any case, here is one way to define a "large" universe ("large" in the sense: we allow all externally definable functions) with naturals, dependent sums, and dependent products.  A more careful presentation might work on a fibration over functions,
 { AB : Type * Type & fst AB -> snd AB } -> Type
instead, but good luck with that.
*)

jcmckeown

var id_math_stuff = {
    // id_math_stuff.theMJ
    theMJ : window.MathJax,
    
    // id_math_stuff.idMathRun =
    idMathRun : function () {
        if (id_math_stuff.theMJ) {
            id_math_stuff.theMJ.Hub.Queue(["Typeset", id_math_stuff.theMJ.Hub, "idc-cover"]);
        } else {
            console.log("there is still no mathjax?");