Skip to content

Instantly share code, notes, and snippets.

View mstewartgallus's full-sized avatar
🏳️‍⚧️
Trans

Ms. Molly Stewart-Gallus mstewartgallus

🏳️‍⚧️
Trans
26 followers · 4 following
View GitHub Profile
@mstewartgallus
mstewartgallus / syntactic.v
Last active December 1, 2023 17:17
I tried to do some Polynominal endofunctor stuff in a slightly more syntactic way. Unfortunately I don't think it quite works.
Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.
Inductive U :=
| const (A: Type)
| id
(* | compose (τ0 τ1: U) *)
| empty
@mstewartgallus
mstewartgallus / fixed.v
Last active October 28, 2023 05:14
the fixed point of a lax double endofunctor on Span ought to be a category. I can't figure it out though as I get trapped in setoid hell and stuff.
Set Primitive Projections.
Require Import Coq.Unicode.Utf8.
Reserved Infix "∈" (at level 90, right associativity).
Variant fiber {A B} (f: A → B): B → Type :=
| fiber_intro x: fiber f (f x).
Arguments fiber_intro {A B f}.
@mstewartgallus
mstewartgallus / kappa.v
Last active October 25, 2023 22:32
Some weird kappa calculus stuff with symmetric multicategories
Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Coq.Lists.List.
Import List.ListNotations.
Reserved Notation "Γ ⊢ Δ ⇒ τ" (at level 90).
Reserved Notation "x ∈ Γ" (at level 90).
Reserved Infix "$" (at level 20, left associativity).
@mstewartgallus
mstewartgallus / zippertypetheory.v
Last active June 7, 2023 18:56
Global Set Primitive Projections.
Require Import Coq.Unicode.Utf8.
Require Coq.Lists.List.
Import List.ListNotations.
Variant zipper {A} := zip (Γ1: list A) (τ: A) (Γ2: list A).
Arguments zipper: clear implicits.
@mstewartgallus
mstewartgallus / silliness.jsx
Created April 18, 2023 17:25
Mostly silly because you can just use an error boundary utility based around https://react.dev/reference/react/Component#static-getderivedstatefromerror
import {
lazy, Suspense,
createContext, useCallback, useContext, useEffect, useReducer, useTransition
} from "react";
const initialState = {
poison: false,
throwable: undefined
};
@mstewartgallus
mstewartgallus / panel.jsx
Last active March 19, 2023 20:28
Fscked up ebil shenigans. It doesn't actually seem possible to use details for an accordion not even by abusing aria-owns. Unfortunately the spec says that summary is only sometimes exposed as a button role. details has only slightly less weirdness.
import { useId, useState, useCallback } from "react";
const Panel = ({children, heading}) => {
const detailsId = useId();
const headingTextId = useId();
const headingId = useId();
const contentId = useId();
const [open, setOpen] = useState(false);
const onToggle = useCallback(e => {
@mstewartgallus
mstewartgallus / impredicative_induction.v
Created March 10, 2023 00:17
Really confused here. I thought induction was not derivable. Not sure how that applies to anafunctions?
Require Import Coq.Unicode.Utf8.
(* ana is short for anafunction, not really a better name *)
Definition ana A := { P: A → Prop | exists! a: A, P a }.
Definition map {A B} (f: A → B) (x: ana A): ana B.
Proof.
exists (λ b, ∃ a, proj1_sig x a ∧ f a = b).
destruct x as [? [a p]].
exists (f a).
@mstewartgallus
mstewartgallus / sandbox.jsx
Created January 31, 2023 22:43
I think I want something like this for sandboxing blog comments. I feel like it might break horribly though.
import * as React from "react";
const empty = `<!DOCTYPE>
<html>
<body>
</body>
</html>
`;
export const Sandbox = ({children}) => {
@mstewartgallus
mstewartgallus / ceskusecase.js
Created January 25, 2023 04:14
class Control {
to(name, rest) {
return new LetControl(name, this, rest);
}
apply(x) {
return new ApplyControl(this, x);
}
map(f) {
@mstewartgallus
mstewartgallus / weirdness.js
Created January 12, 2023 16:51
You can actually replace the current page with a blob. However, this page as a blob has very limited permissions.
document.location.replace(URL.createObjectURL(new Blob([`<!DOCTYPE html>
<html>
<head>
<title>Lol</title>
<script>
history.replaceState(null, null, "lol");
</script>
</head>
<body>
lol lmao