:: YELLOW20 semantic presentation

K154() is M2( bool K150())
K150() is set
bool K150() is non empty set
K116() is set
bool K116() is non empty set
bool K154() is non empty set
{} is set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Function-yielding V37() set
1 is non empty set
{{},1} is set
proj1 {} is set
proj2 {} is set
A1 is non empty transitive with_units reflexive AltCatStr
A2 is non empty transitive with_units reflexive AltCatStr
the carrier of A1 is non empty set
the carrier of A2 is non empty set
F is reflexive feasible FunctorStr over A1,A2
F " is strict FunctorStr over A2,A1
B2 is M2( the carrier of A1)
F . B2 is M2( the carrier of A2)
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of F . [B2,B2] is set
( the ObjectMap of F . (B2,B2)) `1 is set
G is M2( the carrier of A2)
(F ") . G is M2( the carrier of A1)
the ObjectMap of (F ") is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of (F ") . (G,G) is M2([: the carrier of A1, the carrier of A1:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of (F ") . [G,G] is set
( the ObjectMap of (F ") . (G,G)) `1 is set
(F ") * F is strict FunctorStr over A1,A1
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
((F ") * F) . B2 is M2( the carrier of A1)
the ObjectMap of ((F ") * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of ((F ") * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of ((F ") * F) . [B2,B2] is set
( the ObjectMap of ((F ") * F) . (B2,B2)) `1 is set
B1 is reflexive feasible FunctorStr over A2,A1
F * B1 is feasible strict FunctorStr over A2,A2
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
(F * B1) . G is M2( the carrier of A2)
the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of (F * B1) . (G,G) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (F * B1) . [G,G] is set
( the ObjectMap of (F * B1) . (G,G)) `1 is set
A1 is non empty transitive with_units reflexive AltCatStr
A2 is non empty transitive with_units reflexive AltCatStr
the carrier of A1 is non empty set
F is reflexive feasible Covariant FunctorStr over A1,A2
F " is strict FunctorStr over A2,A1
B1 is reflexive feasible Covariant FunctorStr over A2,A1
B2 is M2( the carrier of A1)
G is M2( the carrier of A1)
<^B2,G^> is set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
the Arrows of A1 . (B2,G) is set
[B2,G] is V15() set
{B2,G} is set
{B2} is set
{{B2,G},{B2}} is set
the Arrows of A1 . [B2,G] is set
F . B2 is M2( the carrier of A2)
the carrier of A2 is non empty set
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of F . [B2,B2] is set
( the ObjectMap of F . (B2,B2)) `1 is set
F . G is M2( the carrier of A2)
the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of F . [G,G] is set
( the ObjectMap of F . (G,G)) `1 is set
<^(F . B2),(F . G)^> is set
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A2 . ((F . B2),(F . G)) is set
[(F . B2),(F . G)] is V15() set
{(F . B2),(F . G)} is set
{(F . B2)} is set
{{(F . B2),(F . G)},{(F . B2)}} is set
the Arrows of A2 . [(F . B2),(F . G)] is set
B1 . (F . B2) is M2( the carrier of A1)
the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])
[(F . B2),(F . B2)] is V15() set
{(F . B2),(F . B2)} is set
{{(F . B2),(F . B2)},{(F . B2)}} is set
the ObjectMap of B1 . [(F . B2),(F . B2)] is set
( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set
B1 . (F . G) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])
[(F . G),(F . G)] is V15() set
{(F . G),(F . G)} is set
{(F . G)} is set
{{(F . G),(F . G)},{(F . G)}} is set
the ObjectMap of B1 . [(F . G),(F . G)] is set
( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set
b is M2(<^B2,G^>)
F . b is M2(<^(F . B2),(F . G)^>)
c is M2(<^(F . B2),(F . G)^>)
B1 . c is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)
<^(B1 . (F . B2)),(B1 . (F . G))^> is set
the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set
[(B1 . (F . B2)),(B1 . (F . G))] is V15() set
{(B1 . (F . B2)),(B1 . (F . G))} is set
{(B1 . (F . B2))} is set
{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set
the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set
(F ") * F is strict FunctorStr over A1,A1
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
B1 * F is reflexive feasible strict Covariant FunctorStr over A1,A1
(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)
(B1 * F) . B2 is M2( the carrier of A1)
the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (B1 * F) . [B2,B2] is set
( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set
(B1 * F) . G is M2( the carrier of A1)
the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (B1 * F) . [G,G] is set
( the ObjectMap of (B1 * F) . (G,G)) `1 is set
<^((B1 * F) . B2),((B1 * F) . G)^> is set
the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set
[((B1 * F) . B2),((B1 * F) . G)] is V15() set
{((B1 * F) . B2),((B1 * F) . G)} is set
{((B1 * F) . B2)} is set
{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set
the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set
F * B1 is reflexive feasible strict Covariant FunctorStr over A2,A2
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
(F * B1) . c is M2(<^((F * B1) . (F . B2)),((F * B1) . (F . G))^>)
(F * B1) . (F . B2) is M2( the carrier of A2)
the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of (F * B1) . ((F . B2),(F . B2)) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (F * B1) . [(F . B2),(F . B2)] is set
( the ObjectMap of (F * B1) . ((F . B2),(F . B2))) `1 is set
(F * B1) . (F . G) is M2( the carrier of A2)
the ObjectMap of (F * B1) . ((F . G),(F . G)) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (F * B1) . [(F . G),(F . G)] is set
( the ObjectMap of (F * B1) . ((F . G),(F . G))) `1 is set
<^((F * B1) . (F . B2)),((F * B1) . (F . G))^> is set
the Arrows of A2 . (((F * B1) . (F . B2)),((F * B1) . (F . G))) is set
[((F * B1) . (F . B2)),((F * B1) . (F . G))] is V15() set
{((F * B1) . (F . B2)),((F * B1) . (F . G))} is set
{((F * B1) . (F . B2))} is set
{{((F * B1) . (F . B2)),((F * B1) . (F . G))},{((F * B1) . (F . B2))}} is set
the Arrows of A2 . [((F * B1) . (F . B2)),((F * B1) . (F . G))] is set
A1 is non empty transitive with_units reflexive AltCatStr
A2 is non empty transitive with_units reflexive AltCatStr
the carrier of A1 is non empty set
F is reflexive feasible Contravariant FunctorStr over A1,A2
F " is strict FunctorStr over A2,A1
B1 is reflexive feasible Contravariant FunctorStr over A2,A1
B2 is M2( the carrier of A1)
G is M2( the carrier of A1)
<^B2,G^> is set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
the Arrows of A1 . (B2,G) is set
[B2,G] is V15() set
{B2,G} is set
{B2} is set
{{B2,G},{B2}} is set
the Arrows of A1 . [B2,G] is set
F . G is M2( the carrier of A2)
the carrier of A2 is non empty set
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of F . [G,G] is set
( the ObjectMap of F . (G,G)) `1 is set
F . B2 is M2( the carrier of A2)
the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of F . [B2,B2] is set
( the ObjectMap of F . (B2,B2)) `1 is set
<^(F . G),(F . B2)^> is set
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A2 . ((F . G),(F . B2)) is set
[(F . G),(F . B2)] is V15() set
{(F . G),(F . B2)} is set
{(F . G)} is set
{{(F . G),(F . B2)},{(F . G)}} is set
the Arrows of A2 . [(F . G),(F . B2)] is set
B1 . (F . B2) is M2( the carrier of A1)
the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])
[(F . B2),(F . B2)] is V15() set
{(F . B2),(F . B2)} is set
{(F . B2)} is set
{{(F . B2),(F . B2)},{(F . B2)}} is set
the ObjectMap of B1 . [(F . B2),(F . B2)] is set
( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set
B1 . (F . G) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])
[(F . G),(F . G)] is V15() set
{(F . G),(F . G)} is set
{{(F . G),(F . G)},{(F . G)}} is set
the ObjectMap of B1 . [(F . G),(F . G)] is set
( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set
b is M2(<^B2,G^>)
F . b is M2(<^(F . G),(F . B2)^>)
c is M2(<^(F . G),(F . B2)^>)
B1 . c is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)
<^(B1 . (F . B2)),(B1 . (F . G))^> is set
the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set
[(B1 . (F . B2)),(B1 . (F . G))] is V15() set
{(B1 . (F . B2)),(B1 . (F . G))} is set
{(B1 . (F . B2))} is set
{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set
the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set
(F ") * F is strict FunctorStr over A1,A1
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
B1 * F is reflexive feasible strict Covariant FunctorStr over A1,A1
(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)
(B1 * F) . B2 is M2( the carrier of A1)
the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (B1 * F) . [B2,B2] is set
( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set
(B1 * F) . G is M2( the carrier of A1)
the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (B1 * F) . [G,G] is set
( the ObjectMap of (B1 * F) . (G,G)) `1 is set
<^((B1 * F) . B2),((B1 * F) . G)^> is set
the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set
[((B1 * F) . B2),((B1 * F) . G)] is V15() set
{((B1 * F) . B2),((B1 * F) . G)} is set
{((B1 * F) . B2)} is set
{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set
the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set
F * B1 is reflexive feasible strict Covariant FunctorStr over A2,A2
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
(F * B1) . c is M2(<^((F * B1) . (F . G)),((F * B1) . (F . B2))^>)
(F * B1) . (F . G) is M2( the carrier of A2)
the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of (F * B1) . ((F . G),(F . G)) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (F * B1) . [(F . G),(F . G)] is set
( the ObjectMap of (F * B1) . ((F . G),(F . G))) `1 is set
(F * B1) . (F . B2) is M2( the carrier of A2)
the ObjectMap of (F * B1) . ((F . B2),(F . B2)) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (F * B1) . [(F . B2),(F . B2)] is set
( the ObjectMap of (F * B1) . ((F . B2),(F . B2))) `1 is set
<^((F * B1) . (F . G)),((F * B1) . (F . B2))^> is set
the Arrows of A2 . (((F * B1) . (F . G)),((F * B1) . (F . B2))) is set
[((F * B1) . (F . G)),((F * B1) . (F . B2))] is V15() set
{((F * B1) . (F . G)),((F * B1) . (F . B2))} is set
{((F * B1) . (F . G))} is set
{{((F * B1) . (F . G)),((F * B1) . (F . B2))},{((F * B1) . (F . G))}} is set
the Arrows of A2 . [((F * B1) . (F . G)),((F * B1) . (F . B2))] is set
A1 is non empty transitive V106() with_units reflexive AltCatStr
A2 is non empty transitive V106() with_units reflexive AltCatStr
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
F is feasible id-preserving Functor of A1,A2
F " is strict FunctorStr over A2,A1
(F ") * F is strict FunctorStr over A1,A1
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
B2 is feasible id-preserving Functor of A2,A1
F * B2 is feasible strict FunctorStr over A2,A2
the ObjectMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
the carrier of A2 is non empty set
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the carrier of A1 is non empty set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the MorphMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B2, the Arrows of A2, the Arrows of A1
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
FunctorStr(# the ObjectMap of B2, the MorphMap of B2 #) is strict FunctorStr over A2,A1
(id A1) * B2 is feasible strict FunctorStr over A2,A1
B1 is feasible FunctorStr over A2,A1
B1 * (id A2) is feasible strict FunctorStr over A2,A1
A1 is non empty transitive V106() with_units reflexive AltCatStr
A2 is non empty transitive V106() with_units reflexive AltCatStr
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
F is feasible id-preserving Functor of A1,A2
F " is strict FunctorStr over A2,A1
B1 is feasible FunctorStr over A2,A1
F * B1 is feasible strict FunctorStr over A2,A2
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
B2 is feasible id-preserving Functor of A2,A1
B2 * F is feasible strict FunctorStr over A1,A1
the ObjectMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
the carrier of A2 is non empty set
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the carrier of A1 is non empty set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the MorphMap of B2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B2, the Arrows of A2, the Arrows of A1
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
FunctorStr(# the ObjectMap of B2, the MorphMap of B2 #) is strict FunctorStr over A2,A1
(id A1) * B1 is feasible strict FunctorStr over A2,A1
B2 * (id A2) is feasible strict id-preserving FunctorStr over A2,A1
A1 is non empty transitive V106() with_units reflexive AltCatStr
A2 is non empty transitive V106() with_units reflexive AltCatStr
the carrier of A2 is non empty set
F is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A1,A2
F " is strict FunctorStr over A2,A1
B1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A2,A1
the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the carrier of A1 is non empty set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1
B2 is M2( the carrier of A2)
G is M2( the carrier of A2)
<^B2,G^> is set
the Arrows of A2 . (B2,G) is set
[B2,G] is V15() set
{B2,G} is set
{B2} is set
{{B2,G},{B2}} is set
the Arrows of A2 . [B2,G] is set
F * B1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A2,A2
b is M2(<^B2,G^>)
(F * B1) . b is M2(<^((F * B1) . B2),((F * B1) . G)^>)
(F * B1) . B2 is M2( the carrier of A2)
the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (F * B1) . [B2,B2] is set
( the ObjectMap of (F * B1) . (B2,B2)) `1 is set
(F * B1) . G is M2( the carrier of A2)
the ObjectMap of (F * B1) . (G,G) is M2([: the carrier of A2, the carrier of A2:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of (F * B1) . [G,G] is set
( the ObjectMap of (F * B1) . (G,G)) `1 is set
<^((F * B1) . B2),((F * B1) . G)^> is set
the Arrows of A2 . (((F * B1) . B2),((F * B1) . G)) is set
[((F * B1) . B2),((F * B1) . G)] is V15() set
{((F * B1) . B2),((F * B1) . G)} is set
{((F * B1) . B2)} is set
{{((F * B1) . B2),((F * B1) . G)},{((F * B1) . B2)}} is set
the Arrows of A2 . [((F * B1) . B2),((F * B1) . G)] is set
B1 . B2 is M2( the carrier of A1)
the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of B1 . [B2,B2] is set
( the ObjectMap of B1 . (B2,B2)) `1 is set
B1 . G is M2( the carrier of A1)
the ObjectMap of B1 . (G,G) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of B1 . [G,G] is set
( the ObjectMap of B1 . (G,G)) `1 is set
B1 . b is M2(<^(B1 . B2),(B1 . G)^>)
<^(B1 . B2),(B1 . G)^> is set
the Arrows of A1 . ((B1 . B2),(B1 . G)) is set
[(B1 . B2),(B1 . G)] is V15() set
{(B1 . B2),(B1 . G)} is set
{(B1 . B2)} is set
{{(B1 . B2),(B1 . G)},{(B1 . B2)}} is set
the Arrows of A1 . [(B1 . B2),(B1 . G)] is set
F . (B1 . b) is M2(<^(F . (B1 . B2)),(F . (B1 . G))^>)
F . (B1 . B2) is M2( the carrier of A2)
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])
[(B1 . B2),(B1 . B2)] is V15() set
{(B1 . B2),(B1 . B2)} is set
{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set
the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set
( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set
F . (B1 . G) is M2( the carrier of A2)
the ObjectMap of F . ((B1 . G),(B1 . G)) is M2([: the carrier of A2, the carrier of A2:])
[(B1 . G),(B1 . G)] is V15() set
{(B1 . G),(B1 . G)} is set
{(B1 . G)} is set
{{(B1 . G),(B1 . G)},{(B1 . G)}} is set
the ObjectMap of F . [(B1 . G),(B1 . G)] is set
( the ObjectMap of F . ((B1 . G),(B1 . G))) `1 is set
<^(F . (B1 . B2)),(F . (B1 . G))^> is set
the Arrows of A2 . ((F . (B1 . B2)),(F . (B1 . G))) is set
[(F . (B1 . B2)),(F . (B1 . G))] is V15() set
{(F . (B1 . B2)),(F . (B1 . G))} is set
{(F . (B1 . B2))} is set
{{(F . (B1 . B2)),(F . (B1 . G))},{(F . (B1 . B2))}} is set
the Arrows of A2 . [(F . (B1 . B2)),(F . (B1 . G))] is set
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
(id A2) . b is M2(<^((id A2) . B2),((id A2) . G)^>)
(id A2) . B2 is M2( the carrier of A2)
the ObjectMap of (id A2) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (id A2) . [B2,B2] is set
( the ObjectMap of (id A2) . (B2,B2)) `1 is set
(id A2) . G is M2( the carrier of A2)
the ObjectMap of (id A2) . (G,G) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (id A2) . [G,G] is set
( the ObjectMap of (id A2) . (G,G)) `1 is set
<^((id A2) . B2),((id A2) . G)^> is set
the Arrows of A2 . (((id A2) . B2),((id A2) . G)) is set
[((id A2) . B2),((id A2) . G)] is V15() set
{((id A2) . B2),((id A2) . G)} is set
{((id A2) . B2)} is set
{{((id A2) . B2),((id A2) . G)},{((id A2) . B2)}} is set
the Arrows of A2 . [((id A2) . B2),((id A2) . G)] is set
B2 is M2( the carrier of A2)
(F * B1) . B2 is M2( the carrier of A2)
the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (F * B1) . [B2,B2] is set
( the ObjectMap of (F * B1) . (B2,B2)) `1 is set
B1 . B2 is M2( the carrier of A1)
the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of B1 . [B2,B2] is set
( the ObjectMap of B1 . (B2,B2)) `1 is set
F . (B1 . B2) is M2( the carrier of A2)
the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])
[(B1 . B2),(B1 . B2)] is V15() set
{(B1 . B2),(B1 . B2)} is set
{(B1 . B2)} is set
{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set
the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set
( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set
(id A2) . B2 is M2( the carrier of A2)
the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (id A2) . [B2,B2] is set
( the ObjectMap of (id A2) . (B2,B2)) `1 is set
A1 is non empty transitive V106() with_units reflexive AltCatStr
A2 is non empty transitive V106() with_units reflexive AltCatStr
the carrier of A2 is non empty set
F is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A1,A2
F " is strict FunctorStr over A2,A1
B1 is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A2,A1
the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
the carrier of A1 is non empty set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1
B2 is M2( the carrier of A2)
G is M2( the carrier of A2)
<^B2,G^> is set
the Arrows of A2 . (B2,G) is set
[B2,G] is V15() set
{B2,G} is set
{B2} is set
{{B2,G},{B2}} is set
the Arrows of A2 . [B2,G] is set
F * B1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A2,A2
b is M2(<^B2,G^>)
(F * B1) . b is M2(<^((F * B1) . B2),((F * B1) . G)^>)
(F * B1) . B2 is M2( the carrier of A2)
the ObjectMap of (F * B1) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (F * B1) . [B2,B2] is set
( the ObjectMap of (F * B1) . (B2,B2)) `1 is set
(F * B1) . G is M2( the carrier of A2)
the ObjectMap of (F * B1) . (G,G) is M2([: the carrier of A2, the carrier of A2:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of (F * B1) . [G,G] is set
( the ObjectMap of (F * B1) . (G,G)) `1 is set
<^((F * B1) . B2),((F * B1) . G)^> is set
the Arrows of A2 . (((F * B1) . B2),((F * B1) . G)) is set
[((F * B1) . B2),((F * B1) . G)] is V15() set
{((F * B1) . B2),((F * B1) . G)} is set
{((F * B1) . B2)} is set
{{((F * B1) . B2),((F * B1) . G)},{((F * B1) . B2)}} is set
the Arrows of A2 . [((F * B1) . B2),((F * B1) . G)] is set
B1 . G is M2( the carrier of A1)
the ObjectMap of B1 . (G,G) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of B1 . [G,G] is set
( the ObjectMap of B1 . (G,G)) `1 is set
B1 . B2 is M2( the carrier of A1)
the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of B1 . [B2,B2] is set
( the ObjectMap of B1 . (B2,B2)) `1 is set
B1 . b is M2(<^(B1 . G),(B1 . B2)^>)
<^(B1 . G),(B1 . B2)^> is set
the Arrows of A1 . ((B1 . G),(B1 . B2)) is set
[(B1 . G),(B1 . B2)] is V15() set
{(B1 . G),(B1 . B2)} is set
{(B1 . G)} is set
{{(B1 . G),(B1 . B2)},{(B1 . G)}} is set
the Arrows of A1 . [(B1 . G),(B1 . B2)] is set
F . (B1 . b) is M2(<^(F . (B1 . B2)),(F . (B1 . G))^>)
F . (B1 . B2) is M2( the carrier of A2)
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])
[(B1 . B2),(B1 . B2)] is V15() set
{(B1 . B2),(B1 . B2)} is set
{(B1 . B2)} is set
{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set
the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set
( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set
F . (B1 . G) is M2( the carrier of A2)
the ObjectMap of F . ((B1 . G),(B1 . G)) is M2([: the carrier of A2, the carrier of A2:])
[(B1 . G),(B1 . G)] is V15() set
{(B1 . G),(B1 . G)} is set
{{(B1 . G),(B1 . G)},{(B1 . G)}} is set
the ObjectMap of F . [(B1 . G),(B1 . G)] is set
( the ObjectMap of F . ((B1 . G),(B1 . G))) `1 is set
<^(F . (B1 . B2)),(F . (B1 . G))^> is set
the Arrows of A2 . ((F . (B1 . B2)),(F . (B1 . G))) is set
[(F . (B1 . B2)),(F . (B1 . G))] is V15() set
{(F . (B1 . B2)),(F . (B1 . G))} is set
{(F . (B1 . B2))} is set
{{(F . (B1 . B2)),(F . (B1 . G))},{(F . (B1 . B2))}} is set
the Arrows of A2 . [(F . (B1 . B2)),(F . (B1 . G))] is set
id A2 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A2,A2
(id A2) . b is M2(<^((id A2) . B2),((id A2) . G)^>)
(id A2) . B2 is M2( the carrier of A2)
the ObjectMap of (id A2) is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A2, the carrier of A2:]:])
the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (id A2) . [B2,B2] is set
( the ObjectMap of (id A2) . (B2,B2)) `1 is set
(id A2) . G is M2( the carrier of A2)
the ObjectMap of (id A2) . (G,G) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (id A2) . [G,G] is set
( the ObjectMap of (id A2) . (G,G)) `1 is set
<^((id A2) . B2),((id A2) . G)^> is set
the Arrows of A2 . (((id A2) . B2),((id A2) . G)) is set
[((id A2) . B2),((id A2) . G)] is V15() set
{((id A2) . B2),((id A2) . G)} is set
{((id A2) . B2)} is set
{{((id A2) . B2),((id A2) . G)},{((id A2) . B2)}} is set
the Arrows of A2 . [((id A2) . B2),((id A2) . G)] is set
B2 is M2( the carrier of A2)
(F * B1) . B2 is M2( the carrier of A2)
the ObjectMap of (F * B1) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
[B2,B2] is V15() set
{B2,B2} is set
{B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (F * B1) . [B2,B2] is set
( the ObjectMap of (F * B1) . (B2,B2)) `1 is set
B1 . B2 is M2( the carrier of A1)
the ObjectMap of B1 . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of B1 . [B2,B2] is set
( the ObjectMap of B1 . (B2,B2)) `1 is set
F . (B1 . B2) is M2( the carrier of A2)
the ObjectMap of F . ((B1 . B2),(B1 . B2)) is M2([: the carrier of A2, the carrier of A2:])
[(B1 . B2),(B1 . B2)] is V15() set
{(B1 . B2),(B1 . B2)} is set
{(B1 . B2)} is set
{{(B1 . B2),(B1 . B2)},{(B1 . B2)}} is set
the ObjectMap of F . [(B1 . B2),(B1 . B2)] is set
( the ObjectMap of F . ((B1 . B2),(B1 . B2))) `1 is set
(id A2) . B2 is M2( the carrier of A2)
the ObjectMap of (id A2) . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of (id A2) . [B2,B2] is set
( the ObjectMap of (id A2) . (B2,B2)) `1 is set
A1 is non empty transitive V106() with_units reflexive AltCatStr
A2 is non empty transitive V106() with_units reflexive AltCatStr
the carrier of A1 is non empty set
F is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A1,A2
F " is strict FunctorStr over A2,A1
B1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of A2,A1
the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
the carrier of A2 is non empty set
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1
B2 is M2( the carrier of A1)
G is M2( the carrier of A1)
<^B2,G^> is set
the Arrows of A1 . (B2,G) is set
[B2,G] is V15() set
{B2,G} is set
{B2} is set
{{B2,G},{B2}} is set
the Arrows of A1 . [B2,G] is set
B1 * F is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A1,A1
b is M2(<^B2,G^>)
(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)
(B1 * F) . B2 is M2( the carrier of A1)
the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
[B2,B2] is V15() set
{B2,B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (B1 * F) . [B2,B2] is set
( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set
(B1 * F) . G is M2( the carrier of A1)
the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of (B1 * F) . [G,G] is set
( the ObjectMap of (B1 * F) . (G,G)) `1 is set
<^((B1 * F) . B2),((B1 * F) . G)^> is set
the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set
[((B1 * F) . B2),((B1 * F) . G)] is V15() set
{((B1 * F) . B2),((B1 * F) . G)} is set
{((B1 * F) . B2)} is set
{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set
the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set
F . B2 is M2( the carrier of A2)
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of F . [B2,B2] is set
( the ObjectMap of F . (B2,B2)) `1 is set
F . G is M2( the carrier of A2)
the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of F . [G,G] is set
( the ObjectMap of F . (G,G)) `1 is set
F . b is M2(<^(F . B2),(F . G)^>)
<^(F . B2),(F . G)^> is set
the Arrows of A2 . ((F . B2),(F . G)) is set
[(F . B2),(F . G)] is V15() set
{(F . B2),(F . G)} is set
{(F . B2)} is set
{{(F . B2),(F . G)},{(F . B2)}} is set
the Arrows of A2 . [(F . B2),(F . G)] is set
B1 . (F . b) is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)
B1 . (F . B2) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])
[(F . B2),(F . B2)] is V15() set
{(F . B2),(F . B2)} is set
{{(F . B2),(F . B2)},{(F . B2)}} is set
the ObjectMap of B1 . [(F . B2),(F . B2)] is set
( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set
B1 . (F . G) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])
[(F . G),(F . G)] is V15() set
{(F . G),(F . G)} is set
{(F . G)} is set
{{(F . G),(F . G)},{(F . G)}} is set
the ObjectMap of B1 . [(F . G),(F . G)] is set
( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set
<^(B1 . (F . B2)),(B1 . (F . G))^> is set
the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set
[(B1 . (F . B2)),(B1 . (F . G))] is V15() set
{(B1 . (F . B2)),(B1 . (F . G))} is set
{(B1 . (F . B2))} is set
{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set
the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
(id A1) . b is M2(<^((id A1) . B2),((id A1) . G)^>)
(id A1) . B2 is M2( the carrier of A1)
the ObjectMap of (id A1) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])
the ObjectMap of (id A1) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (id A1) . [B2,B2] is set
( the ObjectMap of (id A1) . (B2,B2)) `1 is set
(id A1) . G is M2( the carrier of A1)
the ObjectMap of (id A1) . (G,G) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (id A1) . [G,G] is set
( the ObjectMap of (id A1) . (G,G)) `1 is set
<^((id A1) . B2),((id A1) . G)^> is set
the Arrows of A1 . (((id A1) . B2),((id A1) . G)) is set
[((id A1) . B2),((id A1) . G)] is V15() set
{((id A1) . B2),((id A1) . G)} is set
{((id A1) . B2)} is set
{{((id A1) . B2),((id A1) . G)},{((id A1) . B2)}} is set
the Arrows of A1 . [((id A1) . B2),((id A1) . G)] is set
B2 is M2( the carrier of A1)
(B1 * F) . B2 is M2( the carrier of A1)
the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
[B2,B2] is V15() set
{B2,B2} is set
{B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (B1 * F) . [B2,B2] is set
( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set
F . B2 is M2( the carrier of A2)
the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of F . [B2,B2] is set
( the ObjectMap of F . (B2,B2)) `1 is set
B1 . (F . B2) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])
[(F . B2),(F . B2)] is V15() set
{(F . B2),(F . B2)} is set
{(F . B2)} is set
{{(F . B2),(F . B2)},{(F . B2)}} is set
the ObjectMap of B1 . [(F . B2),(F . B2)] is set
( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set
(id A1) . B2 is M2( the carrier of A1)
the ObjectMap of (id A1) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
the ObjectMap of (id A1) . [B2,B2] is set
( the ObjectMap of (id A1) . (B2,B2)) `1 is set
A1 is non empty transitive V106() with_units reflexive AltCatStr
A2 is non empty transitive V106() with_units reflexive AltCatStr
the carrier of A1 is non empty set
F is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A1,A2
F " is strict FunctorStr over A2,A1
B1 is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of A2,A1
the ObjectMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:])
the carrier of A2 is non empty set
[: the carrier of A2, the carrier of A2:] is Relation-like non empty set
[: the carrier of A1, the carrier of A1:] is Relation-like non empty set
[:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A2, the carrier of A2:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the MorphMap of B1 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total Function-yielding V37() MSUnTrans of the ObjectMap of B1, the Arrows of A2, the Arrows of A1
the Arrows of A2 is Relation-like [: the carrier of A2, the carrier of A2:] -defined Function-like non empty total set
the Arrows of A1 is Relation-like [: the carrier of A1, the carrier of A1:] -defined Function-like non empty total set
FunctorStr(# the ObjectMap of B1, the MorphMap of B1 #) is strict FunctorStr over A2,A1
B2 is M2( the carrier of A1)
G is M2( the carrier of A1)
<^B2,G^> is set
the Arrows of A1 . (B2,G) is set
[B2,G] is V15() set
{B2,G} is set
{B2} is set
{{B2,G},{B2}} is set
the Arrows of A1 . [B2,G] is set
B1 * F is reflexive feasible strict Covariant id-preserving comp-preserving covariant Functor of A1,A1
b is M2(<^B2,G^>)
(B1 * F) . b is M2(<^((B1 * F) . B2),((B1 * F) . G)^>)
(B1 * F) . B2 is M2( the carrier of A1)
the ObjectMap of (B1 * F) is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A1, the carrier of A1:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A1, the carrier of A1:]:] is non empty set
the ObjectMap of (B1 * F) . (B2,B2) is M2([: the carrier of A1, the carrier of A1:])
[B2,B2] is V15() set
{B2,B2} is set
{{B2,B2},{B2}} is set
the ObjectMap of (B1 * F) . [B2,B2] is set
( the ObjectMap of (B1 * F) . (B2,B2)) `1 is set
(B1 * F) . G is M2( the carrier of A1)
the ObjectMap of (B1 * F) . (G,G) is M2([: the carrier of A1, the carrier of A1:])
[G,G] is V15() set
{G,G} is set
{G} is set
{{G,G},{G}} is set
the ObjectMap of (B1 * F) . [G,G] is set
( the ObjectMap of (B1 * F) . (G,G)) `1 is set
<^((B1 * F) . B2),((B1 * F) . G)^> is set
the Arrows of A1 . (((B1 * F) . B2),((B1 * F) . G)) is set
[((B1 * F) . B2),((B1 * F) . G)] is V15() set
{((B1 * F) . B2),((B1 * F) . G)} is set
{((B1 * F) . B2)} is set
{{((B1 * F) . B2),((B1 * F) . G)},{((B1 * F) . B2)}} is set
the Arrows of A1 . [((B1 * F) . B2),((B1 * F) . G)] is set
F . G is M2( the carrier of A2)
the ObjectMap of F is Relation-like [: the carrier of A1, the carrier of A1:] -defined [: the carrier of A2, the carrier of A2:] -valued Function-like quasi_total M2( bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:])
[:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is Relation-like non empty set
bool [:[: the carrier of A1, the carrier of A1:],[: the carrier of A2, the carrier of A2:]:] is non empty set
the ObjectMap of F . (G,G) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of F . [G,G] is set
( the ObjectMap of F . (G,G)) `1 is set
F . B2 is M2( the carrier of A2)
the ObjectMap of F . (B2,B2) is M2([: the carrier of A2, the carrier of A2:])
the ObjectMap of F . [B2,B2] is set
( the ObjectMap of F . (B2,B2)) `1 is set
F . b is M2(<^(F . G),(F . B2)^>)
<^(F . G),(F . B2)^> is set
the Arrows of A2 . ((F . G),(F . B2)) is set
[(F . G),(F . B2)] is V15() set
{(F . G),(F . B2)} is set
{(F . G)} is set
{{(F . G),(F . B2)},{(F . G)}} is set
the Arrows of A2 . [(F . G),(F . B2)] is set
B1 . (F . b) is M2(<^(B1 . (F . B2)),(B1 . (F . G))^>)
B1 . (F . B2) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . B2),(F . B2)) is M2([: the carrier of A1, the carrier of A1:])
[(F . B2),(F . B2)] is V15() set
{(F . B2),(F . B2)} is set
{(F . B2)} is set
{{(F . B2),(F . B2)},{(F . B2)}} is set
the ObjectMap of B1 . [(F . B2),(F . B2)] is set
( the ObjectMap of B1 . ((F . B2),(F . B2))) `1 is set
B1 . (F . G) is M2( the carrier of A1)
the ObjectMap of B1 . ((F . G),(F . G)) is M2([: the carrier of A1, the carrier of A1:])
[(F . G),(F . G)] is V15() set
{(F . G),(F . G)} is set
{{(F . G),(F . G)},{(F . G)}} is set
the ObjectMap of B1 . [(F . G),(F . G)] is set
( the ObjectMap of B1 . ((F . G),(F . G))) `1 is set
<^(B1 . (F . B2)),(B1 . (F . G))^> is set
the Arrows of A1 . ((B1 . (F . B2)),(B1 . (F . G))) is set
[(B1 . (F . B2)),(B1 . (F . G))] is V15() set
{(B1 . (F . B2)),(B1 . (F . G))} is set
{(B1 . (F . B2))} is set
{{(B1 . (F . B2)),(B1 . (F . G))},{(B1 . (F . B2))}} is set
the Arrows of A1 . [(B1 . (F . B2)),(B1 . (F . G))] is set
id A1 is reflexive feasible strict Covariant id-preserving comp-preserving covariant bijective Functor of A1,A1
(id A1) . b is M2(<^((id A1) . B2),((id A1) . G)^>)
(id A1) . B2 is M2( the carrier of A1)
the ObjectMap of (id A1) is Relation-like [: the