closed

The free closed markov category, i.e. with copy, discard, exponentials and products that are not strictly associative.

Summary

Ty	A closed type is a biclosed type in a symmetric category where left and right exponentials coincide, i.e. X << Y == X ** Y == Y >> X.
Exp	An exponential object in a markov category.
Product	The product of a tuple of types, which is not strictly associative, called with * in the binary case.
TermBase	A term in the internal language of a closed category, i.e. a lambda term which need not be linear: this module implements closed markov categories by design, so a variable may be copied and discarded, i.e. occur any number of times.
Constant	A constant term, evaluated in a context by discarding it.
Variable	A variable, evaluated in a context by discarding the other variables.
Application	The application func(args) of a term to another.
Abstraction	The abstraction var.cod(lambda var: body) of a variable in a term, which need not occur in it or may occur several times.
Compound	A term built from other terms, its parts: a Tuple, a Projection or a Let.
Tuple	The tupling of terms, its codomain is the Product of theirs.
Projection	The projection onto one factor of a term with a Product type, which evaluation interprets by discarding the other factors.
Let	The evaluation of an expression term, binding a tuple of variables to the factors of its result inside a body term, i.e. the statement let (x, ..., z) = expression in body.
Substitution	The simultaneous, capture-avoiding substitution of terms for variables.
Diagram	A closed diagram is both a markov and a biclosed diagram.
Box	A closed box is a markov and biclosed box in a closed diagram.
Eval	The evaluation of an exponential type.
Coeval	The coevaluation of an exponential type, i.e. the dagger of an Eval.
Curry	The currying of a closed diagram, linear when its argument is.
Pack	The canonical isomorphism from the tensor of the factors of a Product type to the product itself.
Unpack	The canonical isomorphism from a Product type to the tensor of its factors, i.e. the dagger of Pack.
Discard	A markov discard in a closed category.
Sum	A markov sum is a symmetric sum and a markov box, linear when every term is.
Functor	A closed functor is a markov functor that preserves evaluation, currying and packing.
CMap	alias of CMap[Diagram]

Functions

let	Bind the result of an expression term inside the body of a Python function, whose variable names are given by introspection and whose types are the factors of the codomain of expression.

Axioms

Diagram.curry() and Diagram.uncurry() are inverses.

>>> x, y, z = map(Ty, "xyz")
>>> f, g = Box('f', x, z << y), Box('g', x @ y, z)

>>> Equation(f.uncurry().curry(), f).draw(
...     doctest='docs/_static/closed/curry-left.svg', margins=(0.1, 0.05))

>>> Equation(g.curry().uncurry(), g).draw(
...     doctest='docs/_static/closed/uncurry.svg')