working on second pasting lemma. sync.
modified:   Categories.agda