mstewartgallus’s gists

mstewartgallus / antisymmetric.txt

Last active July 26, 2026 23:33

Draft of antisymmetric logic

	Trying to figure out an odd kind of anti-symmetric calculus. Just very awkward to work with substructural logic.

	The trouble is that a double category sort of thing where the source object is the composition of several spans is really awkward to work with. Anti-symmetry is an attempt to approach things from the opposite perspective of apartness instead of equivalence and groupoids.

	t ::= 𝔻 \| 1 \| t₀ ∧ t₁ \| ⋆t

	─── id
	t ⊢ t

	Γ, t₀, Δ, t₁, Σ, t₂, Π ⊢ t₃

mstewartgallus / alternating.txt

Last active July 26, 2026 14:05

Relational calculus with semantics in a Z/2-graded "alternating multicategory"

	Relational calculus with hopes to give semantics in a kind of "alternating multicategory".

	I want to work with the exterior algebra ⋀ 𝔽₂[S] (or possibly formal power series ⋀ 𝔽₂[[S]] or algebraic power series ⋀ 𝔽₂(S)) as a nice way of working with set-set apartness relations and denotational semantics.

	I want a kind of operad for my set of terms S that composes well with the exterior algebra ⋀ 𝔽₂[S]. I think I require some form of "super operads" but finite fields are already really confusing. Not really happy that enriching over super vector spaces seems to be required.

	I suspect you basically want a kind of graded closed semi-additive category but maybe a little weaker.

	Symmetry is a natural isomorphism.

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 / 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 / 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 / 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 / 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 / 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 / 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 / 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}) => {

Molly Stewart-Gallus mstewartgallus