jcreedcmu

export function range(n) {
  const rv = [];
  for (let i = 0; i < n; i++)
	 rv.push(i);
  return rv;
}

const r = Math.random;
type Point = {x: number, y: number};

jcreedcmu

module RelationList (A : Set)  where

-- Converse of relation
converse : (A → A → Set) → (A → A → Set)
converse R a a' = R a' a

-- A list of things (a1, a2, ... an) with relations
-- u -R-> a1 -R-> a2 -R-> ... -R-> an -R-> v
data Rist' (R : A → A → Set) (v : A) : (u : A) → Set where
  rnil : {u : A} → (r : R u v) → Rist' R v u

jcreedcmu

{-# OPTIONS --without-K #-}
open import HoTT

module b where

A : Set
A = ℕ

rev : (A → A → Set) → (A → A → Set)
rev R a a' = R a' a

jcreedcmu

module DagTypes where

data Unit : Set where
  * : Unit

data Void : Set where

data Sum (A B : Set) : Set where
  inl : A → Sum A B
  inr : B → Sum A B

jcreedcmu

@media (min-width: 1024px) {
    .tabs-bar {display: flex; width: 785px; margin-left: calc(25% + 155px); z-index: 1;}
	.columns-area {width: calc(50% + 300px); margin: -60px auto auto;}
	.column {display: none;}
	.column:last-child {display: flex; min-width: 800px; margin-top: 55px;}
}

a[data-preview-title-id="column.community"] {
    display: none;
}

jcreedcmu

function tmap<T, U>(f : (x : T) => U, xss: T[][]): U[][] {
  return xss.map(xs => xs.map(x => f(x)));
}

function table<T>(xss: string[][], extra? : string): string {
  const es = extra || '';
  let buf = `<table ${es}>`;
  xss.forEach(xs => {
	 buf += "<tr>";
	 xs.forEach(x => {

jcreedcmu

{-# OPTIONS --rewriting #-}
module a where

infix 30 _↦_
postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i

{-# BUILTIN REWRITE _↦_ #-}

data Foo : Set where

jcreedcmu

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

open import HoTT

-- The type of categories whose set of objects is X
record Cat (X : Set) : Set₁ where
  constructor cat
  field
    hom : X → X → Set

jcreedcmu

type Rec = {
  'text': string,
  'bool': boolean
};

type Un =
  | {t: 'text', v: string}
  | {t: 'bool', v: boolean};

type Datum<K, V> = { t: K, v: V };

jcreedcmu

type Union =
  { type: 'A', a: string } |
  { type: 'B', b: number }

type FilterType<T, K> = (T extends { type: K } ? T : never);
type RemoveType<T, K> = (T extends K ? never : T);

type MappedUnion = {[P in Union['type']]: RemoveTypeFromRecord<FilterType<Union, P>, 'type'>};

type MappedUnionTarget = {