Make functor arguments of nat_trans_comp implicit #1981

The three functors F G H in

Definition nat_trans_comp {C:precategory_data}{C' : precategory}
  (F G H: functor_data C C')
  (a : nat_trans F G)
  (b : nat_trans G H): nat_trans F H :=
    tpair _ _ (is_nat_trans_comp a b).

are explicit arguments, but every definition (or 99% of them) uses _ _ _ to let coq infer them, or even depends on some Arguments nat_trans_comp {_ _ _ _ _} _ _. to make them implicit. However, they are still displayed in goals, which makes those goals harder to read.

I think it would be a good idea to make them implicit by default.