jcreedcmu

If I have

𝔹 : ∀X. X → X → X

then parametricity tells me

(b : 𝔹)(f : X → Y)(x₁ x₂ : X) → f (b x₁ x₂) = b (f x₁) (f x₂).

From this I want to prove

jcreedcmu

Suppose ℂ is a ω-cocomplete category: it has colimits of any
diagram that is a functor ω → ℂ. Suppose ℂ has an initial object ⊥.
Suppose F is a functor ℂ → ℂ that preserves all ω-colimits.

Let U : ω → ℂ be the diagram

       !      F!       F²
    ⊥ → F(⊥) → F²(⊥) → ⋯

Lemma: If we have a map m : FA → A, then we can construct a map colim U → A.

jcreedcmu

open import Agda.Primitive

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A

jcreedcmu

Lemma 2: ("Real Induction") Let A be a subset of real numbers.
If
 (0) α ∈ A
 (1) ∀x ∈ A. ∃y. [x,y) ⊆ A
 (2) ∀xy. [x, y) ⊆ A ⇒ y ∈ A
then [α,∞) ⊆ A.

Proof:
Suppose towards a contradiction that [α,∞) ∖ A is nonempty. Set β = inf ([α,∞) ∖ A).
(1) means we can't have β ∈ A, because it would collide with the infimum.

jcreedcmu

/***
 * A little bit of research into what would be needed for a "direct manipulation" toy in emacs.
 * - NodeJS allows replacing `Error.prepareStackStrace` with a custom handler that can obtain
 *   first-class stack trace data.
 * - An arbitrary function call (see below, `knob(1429)` for example) can obtain a stack
 *   trace and inspect it to find out where in the file the actual call to knob(1429) took place.
 * - Since we're in typescript, we can also find the sourcemap and use it to map this into
 *   a location into the original `.ts` file.
 * - We can shell out to emacsclient to evaluate arbitrary elisp
 * - It can in turn go to the appropriate place in the active buffer viewing the `.ts` file,

jcreedcmu

// g++ -I/usr/local/include/SDL2 -I/usr/include/GL b.cc -lSDL2 -lGL -lGLU -o b

#include <SDL2/SDL.h>
#include <SDL2/SDL_opengl.h>
#include <gl.h>

static SDL_Window *window;
static SDL_Renderer *renderer;

#define width 640

jcreedcmu

const W = 52;
const H = 30;
const MAX_ITER = 1000;

function iters(cr, ci) {
  let zi = 0;
  let zr = 0;
  for (let i = 0; i < MAX_ITER; i++) {
    [zr, zi] = [zr * zr - zi * zi + cr,  2 * zr * zi + ci];
    if (zr * zr + zi * zi > 16.0) return i;

jcreedcmu

5403 Friendship Avenue.

Henry Wright Fisher loĝis ĉi tie en 1912.

Sr. Fisher naskiĝis en Youghal, Ireland, Januaro 31, 1861, la filo de
Abram kaj Sara (Wright) Fisher. Li alvenis al Usono je 1874, kaj post
dekkvar jaroj, ricevis diplomon pri mekanika inĝenierarto de la
universitato Cornell. Post diplomiĝo, li ligiĝis kun la entrepreno
Bergman & Co. kaj la C. & C. Motor Company, kaj poste eniris la
servicon de Standard Underground Cable Company, fariĝinte ĝia

jcreedcmu

# # I ran the following perl script on the file
# # https://www.unicode.org/Public/UCD/latest/ucd/UnicodeData.txt:
# 
# #!/usr/bin/perl
# 
# use charnames();
# use utf8;
# use open qw( :std :encoding(UTF-8) );
# use File::Basename;
# 

jcreedcmu

import { Point, rot90, rotate, vdiv, vdot, vplus, vscale } from './point';

const NARROW_COLOR = '#ffffff';
const WIDE_COLOR = '#7777ff';
const BG_COLOR = WIDE_COLOR; // '#dff';
const LINE_WIDTH = 0.25;

const width = 1024;
const height = 768;
const OFF_MIN = -9;