fun 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def (f o g)(x) == f(g(x))

is mentioned by

Thm* f:(AB). f o Id = f[comp_id_r]
Thm* f:(AB). Id o f = f[comp_id_l]
Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f  AD[comp_assoc]
Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id[inv_funs]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

fun 1 Sections StandardLIB Doc