Apologies for the faulty messages. Eleven replies! Thanks to everyone. Two obvious benefits: a line is easier to type and occupies less space than a vertical arrow. Ross Street wrote, "It means there is a natural bijection. ..." Micah Blake McCurdy wrote, "... The notation itself goes back to Gentzen, I think, but the meaning was not the same there -- he meant that the implication below the line could be deduced from the implication above the line." Andrej Bauer wrote, "In logic ... you put a double horizontal line if you want to emphasize that the rule goes both ways." So in Cat. Th., a single line might represent an arrow while a double line would represent a bijection? Apparently this convention isn't well established. Regards, ... Peter E. -- http://members.shaw.ca/peasthope/ http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/