proposition: Lemma whisker_flip A B C (F : A ⟶ B) (G : B ⟶ C) : (to (nat_λ G) ⊲ F) ∙ to (nat_α F Id G) ≈ G ⊳ (to (nat_ρ F)).
proof: Proof. simpl; intros; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Instance.Sets