theory ProductCategory
  imports Main
begin

record ('obj, 'arr) Precategory =
    hom :: "'obj ⇒ 'obj ⇒ 'arr set"
    comp :: "'obj ⇒ 'obj ⇒ 'obj ⇒ 'arr ⇒ 'arr ⇒ 'arr"

locale Assoc =
  fixes C :: "('obj, 'arr) Precategory"
  assumes
    comp_assoc : "⟦ f ∈ hom C w x ; g ∈ hom C x y ; h ∈ hom C y z ⟧ ⟹
      comp C w y z (comp C w x y f g) h = comp C w x z f (comp C x y z g h)"

definition ProductPrecategory :: "('objC, 'arrC) Precategory ⇒ ('objD,
'arrD) Precategory ⇒
    ('objC × 'objD, 'arrC × 'arrD) Precategory" where
  "ProductPrecategory C D ≡
    ⦇
    hom = λ c1 c2. (hom C (fst c1) (fst c2)) × (hom D (snd c1) (snd c2)),
    comp = λ c1 c2 c3 f g.
      (comp C (fst c1) (fst c2) (fst c3) (fst f) (fst g),
       comp D (snd c1) (snd c2) (snd c3) (snd f) (snd g))
 ⦈"

theorem test : "Assoc C ⟹
f ∈ hom (ProductPrecategory C D) x y ⟹ (fst f) ∈ hom C (fst x) (fst y)"
  by (metis (no_types, lifting) ProductPrecategory_def SigmaD1 ext_inject
prod.exhaust_sel surjective)

theorem test2 : "Assoc C ⟹
f ∈ hom (ProductPrecategory C D) x y ⟹ (fst f) ∈ hom C (fst x) (fst y)"
  nitpick