proposition: Lemma invert_comp (Fff : ff_struct) {X Y Z} (f:D⦅F Y;F Z⦆) (g:D⦅F X;F Y⦆): Fff _ _ (f ∙ g) ∼ Fff _ _ f ∙ Fff _ _ g.
proof: Proof. rewrite -{1}(ff_section Fff f) -{1}(ff_section Fff g) -functor_law2 ff_retraction ; reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)