This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
//////// | |
// The vm module lets you run a string containing javascript code 'in | |
// a sandbox', where you specify a context of global variables that | |
// exist for the duration of its execution. This works more or less | |
// well, and if you're in control of the code that's running, and you | |
// have a reasonable protocol in mind// for how it expects a certain | |
// context to exist and interacts with it --- like, maybe a plug-in | |
// API for a program, with some endpoints defined for it that do | |
// useful domain-specific things --- your life can go smoothly. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/*** | |
* 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, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# # 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; | |
# |
NewerOlder