show (cat_n n) is a discrete category, part 3
update to accommodate a change to RezkCompletion
clean up