fact: Definition Full_law0'' (F : Functor0'' C D) (H : forall a b : C, Hom'' (F a) (F b) -> (a --> b)) := forall (a b : C) (h : Hom'' (F a) (F b)), h =_S'' FMor0'' F (H a b h).
imports: Category Category_dup2 Map0_dup1 Setoid_dup2