Nuprl Definition : cat-square-commutes
x_y1 o y1_z = x_y2 o y2_z == (cat-comp(C) x y1 z x_y1 y1_z) = (cat-comp(C) x y2 z x_y2 y2_z) ∈ (cat-arrow(C) x z)
Definitions occuring in Statement :
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
apply: f a,
cat-comp: cat-comp(C)
FDL editor aliases :
cat-square-commutes
Latex:
x$_{y1}$ o y1$_{z}$ = x$_{y2}$ o y2$\000C_{z}$ == (cat-comp(C) x y1 z x$_{y1}$ y1$_{z}\mbackslash{}f\000Cf24) = (cat-comp(C) x y2 z x$_{y2}$ y2$_{z}$)
Date html generated:
2020_05_20-AM-07_54_50
Last ObjectModification:
2015_09_23-AM-09_29_17
Theory : small!categories
Home
Index