Lathe Morphisms
Lathe Morphisms for Racket isn’t much yet, but it’s going to be a library centering around category theory and foundational mathematics. We recognize not everyone is going to want to wade through specialized mathematical terminology, so as we design and document Lathe Morphisms, we hope to first consider the needs of those people who have little choice.
This goal of writing a category theory library for Racket can take many forms. Even within the field of category theory, it’s common to investigate alternative ways of formalizing the basic concepts. Then when trying to represent category theory concepts in a programming language, it’s possible to approach that task with varying degrees of fidelity to the matematical concepts. Finally, Racket is a programming language that embraces language extension and polyglot programming, and different ways of programming in Racket (especially different #langs) may justify different API design approaches.
In Lathe Morphisms for Racket, we choose our naming conventions to make room for a number of different approaches all at once. In particular, we’re making room for approaches that have support for a form of classical reasoning, even though for now we just have a couple of approaches based on a constructive form of category theory without proof witnesses.
Throughout this library, we sometimes need to ensure that more than one value passed to a function are all close enough together. For functions like these, we consider one of the values v to be the source of truth, and we check that the others are (ok/c v). This calls the value’s atomic-set-element-sys-accepts/c method if it has one, and otherwise it just uses any/c.
At its strictest, the implementation of a value’s ...-accepts/c method will tend to use match/c around some recursive calls to ok/c. At its most lenient, it can simply return any/c. Even for programs where the strictness of contracts is a priority, it’s advisable to be at least a lenient enough to allow for any impersonators that program’s contracts produce. Generally, concepts Lathe Morphisms offers like categories and functors can’t be impersonated in a way that’s actually an impersonator-of? the original, so they’ll be a kind of pseudo-impersonator. Lathe Morphisms doesn’t currently offer any pseudo-impersonators of its own, but programmers should watch out for at least the pseudo-impersonators they define themselves.
1.1 Functional-programming-based theories that are "mediary" for open extensibility |
1 Functional-programming-based theories
1.1 Functional-programming-based theories that are "mediary" for open extensibility
1.1.1 Mediary sets and their elements
(require lathe-morphisms/in-fp/mediary/set) | |
package: lathe-morphisms-lib |
1.1.1.1 Behavior of well-behaved set elements
syntax
syntax
(set-element-good-behavior getter-of-value-expr getter-of-accepts/c-expr)
getter-of-value-expr : (-> any/c)
getter-of-accepts/c-expr : (-> (flat-contract-accepting/c (getter-of-value-expr)))
match expander
(set-element-good-behavior getter-of-value-pat getter-of-accepts/c-pat)
procedure
v : any/c
procedure
(set-element-good-behavior-getter-of-value element-gb)
→ (-> any/c) element-gb : set-element-good-behavior?
procedure
(set-element-good-behavior-getter-of-accepts/c element-gb)
→
(-> (flat-contract-accepting/c (set-element-good-behavior-value element-gb))) element-gb : set-element-good-behavior?
Two set-element-good-behavior values are equal? if they contain equal? elements.
procedure
(set-element-good-behavior-value element-gb) → any/c
element-gb : set-element-good-behavior?
procedure
(set-element-good-behavior-with-value/c value/c) → contract?
value/c : contract?
procedure
→ contract? mss : mediary-set-sys?
1.1.1.2 Atomic set elements
procedure
v : any/c
procedure
v : any/c
value
: (struct-type-property/c atomic-set-element-sys-impl?)
procedure
(atomic-set-element-sys-good-behavior element)
→ set-element-good-behavior? element : atomic-set-element-sys?
procedure
(atomic-set-element-sys-accepts/c element)
→ (flat-contract-accepting/c element) element : atomic-set-element-sys?
procedure
(make-atomic-set-element-sys-impl-from-good-behavior good-behavior)
→ atomic-set-element-sys-impl? good-behavior : (-> atomic-set-element-sys? set-element-good-behavior?)
When good-behavior is called with an element element to obtain a set-element-good-behavior? value, the result of calling the set-element-good-behavior-getter-of-value getter of that value should be element.
Most of the time, make-atomic-set-element-sys-impl-from-good-behavior is more general-purpose than necessary, and make-atomic-set-element-sys-impl-from-contract can be used instead.
procedure
(make-atomic-set-element-sys-impl-from-contract accepts/c)
→ atomic-set-element-sys-impl?
accepts/c :
(->i ([element atomic-set-element-sys?]) [_ (element) (flat-contract-accepting/c element)])
While this is more convenient, make-atomic-set-element-sys-impl-from-good-behavior is technically more general-purpose. That alternative gives more comprehensive control over things like the eq? identity of various values, the timing of side effects, the particular prop:procedure-implementing structs that implement the procedures, the presence of impersonators in various places, and whether the set-element-good-behavior-getter-of-value getter returns element (which it should) or some other value (which it shouldn’t). For an API-compliant pure FP style with little use of impersonators, there’s virtually no need for that extra generality.
1.1.1.3 Mediary sets themselves
procedure
(mediary-set-sys? v) → boolean?
v : any/c
procedure
v : any/c
value
: (struct-type-property/c mediary-set-sys-impl?)
The only thing that makes an element well-behaved is that it can recognize when another value is close enough to it.
The behavior of a mediary set itself is limited to recognizing its values.
procedure
(mediary-set-sys-element/c mss) → contract?
mss : mediary-set-sys?
procedure
(make-mediary-set-sys-impl-from-contract element/c)
→ mediary-set-sys-impl? element/c : (-> mediary-set-sys? contract?)
1.1.1.4 Utilities based on mediary sets
procedure
(ok/c example) → (flat-contract-accepting/c example)
example : any/c
1.2 Sets
(require lathe-morphisms/in-fp/set) | |
package: lathe-morphisms-lib |
procedure
v : any/c
procedure
(set-sys-impl? v) → boolean?
v : any/c
value
procedure
(set-sys-element/c ss) → contract?
ss : set-sys?
procedure
(set-sys-element-accepts/c ss element)
→ (flat-contract-accepting/c element) ss : set-sys? element : (set-sys-element/c ss)
procedure
(make-set-sys-impl-from-contract element/c element-accepts/c) → set-sys-impl? element/c : (-> set-sys? contract?)
element-accepts/c :
(->i ([ss set-sys?] [element (ss) (set-sys-element/c ss)]) [_ (element) (flat-contract-accepting/c element)])
procedure
(makeshift-set-sys-from-contract element/c element-accepts/c) → set-sys? element/c : (-> contract?)
element-accepts/c :
(->i ([element (element/c)]) [_ (element) (flat-contract-accepting/c element)])
1.3 Categories
(require lathe-morphisms/in-fp/category) | |
package: lathe-morphisms-lib |
procedure
(category-sys? v) → boolean?
v : any/c
procedure
(category-sys-impl? v) → boolean?
v : any/c
value
prop:category-sys : (struct-type-property/c category-sys-impl?)
procedure
cs : category-sys?
procedure
(category-sys-object/c cs) → contract?
cs : category-sys?
procedure
(category-sys-morphism-set-sys cs s t) → set-sys?
cs : category-sys? s : (category-sys-object/c cs) t : (category-sys-object/c cs)
procedure
(category-sys-morphism/c cs s t) → contract?
cs : category-sys? s : (category-sys-object/c cs) t : (category-sys-object/c cs)
procedure
(category-sys-object-identity-morphism cs object) → (category-sys-morphism/c cs object object) cs : category-sys? object : (category-sys-object/c cs)
procedure
(category-sys-morphism-chain-two cs a b c ab bc) → (category-sys-morphism/c cs a c) cs : category-sys? a : (category-sys-object/c cs) b : (category-sys-object/c cs) c : (category-sys-object/c cs) ab : (category-sys-morphism/c cs a b) bc : (category-sys-morphism/c cs b c)
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the source to the target of each morphism. Composition in category theory literature is most often written with its arguments the other way around.
procedure
(make-category-sys-impl-from-chain-two object-set-sys morphism-set-sys object-identity-morphism morphism-chain-two) → category-sys-impl? object-set-sys : (-> category-sys? set-sys?)
morphism-set-sys :
(->i ( [cs category-sys?] [s (cs) (category-sys-object/c cs)] [t (cs) (category-sys-object/c cs)]) [_ set-sys?])
object-identity-morphism :
(->i ([cs category-sys?] [object (cs) (category-sys-object/c cs)]) [_ (cs object) (category-sys-morphism/c cs object object)])
morphism-chain-two :
(->i ( [cs category-sys?] [a (cs) (category-sys-object/c cs)] [b (cs) (category-sys-object/c cs)] [c (cs) (category-sys-object/c cs)] [ab (cs a b) (category-sys-morphism/c cs a b)] [bc (cs b c) (category-sys-morphism/c cs b c)]) [_ (cs a c) (category-sys-morphism/c cs a c)])
The given method implementations should observe some algebraic laws. Namely, the morphism-chain-two operation should be associative, and object-identity-morphism should act as an identity element for it. In more symbolic terms (using a pseudocode DSL):
(#:for-all cs category-sys? a (category-sys-object/c cs) b (category-sys-object/c cs) ab (category-sys-morphism/c cs a b) (#:should-be-equal (morphism-chain-two cs a a b (object-identity-morphism cs a) ab) ab)) (#:for-all cs category-sys? a (category-sys-object/c cs) b (category-sys-object/c cs) ab (category-sys-morphism/c cs a b) (#:should-be-equal (morphism-chain-two cs a b b ab (object-identity-morphism cs b)) ab)) (#:for-all cs category-sys? a (category-sys-object/c cs) b (category-sys-object/c cs) c (category-sys-object/c cs) d (category-sys-object/c cs) ab (category-sys-morphism/c cs a b) bc (category-sys-morphism/c cs b c) cd (category-sys-morphism/c cs c d) (#:should-be-equal (morphism-chain-two cs a c d (morphism-chain-two cs a b c ab bc) cd) (morphism-chain-two cs a b d ab (morphism-chain-two cs b c d bc cd))))
procedure
(functor-sys? v) → boolean?
v : any/c
procedure
(functor-sys-impl? v) → boolean?
v : any/c
value
prop:functor-sys : (struct-type-property/c functor-sys-impl?)
procedure
(functor-sys-source fs) → category-sys?
fs : functor-sys?
procedure
(functor-sys-replace-source fs new-s) → functor-sys?
fs : functor-sys? new-s : category-sys?
procedure
(functor-sys-target fs) → category-sys?
fs : functor-sys?
procedure
(functor-sys-replace-target fs new-t) → functor-sys?
fs : functor-sys? new-t : category-sys?
procedure
(functor-sys-apply-to-object fs object)
→ (category-sys-object/c (functor-sys-target fs)) fs : functor-sys? object : (category-sys-object/c (functor-sys-source fs))
procedure
(functor-sys-apply-to-morphism fs a b ab)
→
(category-sys-morphism/c (functor-sys-target fs) (functor-sys-apply-to-object fs a) (functor-sys-apply-to-object fs b)) fs : functor-sys? a : (category-sys-object/c (functor-sys-source fs)) b : (category-sys-object/c (functor-sys-source fs)) ab : (category-sys-morphism/c (functor-sys-source fs) a b)
procedure
(make-functor-sys-impl-from-apply source replace-source target replace-target apply-to-object apply-to-morphism) → functor-sys-impl? source : (-> functor-sys? category-sys?) replace-source : (-> functor-sys? category-sys? functor-sys?) target : (-> functor-sys? category-sys?) replace-target : (-> functor-sys? category-sys? functor-sys?)
apply-to-object :
(->i ( [fs functor-sys?] [object (fs) (category-sys-object/c (functor-sys-source fs))]) [_ (fs) (category-sys-object/c (functor-sys-target fs))])
apply-to-morphism :
(->i ( [fs functor-sys?] [a (fs) (category-sys-object/c (functor-sys-source fs))] [b (fs) (category-sys-object/c (functor-sys-source fs))] [morphism (fs a b) (category-sys-morphism/c (functor-sys-source fs) a b)]) [_ (fs a b) (category-sys-morphism/c (functor-sys-target fs) (functor-sys-apply-to-object fs a) (functor-sys-apply-to-object fs b))])
When the replace methods don’t raise errors, they should observe the lens laws: The result of getting a value after it’s been replaced should be the same as just using the value that was passed to the replacer. The result of replacing a value with itself should be the same as not using the replacer at all. The result of replacing a value and replacing it a second time should be the same as just skipping to the second replacement.
Moreover, the replace methods should not raise an error when a value is replaced with itself. They’re intended only for use by functor-sys/c and similar error-detection systems, which will tend to replace a replace a value with one that reports better errors.
The other given method implementations should observe some algebraic laws. Namely, the apply-to-morphism operation should respect the identity and associativity laws of the category-sys-object-identity-morphism and category-sys-morphism-chain-two operations. In more symbolic terms (using a pseudocode DSL):
(#:for-all fs functor-sys? #:let s (functor-sys-source fs) #:let t (functor-sys-target fs) a (category-sys-object/c s) (#:should-be-equal (apply-to-morphism fs a a (category-sys-object-identity-morphism s a)) (category-sys-object-identity-morphism t (apply-to-object fs a)))) (#:for-all fs functor-sys? #:let s (functor-sys-source fs) #:let t (functor-sys-target fs) a (category-sys-object/c s) b (category-sys-object/c s) c (category-sys-object/c s) ab (category-sys-morphism/c s a b) bc (category-sys-morphism/c s b c) (#:should-be-equal (apply-to-morphism fs a c (category-sys-morphism-chain-two s a b c ab bc)) (category-sys-morphism-chain-two t (apply-to-object fs a) (apply-to-object fs b) (apply-to-object fs c) (apply-to-morphism fs a b ab) (apply-to-morphism fs b c bc))))
procedure
(functor-sys/c source/c target/c) → contract?
source/c : contract? target/c : contract?
The result is a flat contract as long as the given contracts are flat.
procedure
(makeshift-functor-sys s t apply-to-object apply-to-morphism) → (functor-sys/c (ok/c s) (ok/c t)) s : category-sys? t : category-sys? apply-to-object : (-> (category-sys-object/c s) (category-sys-object/c t))
apply-to-morphism :
(->i ( [a (category-sys-object/c s)] [b (category-sys-object/c s)] [ab (a b) (category-sys-morphism/c s a b)]) [_ (a b) (category-sys-morphism/c t (apply-to-object a) (apply-to-object b))])
This may be more convenient than defining an instance of prop:functor-sys.
The given procedures should satisfy algebraic laws. Namely, the apply-to-morphism operation should respect the identity and associativity laws of the category-sys-object-identity-morphism and category-sys-morphism-chain-two operations. In more symbolic terms (using a pseudocode DSL):
(#:for-all a (category-sys-object/c s) (#:should-be-equal (apply-to-morphism a a (category-sys-object-identity-morphism s a)) (category-sys-object-identity-morphism t (apply-to-object a)))) (#:for-all a (category-sys-object/c s) b (category-sys-object/c s) c (category-sys-object/c s) ab (category-sys-morphism/c s a b) bc (category-sys-morphism/c s b c) (#:should-be-equal (apply-to-morphism a c (category-sys-morphism-chain-two s a b c ab bc)) (category-sys-morphism-chain-two t (apply-to-object a) (apply-to-object b) (apply-to-object c) (apply-to-morphism a b ab) (apply-to-morphism b c bc))))
procedure
(functor-sys-identity endpoint)
→ (functor-sys/c (ok/c endpoint) (ok/c endpoint)) endpoint : category-sys?
procedure
(functor-sys-chain-two ab bc)
→
(functor-sys/c (ok/c (functor-sys-source ab)) (ok/c (functor-sys-target bc))) ab : functor-sys? bc : (functor-sys/c (ok/c (functor-sys-target ab)) any/c)
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the source to the target of each functor. Composition in category theory literature is most often written with its arguments the other way around.
procedure
v : any/c
procedure
v : any/c
value
: (struct-type-property/c natural-transformation-sys-impl?)
procedure
→ category-sys? nts : natural-transformation-sys?
procedure
(natural-transformation-sys-replace-endpoint-source nts new-es) → natural-transformation-sys? nts : natural-transformation-sys? new-es : category-sys?
procedure
→ category-sys? nts : natural-transformation-sys?
procedure
(natural-transformation-sys-replace-endpoint-target nts new-et) → natural-transformation-sys? nts : natural-transformation-sys? new-et : category-sys?
procedure
(natural-transformation-sys-endpoint/c nts) → flat-contract?
nts : natural-transformation-sys?
procedure
→ (natural-transformation-sys-endpoint/c nts) nts : natural-transformation-sys?
procedure
(natural-transformation-sys-replace-source nts new-s) → natural-transformation-sys? nts : natural-transformation-sys? new-s : (natural-transformation-sys-endpoint/c nts)
procedure
→ (natural-transformation-sys-endpoint/c nts) nts : natural-transformation-sys?
procedure
(natural-transformation-sys-replace-target nts new-t) → natural-transformation-sys? nts : natural-transformation-sys? new-t : (natural-transformation-sys-endpoint/c nts)
procedure
(natural-transformation-sys-apply-to-morphism nts a b ab) nts : natural-transformation-sys?
a :
(category-sys-object/c (natural-transformation-sys-endpoint-source nts))
b :
(category-sys-object/c (natural-transformation-sys-endpoint-source nts))
ab :
(category-sys-morphism/c (natural-transformation-sys-endpoint-source nts) a b)
procedure
(make-natural-transformation-sys-impl-from-apply endpoint-source replace-endpoint-source endpoint-target replace-endpoint-target source replace-source target replace-target apply-to-morphism) → natural-transformation-sys-impl? endpoint-source : (-> natural-transformation-sys? category-sys?)
replace-endpoint-source :
(-> natural-transformation-sys? category-sys? natural-transformation-sys?) endpoint-target : (-> natural-transformation-sys? category-sys?)
replace-endpoint-target :
(-> natural-transformation-sys? category-sys? natural-transformation-sys?)
source :
(->i ([nts natural-transformation-sys?]) [_ (nts) (natural-transformation-sys-endpoint/c nts)])
replace-source :
(->i ( [nts natural-transformation-sys?] [s (nts) (natural-transformation-sys-endpoint/c nts)]) [_ natural-transformation-sys?])
target :
(->i ([nts natural-transformation-sys?]) [_ (nts) (natural-transformation-sys-endpoint/c nts)])
replace-target :
(->i ( [nts natural-transformation-sys?] [s (nts) (natural-transformation-sys-endpoint/c nts)]) [_ natural-transformation-sys?])
apply-to-morphism :
(->i ( [nts natural-transformation-sys?] [a (nts) (category-sys-object/c (natural-transformation-sys-endpoint-source nts))] [b (nts) (category-sys-object/c (natural-transformation-sys-endpoint-source nts))] [ab (nts a b) (category-sys-morphism/c (natural-transformation-sys-endpoint-source nts) a b)]) [_ (nts a b ab) (category-sys-morphism/c (natural-transformation-sys-endpoint-target nts) (functor-sys-apply-to-object (natural-transformation-sys-source nts) a) (functor-sys-apply-to-object (natural-transformation-sys-target nts) b))])
When the replace methods don’t raise errors, they should observe the lens laws: The result of getting a value after it’s been replaced should be the same as just using the value that was passed to the replacer. The result of replacing a value with itself should be the same as not using the replacer at all. The result of replacing a value and replacing it a second time should be the same as just skipping to the second replacement.
Moreover, the replace methods should not raise an error when a value is replaced with itself. They’re intended only for use by natural-transformation-sys/c and similar error-detection systems, which will tend to replace a replace a value with one that reports better errors.
The other given method implementations should observe some algebraic laws. Namely, applying the apply-to-morphism operation to a composed morphism should be the same as applying it to just one composed part of that morphism and applying the source and target functors to the other parts so that it joins up. In more symbolic terms (using a pseudocode DSL):
(#:for-all nts natural-transformation-sys? #:let es (natural-transformation-sys-endpoint-source nts) #:let et (natural-transformation-sys-endpoint-target nts) #:let s (natural-transformation-sys-source nts) #:let t (natural-transformation-sys-target nts) a (category-sys-object/c es) b (category-sys-object/c es) c (category-sys-object/c es) ab (category-sys-morphism/c es a b) bc (category-sys-morphism/c es b c) (#:should-be-equal (apply-to-morphism nts a c (category-sys-morphism-chain-two es a b c ab bc)) (category-sys-morphism-chain-two t (functor-sys-apply-to-object s a) (functor-sys-apply-to-object s b) (functor-sys-apply-to-object t c) (functor-sys-apply-to-morphism s a b ab) (apply-to-morphism nts b c bc))) (#:should-be-equal (apply-to-morphism nts a c (category-sys-morphism-chain-two es a b c ab bc)) (category-sys-morphism-chain-two t (functor-sys-apply-to-object s a) (functor-sys-apply-to-object t b) (functor-sys-apply-to-object t c) (apply-to-morphism nts a b ab) (functor-sys-apply-to-morphism t b c bc))))
Using an infix notation where we infer most arguments and write (ab ; bc) for the category-sys-morphism-chain-two operation, these laws can be written like so:
s ab ; nts bc = nts (ab ; bc) = nts ab ; t bc
Using more math-style variable name choices:
F f ; alpha g = alpha (f ; g) = alpha f ; G g
In category theory literature, it’s common for natural transformations’ component functions to go from objects to morphisms, not morphisms to morphisms. We consider a natural transformation to act on an object by applying to its identity morphism. In that case the usual naturality square law looks like this:
F f ; alpha (id y) = alpha (id x) ; G f
We can derive that law like so:
F f ; alpha (id y) = alpha (f ; id y) = alpha f = alpha (id x ; f) = alpha (id x) ; G f
procedure
(natural-transformation-sys/c endpoint-source/c endpoint-target/c source/c target/c) → contract? endpoint-source/c : contract? endpoint-target/c : contract? source/c : contract? target/c : contract?
The result is a flat contract as long as the given contracts are flat.
procedure
(makeshift-natural-transformation-sys es et s t apply-to-morphism) → (natural-transformation-sys/c (ok/c es) (ok/c et) (ok/c s) (ok/c t)) es : category-sys? et : category-sys? s : (functor-sys/c (ok/c es) (ok/c et)) t : (functor-sys/c (ok/c es) (ok/c et))
apply-to-morphism :
(->i ( [a (category-sys-object/c es)] [b (category-sys-object/c es)] [ab (a b) (category-sys-morphism/c es a b)]) [_ (a b ab) (category-sys-morphism/c et (functor-sys-apply-to-object s a) (functor-sys-apply-to-object t b))])
This may be more convenient than defining an instance of prop:natural-transformation-sys.
The given procedure should satisfy algebraic laws. Namely, applying the apply-to-morphism operation to a composed morphism should be the same as applying it to just one composed part of that morphism and applying the source and target functors to the other parts so that it joins up. In more symbolic terms (using a pseudocode DSL):
(#:for-all a (category-sys-object/c es) b (category-sys-object/c es) c (category-sys-object/c es) ab (category-sys-morphism/c es a b) bc (category-sys-morphism/c es b c) (#:should-be-equal (apply-to-morphism a c (category-sys-morphism-chain-two es a b c ab bc)) (category-sys-morphism-chain-two t (functor-sys-apply-to-object s a) (functor-sys-apply-to-object s b) (functor-sys-apply-to-object t c) (functor-sys-apply-to-morphism s a b ab) (apply-to-morphism b c bc))) (#:should-be-equal (apply-to-morphism a c (category-sys-morphism-chain-two es a b c ab bc)) (category-sys-morphism-chain-two t (functor-sys-apply-to-object s a) (functor-sys-apply-to-object t b) (functor-sys-apply-to-object t c) (apply-to-morphism a b ab) (functor-sys-apply-to-morphism t b c bc))))
For a little more discussion about how our choice of natural transformation laws relates to the more common naturality square law, see the documentation for make-natural-transformation-sys-impl-from-apply.
procedure
(natural-transformation-sys-identity endpoint)
→
(natural-transformation-sys/c (ok/c (functor-sys-source endpoint)) (ok/c (functor-sys-target endpoint)) (ok/c endpoint) (ok/c endpoint)) endpoint : functor-sys?
procedure
(natural-transformation-sys-chain-two ab bc)
→
(natural-transformation-sys/c (ok/c (natural-transformation-sys-endpoint-source ab)) (ok/c (natural-transformation-sys-endpoint-target ab)) (ok/c (natural-transformation-sys-source ab)) (ok/c (natural-transformation-sys-target bc))) ab : natural-transformation-sys?
bc :
(natural-transformation-sys/c (ok/c (natural-transformation-sys-endpoint-source ab)) (ok/c (natural-transformation-sys-endpoint-target ab)) (ok/c (natural-transformation-sys-target ab)) any/c)
If all the algebraic structures involved obey their laws, then the way this natural transformation transforms a morphism that’s composed from two morphisms is equivalent to applying the first natural transformation to the first part of the morphism, applying the second natural transformation to the second part of the morphism, and composing the results. Moreover, every morphism is the composition of itself and an identity morphism, so this specification determines the behavior on all morphisms. However, if any of the algebraic structures involved doesn’t obey its laws, this operation may leak some Lathe Morphisms implementation details that are subject to change.
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the source to the target of each natural transformation. Composition in category theory literature is most often written with its arguments the other way around.
procedure
(natural-transformation-sys-chain-two-along-end ab bc)
→
(natural-transformation-sys/c (ok/c (natural-transformation-sys-endpoint-source ab)) (ok/c (natural-transformation-sys-endpoint-target bc)) (ok/c (functor-sys-chain-two (natural-transformation-sys-source ab) (natural-transformation-sys-source bc))) (ok/c (functor-sys-chain-two (natural-transformation-sys-target ab) (natural-transformation-sys-target bc)))) ab : natural-transformation-sys?
bc :
(natural-transformation-sys/c (ok/c (natural-transformation-sys-endpoint-target ab)) any/c any/c any/c)
This composition operation is written in diagrammatic order, where in the process of reading off the arguments from left to right, we proceed from the endpoint source to the endpoint target of each natural transformation. Composition in category theory literature is most often written with its arguments the other way around.