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' : ℕ

Trebor-Huang

{-# OPTIONS --cubical --no-import-sorts --postfix-projections -W ignore #-}
module freeCCC where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit using (Unit; isPropUnit; isSetUnit)
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; isSetBool)
open import Cubical.Data.Sum using (_⊎_; inr; inl)
open import Cubical.Data.Sigma using (Σ; _×_; ΣPathP)