Jademaster

import math
from statistics import mean
from PIL import Image, ImageColor, ImageDraw
import sys
import numpy as np
import random

# Copying/cooking my own version Akiyoshi Kitaoka's amazing art (see https://www.ritsumei.ac.jp/~akitaoka/index-e.html)
filename='bird.png'
img = Image.open(filename)

Jademaster

import breeze.linalg._
import breeze.linalg.LU.primitive.LU_DM_Impl_Double
import doodle.core._
import doodle.java2d._
import doodle.syntax.all._
import cats.effect.unsafe.implicits.global
import doodle.image._
import doodle.image.syntax._
import doodle.image.syntax.all.ImageOps
import doodle.image.syntax.image.ImageOps

Jademaster

-- this file implements the Grothendieck construction and its inverse for functions i.e.\ the equivalence between functions f : X -> Set and functions \int f -> X. In the language of functional programming, this gives a reversible procedure for turning dependent types into function types.

-- finite sets with n elements

  
-- just a dependent type
import Data.Vect

Deptype :Type -> Type
Deptype x = x -> Type

Jademaster

data Mu : (pattern : Type -> Type) -> Type where
    In : {f: Type -> Type} -> f (Mu f) -> Mu f

data TwoOps x a = Val x | Addunit | Mulunit | Add a a | Mul a a

Functor (TwoOps x) where
  map f (Val y) = Val y
  map f (Addunit) = Addunit
  map f (Mulunit) = Mulunit
  map f (Add a1 a2) = Add (f a1) (f a2)

Jademaster

import matplotlib.pyplot as plt
import numpy as np
import math 
from PIL import Image

#this code takes a matrix M, regards it as a weighted graph where the entry M_ij indicates the weight between vertex i and vertex j. The free category on this graph is computed using the geometric series formula F(M) = Sum_{n geq 0} M^n with operations valued in the min plus semiring. The function freemetricspace(M,res) computes this formula to the first res terms. In words, this computes the shortest paths which occur in <= n steps.

#this function computes naive matrix multiplication in the min plus semiring
def mult(m1,m2):
  assert (m1.shape[1] == m2.shape[0]), "shape mismatch"