is mentioned by

Thm* f:(AB), g:(BC). Inj(A; B; f) Inj(B; C; g) Inj(A; C; g o f)	[compose_inject]
Thm* f,g:Top, s:Top List. map(f;map(g;s)) ~ map(f o g;s)	[map-map]
Thm* f:(AB), g:(BC). Bij(A; B; f) Bij(B; C; g) Bij(A; C; g o f)	[compose-biject]
Thm* h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h	[comp2_comp2_assoc]
Thm* h:(A'A), g:(ABC), f1:(BB'), f2:(CC'). (f1,f2) o g o h = (f1,f2) o g o h	[comp2_comp_assoc]

In prior sections: fun 1 list 1 mb nat mb list 1 mb list 2

Try larger context: Graphs