jcreedcmu

{-# OPTIONS --without-K --rewriting #-}
module Coglue {n : Set} where

open import HoTT hiding (Span ; S ; span=)

postulate
  # : Set
  ι : n → #

record Span : Set₁ where

jcreedcmu

const foo = {hello: "struff", q: {bar: "bar", baz: "baz"}};

type Replace<T, U> = {
  [P in keyof U]: U[P] extends string ? T : Replace<T, U[P]>;
}
type FooType = typeof foo;
type GenFoo<T> = Replace<T, FooType>;

function xform(input: GenFoo<string>): GenFoo<number> {

jcreedcmu

////////
// The vm module lets you run a string containing javascript code 'in
// a sandbox', where you specify a context of global variables that
// exist for the duration of its execution. This works more or less
// well, and if you're in control of the code that's running, and you
// have a reasonable protocol in mind// for how it expects a certain
// context to exist and interacts with it --- like, maybe a plug-in
// API for a program, with some endpoints defined for it that do
// useful domain-specific things --- your life can go smoothly.

jcreedcmu

{-# OPTIONS --without-K #-}
module InternalCategories where

open import HoTT hiding ( [_] )

record Cat (X : Set) : Set₁ where
  constructor cat
  field
    hom : X → X → Set
    _⋆_ : {x y z : X} → hom x y → hom y z → hom x z

jcreedcmu

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

-- This agda file contains my understanding/reconstruction/digestion of the ideas in
-- "A Presheaf Model of Parametric Type Theory" (Bernardy, Coquand, Moulin, 2015)
-- and Moulin's thesis
-- "Internalizing Parametricity"
-- http://publications.lib.chalmers.se/records/fulltext/235758/235758.pdf

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

jcreedcmu

I think I may have figured out the solution to a puzzle I put to
myself a few years ago, about generating random noise subject to some
particularly persnickety constraints.

Is there a random distribution of functions ℝ² → ℝ such that

(a) it's reasonably efficient to compute samples locally. Let's say we
can (after fixing a sample) that we can compute f(x, y) in constant
expected time.
(b) the distribution is rotation/translation invariant

jcreedcmu

{-# OPTIONS --without-K #-}
module RtnzDatabase where

open import HoTT

Σ' = Σ -- renaming just so we can make the following syntax decl
syntax Σ' A (λ x → B) = ∃ x ∶ A · B

FinSet = Set -- not really constraining to finite, just conveying intent

jcreedcmu

{"message":[144,57,21],"delta_us":0}
{"message":[144,57,0],"delta_us":305940}
{"message":[144,59,30],"delta_us":49327}
{"message":[144,59,0],"delta_us":338871}
{"message":[144,45,28],"delta_us":15964}
{"message":[144,60,39],"delta_us":25149}
{"message":[176,64,127],"delta_us":69250}
{"message":[144,52,31],"delta_us":230901}
{"message":[144,45,0],"delta_us":273879}
{"message":[144,52,0],"delta_us":44989}

jcreedcmu

{-# 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

;; 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 ")")