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 V36() V37() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V36() V37() set
1 is non empty set
{{},1} is set
C is non empty with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
<^i,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
idm o1 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
o2 is M2( the carrier of C)
<^i,o2^> is set
the Arrows of C . (i,o2) is set
[i,o2] is V15() set
{i,o2} is set
{{i,o2},{i}} is set
the Arrows of C . [i,o2] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
o1 is M2(<^i,o1^>)
o2 is M2(<^i,o2^>)
p1 is M2(<^o1,o2^>)
p1 * o1 is M2(<^i,o2^>)
p1 " is M2(<^o2,o1^>)
(p1 ") * p1 is M2(<^o1,o1^>)
(p1 ") * o2 is M2(<^i,o1^>)
((p1 ") * p1) * o1 is M2(<^i,o1^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o2,i^> is set
the Arrows of C . (o2,i) is set
[o2,i] is V15() set
{o2,i} is set
{{o2,i},{o2}} is set
the Arrows of C . [o2,i] is set
<^i,o2^> is set
the Arrows of C . (i,o2) is set
[i,o2] is V15() set
{i,o2} is set
{{i,o2},{i}} is set
the Arrows of C . [i,o2] is set
o1 is M2(<^i,o1^>)
o2 is M2(<^o2,o1^>)
p1 is M2(<^o2,i^>)
o1 * p1 is M2(<^o2,o1^>)
p1 " is M2(<^i,o2^>)
p1 * (p1 ") is M2(<^i,i^>)
o2 * (p1 ") is M2(<^i,o1^>)
o1 * (p1 * (p1 ")) is M2(<^i,o1^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^i,o1^>)
o2 " is M2(<^o1,i^>)
(o2 ") " is M2(<^i,o1^>)
(o2 ") * ((o2 ") ") is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
(o2 ") * o2 is M2(<^i,i^>)
idm i is M2(<^i,i^>)
((o2 ") ") * (o2 ") is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
idm o1 is M2(<^o1,o1^>)
o2 * (o2 ") is M2(<^o1,o1^>)
C is non empty with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 * (idm i) is M2(<^i,o1^>)
o1 is M2(<^i,o1^>)
o1 * (idm i) is M2(<^i,o1^>)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
(idm i) * o2 is M2(<^o1,i^>)
o1 is M2(<^o1,i^>)
(idm i) * o1 is M2(<^o1,i^>)
C is non empty with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is retraction coretraction mono epi M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
idm i is retraction coretraction iso mono epi M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
o2 is M2(<^i,o1^>)
o2 is M2(<^o1,i^>)
o2 * o2 is M2(<^i,i^>)
o1 is M2(<^o1,i^>)
o2 * o1 is M2(<^o1,o1^>)
(o2 * o2) * o1 is M2(<^o1,i^>)
o2 * (idm o1) is M2(<^o1,i^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^i,o1^>)
o1 is M2(<^o1,i^>)
o2 * o1 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
o1 * (o2 * o1) is M2(<^o1,i^>)
o1 * o2 is M2(<^i,i^>)
<^i,i^> is non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
(o1 * o2) * o1 is M2(<^o1,i^>)
idm i is retraction coretraction iso mono epi M2(<^i,i^>)
(idm i) * o1 is M2(<^o1,i^>)
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
o1 * (idm o1) is M2(<^o1,i^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o1 is M2(<^i,o1^>)
o2 is M2( the carrier of C)
<^o2,o2^> is non empty set
the Arrows of C . (o2,o2) is set
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the Arrows of C . [o2,o2] is set
the M2(<^o2,o2^>) is M2(<^o2,o2^>)
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
the M2(<^o2,o1^>) is M2(<^o2,o1^>)
<^i,o2^> is set
the Arrows of C . (i,o2) is set
[i,o2] is V15() set
{i,o2} is set
{{i,o2},{i}} is set
the Arrows of C . [i,o2] is set
the M2(<^i,o2^>) is M2(<^i,o2^>)
the M2(<^o2,o2^>) " is M2(<^o2,o2^>)
( the M2(<^o2,o2^>) ") * the M2(<^o2,o2^>) is M2(<^o2,o2^>)
the M2(<^o2,o1^>) * (( the M2(<^o2,o2^>) ") * the M2(<^o2,o2^>)) is M2(<^o2,o1^>)
( the M2(<^o2,o1^>) * (( the M2(<^o2,o2^>) ") * the M2(<^o2,o2^>))) * the M2(<^i,o2^>) is M2(<^i,o1^>)
C is non empty AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
o2 * o2 is M2(<^o1,o1^>)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
p1 is M2(<^o1,i^>)
o2 * p1 is M2(<^o1,o1^>)
p2 is M2(<^o1,i^>)
C is non empty AltCatStr
the carrier of C is non empty set
o1 is M2( the carrier of C)
i is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 * o2 is M2(<^o1,o1^>)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
p1 is M2(<^i,o1^>)
p1 * o2 is M2(<^o1,o1^>)
p2 is M2(<^i,o1^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
o2 " is M2(<^i,o1^>)
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
(o2 ") * o2 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
o1 is M2( the carrier of C)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 is M2(<^o1,i^>)
(o2 ") * o2 is M2(<^o1,o1^>)
p1 is M2(<^o1,o1^>)
o2 * p1 is M2(<^o1,i^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^i,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 " is M2(<^o1,i^>)
<^o1,i^> is set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
o2 * (o2 ") is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
o1 is M2( the carrier of C)
<^o1,o1^> is set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o2 * (o2 ") is M2(<^o1,o1^>)
p1 is M2(<^o1,o1^>)
p1 * o2 is M2(<^i,o1^>)
C is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
i is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o1,i^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o1,i) is set
[o1,i] is V15() set
{o1,i} is set
{o1} is set
{{o1,i},{o1}} is set
the Arrows of C . [o1,i] is set
<^i,o1^> is set
the Arrows of C . (i,o1) is set
[i,o1] is V15() set
{i,o1} is set
{i} is set
{{i,o1},{i}} is set
the Arrows of C . [i,o1] is set
o2 is M2(<^i,o1^>)
o1 is set
p1 is M2( the carrier of C)
<^o1,p1^> is set
the Arrows of C . (o1,p1) is set
[o1,p1] is V15() set
{o1,p1} is set
{{o1,p1},{o1}} is set
the Arrows of C . [o1,p1] is set
<^i,p1^> is set
the Arrows of C . (i,p1) is set
[i,p1] is V15() set
{i,p1} is set
{{i,p1},{i}} is set
the Arrows of C . [i,p1] is set
p2 is M2(<^i,p1^>)
o2 is M2(<^o1,i^>)
p2 * o2 is M2(<^o1,p1^>)
n is M2(<^o1,p1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the Arrows of C . [o1,o1] is set
n2 is M2(<^o1,o1^>)
n * o2 is M2(<^i,p1^>)
(n * o2) * o2 is M2(<^o1,p1^>)
o2 * o2 is M2(<^o1,o1^>)
n * (o2 * o2) is M2(<^o1,p1^>)
n * n2 is M2(<^o1,p1^>)
idm o1 is retraction coretraction iso mono epi M2(<^o1,o1^>)
n * (idm o1) is M2(<^o1,p1^>)
p1 is M2( the carrier of C)
<^p1,i^> is set
the Arrows of C . (p1,i) is set
[p1,i] is V15() set
{p1,i} is set
{p1} is set
{{p1,i},{p1}} is set
the Arrows of C . [p1,i] is set
<^p1,o1^> is set
the Arrows of C . (p1,o1) is set
[p1,o1] is V15() set
{p1,o1} is set
{{p1,o1},{p1}} is set
the Arrows of C . [p1,o1] is set
p2 is M2(<^p1,o1^>)
o2 is M2(<^o1,i^>)
o2 * p2 is M2(<^p1,i^>)
n is M2(<^p1,i^>)
<^i,i^> is non empty set
the Arrows of C . (i,i) is set
[i,i] is V15() set
{i,i} is set
{{i,i},{i}} is set
the Arrows of C . [i,i] is set
n2 is M2(<^i,i^>)
o2 * n is M2(<^p1,o1^>)
o2 * (o2 * n) is M2(<^p1,i^>)
o2 * o2 is M2(<^i,i^>)
(o2 * o2) * n is M2(<^p1,i^>)
n2 * n is M2(<^p1,i^>)
idm i is retraction coretraction iso mono epi M2(<^i,i^>)
(idm i) * n is M2(<^p1,i^>)
C is non empty transitive with_units reflexive AltCatStr
i is non empty transitive with_units reflexive AltCatStr
the carrier of C is non empty set
o1 is reflexive feasible Contravariant id-preserving comp-reversing contravariant Functor of C,i
o2 is M2( the carrier of C)
idm o2 is retraction coretraction mono epi M2(<^o2,o2^>)
<^o2,o2^> is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o2) is set
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the Arrows of C . [o2,o2] is set
o1 . (idm o2) is M2(<^(o1 . o2),(o1 . o2)^>)
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o2),(o1 . o2)^> is non empty set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o2)) is set
[(o1 . o2),(o1 . o2)] is V15() set
{(o1 . o2),(o1 . o2)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o2)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o2)] is set
idm (o1 . o2) is retraction coretraction mono epi M2(<^(o1 . o2),(o1 . o2)^>)
Morph-Map (o1,o2,o2) is Relation-like <^o2,o2^> -defined <^(o1 . o2),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o2^>,<^(o1 . o2),(o1 . o2)^>:])
[:<^o2,o2^>,<^(o1 . o2),(o1 . o2)^>:] is Relation-like non empty set
bool [:<^o2,o2^>,<^(o1 . o2),(o1 . o2)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o2) is set
the MorphMap of o1 . [o2,o2] is Relation-like Function-like set
(Morph-Map (o1,o2,o2)) . (idm o2) is M2(<^(o1 . o2),(o1 . o2)^>)
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Contravariant FunctorStr over C,i
[: the carrier of C, the carrier of C:] is Relation-like non empty set
o1 is M2( the carrier of C)
o1 . o1 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o1),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:])
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
[:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
proj1 the ObjectMap of o1 is Relation-like set
the ObjectMap of o1 * the Arrows of i is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
p1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() ManySortedFunction of the Arrows of C, the ObjectMap of o1 * the Arrows of i
p1 . [o2,o1] is Relation-like Function-like set
proj2 (p1 . [o2,o1]) is set
( the ObjectMap of o1 * the Arrows of i) . [o2,o1] is set
proj2 (Morph-Map (o1,o2,o1)) is set
the ObjectMap of o1 . (o2,o1) is M2([: the carrier of i, the carrier of i:])
the ObjectMap of o1 . [o2,o1] is set
the Arrows of i . ( the ObjectMap of o1 . (o2,o1)) is set
the ObjectMap of o1 * the Arrows of i is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
o2 is non empty set
[:[: the carrier of C, the carrier of C:],o2:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],o2:] is non empty set
p2 is Relation-like [: the carrier of C, the carrier of C:] -defined o2 -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],o2:])
p1 is Relation-like o2 -defined Function-like non empty V14(o2) set
p2 * p1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() ManySortedFunction of the Arrows of C, the ObjectMap of o1 * the Arrows of i
o2 is set
o1 . o2 is Relation-like Function-like set
proj2 (o1 . o2) is set
( the ObjectMap of o1 * the Arrows of i) . o2 is set
p1 is set
p2 is set
[p1,p2] is V15() set
{p1,p2} is set
{p1} is set
{{p1,p2},{p1}} is set
n2 is M2( the carrier of C)
n is M2( the carrier of C)
[n2,n] is V15() set
{n2,n} is set
{n2} is set
{{n2,n},{n2}} is set
proj1 the ObjectMap of o1 is Relation-like set
o1 . n is M2( the carrier of i)
the ObjectMap of o1 . (n,n) is M2([: the carrier of i, the carrier of i:])
[n,n] is V15() set
{n,n} is set
{n} is set
{{n,n},{n}} is set
the ObjectMap of o1 . [n,n] is set
K40(( the ObjectMap of o1 . (n,n))) is set
o1 . n2 is M2( the carrier of i)
the ObjectMap of o1 . (n2,n2) is M2([: the carrier of i, the carrier of i:])
[n2,n2] is V15() set
{n2,n2} is set
{{n2,n2},{n2}} is set
the ObjectMap of o1 . [n2,n2] is set
K40(( the ObjectMap of o1 . (n2,n2))) is set
<^(o1 . n),(o1 . n2)^> is set
the Arrows of i . ((o1 . n),(o1 . n2)) is set
[(o1 . n),(o1 . n2)] is V15() set
{(o1 . n),(o1 . n2)} is set
{(o1 . n)} is set
{{(o1 . n),(o1 . n2)},{(o1 . n)}} is set
the Arrows of i . [(o1 . n),(o1 . n2)] is set
Morph-Map (o1,n2,n) is Relation-like <^n2,n^> -defined <^(o1 . n),(o1 . n2)^> -valued Function-like quasi_total M2( bool [:<^n2,n^>,<^(o1 . n),(o1 . n2)^>:])
<^n2,n^> is set
the Arrows of C . (n2,n) is set
the Arrows of C . [n2,n] is set
[:<^n2,n^>,<^(o1 . n),(o1 . n2)^>:] is Relation-like set
bool [:<^n2,n^>,<^(o1 . n),(o1 . n2)^>:] is non empty set
the MorphMap of o1 . (n2,n) is set
the MorphMap of o1 . [n2,n] is Relation-like Function-like set
proj2 (Morph-Map (o1,n2,n)) is set
the ObjectMap of o1 . (n2,n) is M2([: the carrier of i, the carrier of i:])
the ObjectMap of o1 . [n2,n] is set
the Arrows of i . ( the ObjectMap of o1 . (n2,n)) is set
( the ObjectMap of o1 * the Arrows of i) . [n2,n] is set
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Contravariant FunctorStr over C,i
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
proj1 the MorphMap of o1 is non empty set
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o1),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:])
<^o2,o1^> is set
the Arrows of C . (o2,o1) is set
the Arrows of C . [o2,o1] is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o1 . o2 is M2( the carrier of i)
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
[:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is non empty set
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
o1 is set
the MorphMap of o1 . o1 is Relation-like Function-like set
o2 is Relation-like Function-like set
p1 is set
p2 is set
[p1,p2] is V15() set
{p1,p2} is set
{p1} is set
{{p1,p2},{p1}} is set
n is M2( the carrier of C)
n2 is M2( the carrier of C)
the MorphMap of o1 . (n,n2) is set
[n,n2] is V15() set
{n,n2} is set
{n} is set
{{n,n2},{n}} is set
the MorphMap of o1 . [n,n2] is Relation-like Function-like set
Morph-Map (o1,n,n2) is Relation-like <^n,n2^> -defined <^(o1 . n2),(o1 . n)^> -valued Function-like quasi_total M2( bool [:<^n,n2^>,<^(o1 . n2),(o1 . n)^>:])
<^n,n2^> is set
the Arrows of C . (n,n2) is set
the Arrows of C . [n,n2] is set
o1 . n2 is M2( the carrier of i)
the ObjectMap of o1 . (n2,n2) is M2([: the carrier of i, the carrier of i:])
[n2,n2] is V15() set
{n2,n2} is set
{n2} is set
{{n2,n2},{n2}} is set
the ObjectMap of o1 . [n2,n2] is set
K40(( the ObjectMap of o1 . (n2,n2))) is set
o1 . n is M2( the carrier of i)
the ObjectMap of o1 . (n,n) is M2([: the carrier of i, the carrier of i:])
[n,n] is V15() set
{n,n} is set
{{n,n},{n}} is set
the ObjectMap of o1 . [n,n] is set
K40(( the ObjectMap of o1 . (n,n))) is set
<^(o1 . n2),(o1 . n)^> is set
the Arrows of i . ((o1 . n2),(o1 . n)) is set
[(o1 . n2),(o1 . n)] is V15() set
{(o1 . n2),(o1 . n)} is set
{(o1 . n2)} is set
{{(o1 . n2),(o1 . n)},{(o1 . n2)}} is set
the Arrows of i . [(o1 . n2),(o1 . n)] is set
[:<^n,n2^>,<^(o1 . n2),(o1 . n)^>:] is Relation-like set
bool [:<^n,n2^>,<^(o1 . n2),(o1 . n)^>:] is non empty set
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Covariant FunctorStr over C,i
o2 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 is M2( the carrier of C)
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
o2 is M2(<^(o1 . o2),(o1 . o1)^>)
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o2),(o1 . o1)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o2),(o1 . o1)^>:])
[:<^o2,o1^>,<^(o1 . o2),(o1 . o1)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o2),(o1 . o1)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
proj2 (Morph-Map (o1,o2,o1)) is set
proj1 (Morph-Map (o1,o2,o1)) is set
p1 is set
(Morph-Map (o1,o2,o1)) . p1 is set
p2 is M2(<^o2,o1^>)
o1 . p2 is M2(<^(o1 . o2),(o1 . o1)^>)
C is non empty AltCatStr
i is non empty AltCatStr
the carrier of C is non empty set
o1 is reflexive Contravariant FunctorStr over C,i
o1 is M2( the carrier of C)
o1 . o1 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
o2 is M2(<^(o1 . o1),(o1 . o2)^>)
Morph-Map (o1,o2,o1) is Relation-like <^o2,o1^> -defined <^(o1 . o1),(o1 . o2)^> -valued Function-like quasi_total M2( bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:])
[:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is Relation-like set
bool [:<^o2,o1^>,<^(o1 . o1),(o1 . o2)^>:] is non empty set
the MorphMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) V36() V37() MSUnTrans of the ObjectMap of o1, the Arrows of C, the Arrows of i
the MorphMap of o1 . (o2,o1) is set
the MorphMap of o1 . [o2,o1] is Relation-like Function-like set
proj2 (Morph-Map (o1,o2,o1)) is set
proj1 (Morph-Map (o1,o2,o1)) is set
p1 is set
(Morph-Map (o1,o2,o1)) . p1 is set
p2 is M2(<^o2,o1^>)
o1 . p2 is M2(<^(o1 . o1),(o1 . o2)^>)
C is non empty transitive with_units reflexive AltCatStr
i is non empty transitive with_units reflexive AltCatStr
the carrier of C is non empty set
o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i
o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{o1} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2(<^o2,o1^>)
o1 . o2 is M2(<^(o1 . o2),(o1 . o1)^>)
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
p1 is M2(<^o1,o2^>)
o1 . p1 is M2(<^(o1 . o1),(o1 . o2)^>)
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
o2 * p1 is M2(<^o1,o1^>)
<^o1,o1^> is non empty set
the Arrows of C . (o1,o1) is set
the Arrows of C . [o1,o1] is set
idm o1 is retraction coretraction mono epi M2(<^o1,o1^>)
(o1 . o2) * (o1 . p1) is M2(<^(o1 . o1),(o1 . o1)^>)
<^(o1 . o1),(o1 . o1)^> is non empty set
the Arrows of i . ((o1 . o1),(o1 . o1)) is set
[(o1 . o1),(o1 . o1)] is V15() set
{(o1 . o1),(o1 . o1)} is set
{{(o1 . o1),(o1 . o1)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o1)] is set
o1 . (idm o1) is M2(<^(o1 . o1),(o1 . o1)^>)
idm (o1 . o1) is retraction coretraction mono epi M2(<^(o1 . o1),(o1 . o1)^>)
C is non empty transitive with_units reflexive AltCatStr
i is non empty transitive with_units reflexive AltCatStr
the carrier of C is non empty set
o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i
o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{o1} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2(<^o2,o1^>)
o1 . o2 is M2(<^(o1 . o2),(o1 . o1)^>)
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
p1 is M2(<^o1,o2^>)
o1 . p1 is M2(<^(o1 . o1),(o1 . o2)^>)
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
p1 * o2 is M2(<^o2,o2^>)
<^o2,o2^> is non empty set
the Arrows of C . (o2,o2) is set
the Arrows of C . [o2,o2] is set
idm o2 is retraction coretraction mono epi M2(<^o2,o2^>)
(o1 . p1) * (o1 . o2) is M2(<^(o1 . o2),(o1 . o2)^>)
<^(o1 . o2),(o1 . o2)^> is non empty set
the Arrows of i . ((o1 . o2),(o1 . o2)) is set
[(o1 . o2),(o1 . o2)] is V15() set
{(o1 . o2),(o1 . o2)} is set
{{(o1 . o2),(o1 . o2)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o2)] is set
o1 . (idm o2) is M2(<^(o1 . o2),(o1 . o2)^>)
idm (o1 . o2) is retraction coretraction mono epi M2(<^(o1 . o2),(o1 . o2)^>)
C is non empty transitive V129() with_units reflexive AltCatStr
i is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i
o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
<^o2,o1^> is set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty V14([: the carrier of C, the carrier of C:]) set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Arrows of C . (o2,o1) is set
[o2,o1] is V15() set
{o2,o1} is set
{o2} is set
{{o2,o1},{o2}} is set
the Arrows of C . [o2,o1] is set
<^o1,o2^> is set
the Arrows of C . (o1,o2) is set
[o1,o2] is V15() set
{o1,o2} is set
{o1} is set
{{o1,o2},{o1}} is set
the Arrows of C . [o1,o2] is set
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{{o2,o2},{o2}} is set
the ObjectMap of o1 . [o2,o2] is set
K40(( the ObjectMap of o1 . (o2,o2))) is set
o1 . o1 is M2( the carrier of i)
the ObjectMap of o1 . (o1,o1) is M2([: the carrier of i, the carrier of i:])
[o1,o1] is V15() set
{o1,o1} is set
{{o1,o1},{o1}} is set
the ObjectMap of o1 . [o1,o1] is set
K40(( the ObjectMap of o1 . (o1,o1))) is set
o2 is M2(<^o2,o1^>)
o1 . o2 is M2(<^(o1 . o2),(o1 . o1)^>)
<^(o1 . o2),(o1 . o1)^> is set
the Arrows of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like non empty V14([: the carrier of i, the carrier of i:]) set
the Arrows of i . ((o1 . o2),(o1 . o1)) is set
[(o1 . o2),(o1 . o1)] is V15() set
{(o1 . o2),(o1 . o1)} is set
{(o1 . o2)} is set
{{(o1 . o2),(o1 . o1)},{(o1 . o2)}} is set
the Arrows of i . [(o1 . o2),(o1 . o1)] is set
<^(o1 . o1),(o1 . o2)^> is set
the Arrows of i . ((o1 . o1),(o1 . o2)) is set
[(o1 . o1),(o1 . o2)] is V15() set
{(o1 . o1),(o1 . o2)} is set
{(o1 . o1)} is set
{{(o1 . o1),(o1 . o2)},{(o1 . o1)}} is set
the Arrows of i . [(o1 . o1),(o1 . o2)] is set
C is non empty transitive V129() with_units reflexive AltCatStr
i is non empty transitive V129() with_units reflexive AltCatStr
the carrier of C is non empty set
o1 is reflexive feasible Covariant id-preserving comp-preserving covariant Functor of C,i
o2 is M2( the carrier of C)
o1 is M2( the carrier of C)
o1 . o2 is M2( the carrier of i)
the carrier of i is non empty set
[: the carrier of i, the carrier of i:] is Relation-like non empty set
the ObjectMap of o1 is Relation-like [: the carrier of C, the carrier of C:] -defined [: the carrier of i, the carrier of i:] -valued Function-like quasi_total M2( bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:])
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:],[: the carrier of i, the carrier of i:]:] is non empty set
the ObjectMap of o1 . (o2,o2) is M2([: the carrier of i, the carrier of i:])
[o2,o2] is V15() set
{o2,o2} is set
{o2