fact: Definition Hom_comp_assoc := forall (a b c d : Ob) (f : Hom a b) (g : Hom b c) (h : Hom c d), Equal (Hom_comp a b d (couple (Hom_comp b c d (couple h g)) f)) (Hom_comp a c d (couple h (Hom_comp a b c (couple g f)))).
imports: Cartesian