Instantly share code, notes, and snippets.

# jcreedcmu

Last active April 26, 2024 18:27
puzzle.md

## Puzzle

There is a party with 37 people. Every pair of them is either friends or not friends. Alice and Bob are the only two people at the party with the same number of friends. Alice and Bob are not friends with each other.

How many people are:

• friends with both Alice and Bob?
• friends with Alice and not Bob?
Last active April 14, 2024 13:19
parametricity.txt
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
Last active March 19, 2024 21:28
lil fixpoint lemma
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.
Last active March 18, 2024 00:09
proof of correctness of chaotic iteration
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
Created May 10, 2023 00:34
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.
Created March 17, 2023 22:35
Snippet of typescript that modifies itself in an emacs buffer
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,
Last active December 28, 2022 16:49
minimal sdl2/opengl example
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 #include #include static SDL_Window *window; static SDL_Renderer *renderer; #define width 640
Created November 30, 2022 23:34