proposition: Corollary fst_comp {C : Category} {D : Category} x y z (f : y ~{C ∏ D}~> z) (g : x ~{C ∏ D}~> y) : fst f ∘ fst g ≈ fst (f ∘ g).
proof: Proof. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor