proposition: Lemma whisker_right_dist A B C (F G H : A ⟶ B) (J : B ⟶ C) (η : F ⟹ G) (θ : G ⟹ H) : (J ⊳ θ) ∙ (J ⊳ η) ≈ J ⊳ (θ ∙ η).
proof: Proof. simpl; intros; cat. now rewrite fmap_comp. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Instance.Sets