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