phantamanta44

	absurd	adjunction	affine connection	Agda	axiom	axiom of choice	baba	blahaj	category	cobordism	cofinality	coherence	composition	contractible	coproduct	cosheaf	directed graph	emacs	embedding	equivalence	extensionality	fibration	functorial	groupoid	hcomp	holonomy	homothety	homotopy	Hopf fibration	identity	induction	infinity groupoid	interval	loop space	monadicity	monodromy	parallel transport	path induction	path over path	proof	proof assistant	proof tree	proposition	pullback	pushout	quotient	recursion	reflexivity	simplex	smugcube	substitution	suspension	torus	total space	transport	truncation	type	type theory	ultracategory	univalence	universe	variable	whiskering	yoneda lemma

I hereby claim:

To claim this, I am signing this object:

	mod FANCY-VENDING is
	--- a single sort Q of states
	sort Q .

	--- a state may have no tokens...
	op ø : -> Q [ctor] .
	--- ...or it may have one token of some kind...
	ops $ $c q qc m&m orr cok : -> Q [ctor] .
	--- ...or it may be the union of two such states
	op _ _ : Q Q -> Q [ctor assoc comm id: ø] .

	module Lib.Cat where

	open import Agda.Primitive using (Level; lsuc; _⊔_)
	open import Relation.Binary.PropositionalEquality public
	open import Lib.Eq using (subst-dep₂)

	private
	variable
	ℓ ℓʹ : Level

	#!/usr/bin/env python3

	from abc import ABC
	from collections import defaultdict
	import itertools
	import sys
	from typing import Any, Iterable, Iterator, Optional, cast

	class Word(ABC):
	pass

	module Main where

	import MiniKanren

	-- r = n + 1
	peanoSuccO :: Term -> Term -> Goal
	peanoSuccO n r = r === Val (Cons n (Val Nil))

	-- r = n - 1
	peanoPredO :: Term -> Term -> Goal

	from multiprocessing import Pool
	from random import random

	import matplotlib.pyplot as plt
	import pandas as pd
	from tqdm import tqdm

	TIER_CNT = 4
	WORKER_CNT = 8
	SIM_CNT = 1_000_000

	package xyz.phanta.forgeveryfast.coremod.engine;

	import net.minecraft.launchwrapper.IClassTransformer;
	import net.minecraft.launchwrapper.LaunchClassLoader;
	import org.objectweb.asm.ClassReader;
	import org.objectweb.asm.ClassWriter;
	import org.objectweb.asm.Handle;
	import org.objectweb.asm.Opcodes;
	import org.objectweb.asm.tree.*;
	import xyz.phanta.forgeveryfast.coremod.engine.injector.MixinInjector;

	def cycle(elems):
	mapping = { elems[i]: elems[(i + 1) % len(elems)] for i in range(len(elems)) }
	return lambda e: mapping[e] if e in mapping else e

	def compose(f, g):
	return lambda e: f(g(e))

	def cmp_list(a, b):
	return all(a[i] == b[i] for i in range(len(a)))

	/**
	* Represents a parameterized type. Unfortunately necessary because the JVM doesn't support
	* reified generics in all cases.
	*/
	@SuppressWarnings("unchecked")
	public class TypeToken<T> {

	/**
	* The type represented by this type token.
	*/