proposition: Theorem cone_coherence_auto1 (x y : J) (f : x ~> y) (w z : C) (g : w ~> z) (A : ACone z F) : fmap[F] f ∘ (vertex_map A x ∘ g) ≈ vertex_map A y ∘ g.
proof: Proof. now rewrite comp_assoc, cone_coherence. Qed.
imports: Category.Lib Category.Lib.Tactics2 Category.Theory.Category Category.Theory.Isomorphism Category.Construction.Opposite Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Hom Category.Instance.Sets Category.Structure.UniversalProperty Category.Structure.Cone Category.Structure.Limit Category.Functor.Hom.Yoneda