Grant#7. Thanks. The part I still don't understand is "there's exactly one morphism from x to y" in John#5. But I suppose I'll have to wait for John to clarify his wording there.