for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = F₁() & ( for a, b being Element of F₁()
for f being Element of F₂() st P₁[a,b,f] holds
[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F₁() ex f being Element of F₂() st
( m = [[a,b],f] & P₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C1
for a1, a2, a3 being Element of F₁()
for f1, f2 being Element of F₂() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F₃(f2,f1)] ) & the carrier of C2 = F₁() & ( for a, b being Element of F₁()
for f being Element of F₂() st P₁[a,b,f] holds
[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F₁() ex f being Element of F₂() st
( m = [[a,b],f] & P₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C2
for a1, a2, a3 being Element of F₁()
for f1, f2 being Element of F₂() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F₃(f2,f1)] ) holds
C1 = C2

for a being Element of F₁() ex f being Element of F₂() st
( P₁[a,a,f] & ( for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[a,b,g] implies F₃(g,f) = g ) & ( P₁[b,a,g] implies F₃(f,g) = g ) ) ) )