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

theorem test2:
  fixes a⇩1 b⇩1 and c⇩1 c⇩2 and  d⇩1  d⇩2  and f ::"unit × bool" and x :: "unit × bool"
  defines "C ≡ ⦇hom = (λx. undefined)(a⇩1 := (λx. undefined)(a⇩1 := {})), comp = (λx. undefined)(a⇩1 := (λx. undefined)(a⇩1 := (λx. undefined)(a⇩1 := (λx. undefined)(b⇩1 := (λx. undefined)(b⇩1 := b⇩1)))))⦈"
  defines "D ≡  ⦇hom = (λx. undefined)(d⇩1 := (λx. undefined)(d⇩1 := {}, d⇩2 := {}), d⇩2 := (λx. undefined)(d⇩1 := {}, d⇩2 := {})),
           comp = (λx. undefined)
             (d⇩1 := (λx. undefined)
                (d⇩1 := (λx. undefined)(d⇩1 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2)), d⇩2 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2))),
                 d⇩2 := (λx. undefined)(d⇩1 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2)), d⇩2 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2)))),
              d⇩2 := (λx. undefined)
                (d⇩1 := (λx. undefined)(d⇩1 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2)), d⇩2 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2))),
                 d⇩2 := (λx. undefined)(d⇩1 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2)), d⇩2 := (λx. undefined)(c⇩1 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2), c⇩2 := (λx. undefined)(c⇩1 := c⇩2, c⇩2 := c⇩2)))))⦈"
  defines "f ≡ (b⇩1, c⇩1)"
  shows " (hom (ProductPrecategory C D) x y) = {}"
  unfolding assms apply (auto simp: Assoc_def ProductPrecategory_def)
  oops


theorem test2 :
  assumes H: "Assoc C" "f ∈ hom (ProductPrecategory C D) x y"
  shows "(fst f) ∈ hom C (fst x) (fst y)"
  supply [[show_types]]
  using assms nitpick[eval="f" "hom C (fst x) (fst y) " " hom (ProductPrecategory C D) x y" "f ∈ hom (ProductPrecategory C D) x y "]

theorem test2 :
  assumes H: "Assoc C" "f ∈ hom (ProductPrecategory C D) x y"
  shows "(fst f) ∈ hom C (fst x) (fst y)"
  supply [[show_types]]
  using assms nitpick[debug, card=1-2]