Commit 2022-04-11 20:58 e8339bd6

feat(category_theory/fully_faithful): nat_trans_of_comp_fully_faithful (#13327) I added nat_iso_of_comp_fully_faithful in an earlier PR, but left out the more basic construction.