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

Trebor-Huang

from functools import lru_cache

class Map:
    def __init__(self, f, iterable):
        self.data = (f, iterable)

    def __iter__(self):
        for i in self.data[1]:
            yield self.data[0](i)

Trebor-Huang

module _ where
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Fin using (Fin) renaming (zero to 𝕫; suc to 𝕤_)
open import Data.Vec using (Vec; []; [_]; _∷_; tail; map; allFin) renaming (lookup to _!_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Data.Vec.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

variable
  n m n' : ℕ