jcreedcmu’s gists

jcreedcmu / foo.sml

Last active August 12, 2019 12:18

fun with higher order functors

	(* Plain old ordinary monad *)
	signature MONAD = sig
	type 'x t
	val return: 'x -> 'x t
	val bind : 'x t -> ('x -> 'y t) -> 'y t
	end

	(*
	Monad indexed by one other type. Not even as fancy as "indexed monads
	a la Atkey" (for which see

jcreedcmu / gist:dc94268bee8a84a80d57c5ac53a67b2c

Created March 30, 2017 23:27

disorganized notes on 3-coloring lambda terms

	it follows from 4ct that:
	[[[
	every normal term with one free variable has at least one of these colorings:
	0

	every normal term with two free variables has at least one of these colorings:
	12
	21

	every normal term with three free variables has at least one of these colorings:

jcreedcmu / Jq.agda

Last active May 14, 2017 01:46

Jq-like update in agda

	module Jq where

	{-

	functional lenses are neat.

	https://medium.com/@dtipson/functional-lenses-d1aba9e52254
	https://bartoszmilewski.com/category/lens/
	https://bartoszmilewski.com/2015/07/13/from-lenses-to-yoneda-embedding/
	https://twanvl.nl/blog/haskell/cps-functional-references

jcreedcmu / Contractible.agda

Last active May 26, 2017 13:18

The pushout of a span of contractible types is contractible

	{-# OPTIONS --without-K --rewriting #-}

	module Contractible where

	open import HoTT hiding ( Type ; _$_ )

	Type = Type0

	idp[] : {A : Type} (a b : A) (path : a == b) → idp == path [ (λ c → a == c) ↓ path ]
	idp[] a b idp = idp

jcreedcmu / gist:5b790a66a1418ce6a614bfbc6af51941

Created June 19, 2017 23:27

Loeb's theorem

jcreedcmu / gist:171061624e71a172975c376048043350

Created July 19, 2017 13:19

	{-# OPTIONS --without-K --rewriting --type-in-type #-}

	module Leibniz where

	open import HoTT

	{- Here's Leibniz equality.
	Two things a and b are equal if for every property P that a satisfies, b satisfies it also. -}
	module _ {A : Set} where
	_=#_ : (a b : A) → Set

jcreedcmu / anim.py

Last active July 26, 2017 01:20

	import bpy
	import mathutils
	import math
	from math import radians
	from mathutils import Matrix

	# When DEBUG = True, this sets up a change-frame callback
	# that modifies the scene to be the current state of the animation,
	# deleting every object that doesn't have the 'pres' attribute set.

jcreedcmu / swap-implicit.el

Created October 16, 2017 20:52

	;; if the binding at point is implicit, make it explicit, and vice-versa
	(defun jcreed-swap-agda-implicit ()
	(interactive)
	(save-excursion
	(if (re-search-backward "[({]" nil t)
	(let ((ms (match-string 0)))
	(cond
	((equal ms "(")
	(replace-match "{")
	(re-search-forward ")")

jcreedcmu / gist:576e0e42ecdd5d4a2526c39ce307a3ca

Created December 11, 2017 00:04

Internalized parametricity

	{-# OPTIONS --without-K --rewriting #-}
	module Sharp where

	open import HoTT hiding ( O; Path; _*_ )

	module WithArity (C : Set) where
	postulate
	𝕀 : Set
	η : C → 𝕀
	Path : ∀ {ℓ} (A : 𝕀 → Set ℓ) (a : (c : C) → A (η c)) → Set ℓ

jcreedcmu / song.json

Created December 16, 2017 15:52 — forked from anonymous/song.json