LeeeeT

# Map f = (a -> b) -> f a -> f b

# Id f = a -> f a

# Join f = f (f a) -> f a

# Bind f = f a -> (a -> f b) -> f b

# Then f = f a -> f b -> f b

LeeeeT

# Map f = (a -> b) -> f a -> f b

# Id f = a -> f a

# Join f = f (f a) -> f a

# Bind f = f a -> (a -> f b) -> f b

# TakeAfter f = f a -> f b -> f b

LeeeeT

from dataclasses import dataclass
from itertools import count


type Name = int


name = count()

LeeeeT

from dataclasses import dataclass
from itertools import count


type Name = int


name = count()

LeeeeT

from collections.abc import Callable
from dataclasses import dataclass
from itertools import count
from typing import Any


type Name = int


name = count(0)

LeeeeT

from dataclasses import dataclass
from itertools import count


type Name = int


name = count(0)

LeeeeT

from collections.abc import Callable
from dataclasses import dataclass
from typing import Any


type Term[T] = Var[T] | Typ[T] | Lam[T] | Fun[T] | App[T]


@dataclass(frozen=True)
class Var[T]:

LeeeeT

# Algebra f a = f a → a
# Fix f = ∀x. Algebra f x → x

# Coalgebra f a = a → f a
# Cofix f = ∃x. x × Coalgebra f x

# ListF a x = 1 + a × x
# List a = Fix (ListF a)
# Colist a = Cofix (ListF a)

LeeeeT

This script simulates IO (print and input) in a pure functional manner using a coinductive data structure.

---

Python-compatible generator:

Generator yield send return = ∃state . state × (state → return + yield × (send → state))

With the point functor:

LeeeeT

P ⊢ Q
----- →-Intro
P → Q


P → Q        P
-------------- →-Elim
Q