abstract B = {

cat S ;

fun f : S -> S 1 ;

}