Trebor-Huang

#import "@preview/cetz:0.3.1" as cetz
#set page(width: auto, height: auto)
// A fixed offset vector in RR^5
#let offset = (
  0.012445987628374,
  0.049637456817326,
  0.291638765345987,
  0.084127469734981,
  0.000249356192837
)

Trebor-Huang

from collections import OrderedDict
import re

def subst(substitution, expr):
  return tuple(token
    for t0 in expr
    for token in (substitution[t0] if t0 in substitution else [t0]))

def decompress(mand, idents, cproof):
  """Decompresses a proof."""

Trebor-Huang

// *** Jump to the bottom for example usage ***

#set page(paper: "a5")
#let Lam(var, body) = ("Lam", var, body)
#let App(fun, arg) = ("App", fun, arg)

// An elaborate pretty printer because I'm bored

#let print-var(str) = if str.starts-with("@") {
  $x_#str.slice(1)$  // generated variable name

Trebor-Huang

from abc import ABC, abstractmethod
from dataclasses import dataclass
from functools import cached_property

@dataclass(frozen=True)
class SimplexMap:
  """A sSet map symbol, mathematically defined as a
  monotone map of ordered finite sets. Represented as a
  tuple of natural numbers, where `l[i]` represents the
  number of elements mapped to `i`."""

Trebor-Huang

open import Agda.Builtin.Equality

-- Some familiar results about equality

UIP : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
UIP x y refl refl = refl

coerce : {A : Set} (B : A → Set)
  → {x y : A} → x ≡ y
  → B x → B y

Trebor-Huang

{-# OPTIONS --cubical #-}
module natmod where
open import Cubical.Foundations.Prelude

data Ctx : Type
data _⊢_ : Ctx → Ctx → Type
data Ty : Ctx → Type
data Tm : Ctx → Type
-- This is halfway between EAT and GAT.
-- GAT is hard! Why is EAT so easy?

Trebor-Huang

{-# OPTIONS --cubical #-}
module HitPuzzle where
open import Cubical.Foundations.Everything
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

data Perm : Type → Type₁ where

Trebor-Huang

{-# OPTIONS --postfix-projections #-}
open import Agda.Primitive
open import Data.Product
module Polynomial where

variable
  X I O : Set

record Poly : Set₁ where
  -- A polynomial is an expression

Trebor-Huang

structure Pprop : Type where
  pos : Prop
  neg : Prop
  syn : pos → neg → False := by intros; assumption
namespace Pprop

instance : CoeSort Pprop Prop := ⟨Pprop.pos⟩
instance : Coe Bool Pprop where
  coe
  | true => {pos := True, neg := False}

Trebor-Huang

{-# OPTIONS --cubical -Wignore #-}
module lccc where
open import Cubical.Foundations.Prelude

data Obj : Type
data Hom : Obj → Obj → Type

variable
  A B C D X Y : Obj
  f g h u v e : Hom A B