"Generate co's" include "cross.cat" let invrf = rf^-1 let cobase = co0 with co from generate_cos(cobase) (* From now, co is a coherence order *) let coi = co & int let coe = co \ coi (* Compute fr *) let fr = (invrf ; co) \ id let fri = fr & int let fre = fr \ fri show co,fr