-- Products and coproducts by their universal property
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Category.Product
import Opposite

-- (p, p1, p2) is a product of a and b: every pair f : x → a, g : x → b
-- factors uniquely through p.
predicate IsProduct (C a b p p1 p2 : Set) :=
  p ∈ Category.obj(C) ∧ p1 ∈ hom(C, p, a) ∧ p2 ∈ hom(C, p, b) ∧
  (∀ x ∈ obj(C), ∀ f ∈ hom(C, x, a), ∀ g ∈ hom(C, x, b),
    ∃ h ∈ hom(C, x, p), comp(C)(p1, h) = f ∧ comp(C)(p2, h) = g ∧
      (∀ k ∈ hom(C, x, p), comp(C)(p1, k) = f → comp(C)(p2, k) = g → k = h))

notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis IsProduct(C, a, b, p, p1, p2) for C.mor

-- A coproduct is a product in the opposite category.
predicate IsCoproduct (C a b p i1 i2 : Set) :=
  IsProduct(opposite(C), a, b, p, i1, i2)

theorem IsProduct.object (C a b p p1 p2 : Set)
  requires product : IsProduct(C, a, b, p, p1, p2)
  shows p ∈ obj(C)
proof
  obtain ⟨pInO, rest⟩ := product
  exact pInO

theorem IsProduct.first (C a b p p1 p2 : Set)
  requires product : IsProduct(C, a, b, p, p1, p2)
  shows p1 ∈ hom(C, p, a)
proof
  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product
  exact firstHom

theorem IsProduct.second (C a b p p1 p2 : Set)
  requires product : IsProduct(C, a, b, p, p1, p2)
  shows p2 ∈ hom(C, p, b)
proof
  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product
  exact secondHom

theorem IsProduct.universal (C a b p p1 p2 x f g : Set)
  requires product : IsProduct(C, a, b, p, p1, p2)
  requires xInO : x ∈ obj(C)
  requires fHom : f ∈ hom(C, x, a)
  requires gHom : g ∈ hom(C, x, b)
  shows ∃ h ∈ hom(C, x, p), p1 ∘ h = f ∧ p2 ∘ h = g ∧
    (∀ k ∈ hom(C, x, p), p1 ∘ k = f → p2 ∘ k = g → k = h)
proof
  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product
  exact universal with x, xInO, f, fHom, g, gHom

-- Two morphisms into a product with the same components are equal.
theorem IsProduct.ext (C a b p p1 p2 x h k : Set)
  requires category : Category(C)
  requires product : IsProduct(C, a, b, p, p1, p2)
  requires xInO : x ∈ obj(C)
  requires hHom : h ∈ hom(C, x, p)
  requires kHom : k ∈ hom(C, x, p)
  requires sameFirst : p1 ∘ h = p1 ∘ k
  requires sameSecond : p2 ∘ h = p2 ∘ k
  shows h = k
proof
  have firstHom := IsProduct.first with product
  have secondHom := IsProduct.second with product
  have fHom := hom.comp with category, firstHom, hHom
  have gHom := hom.comp with category, secondHom, hHom
  obtain ⟨u, uHom, firstLaw, secondLaw, unique⟩ :=
    IsProduct.universal with product, xInO, fHom, gHom
  have hFirst : p1 ∘ h = p1 ∘ h by rfl
  have hSecond : p2 ∘ h = p2 ∘ h by rfl
  have hEqual := unique with h, hHom, hFirst, hSecond
  have kFirst : p1 ∘ k = p1 ∘ h by cc
  have kSecond : p2 ∘ k = p2 ∘ h by cc
  have kEqual := unique with k, kHom, kFirst, kSecond
  calc
    h = u := hEqual
    _ = k := by rw kEqual

-- The pairing of f : x → a and g : x → b through the product.
defunique pairing (C a b p p1 p2 x f g : Set) (h ∈ hom(C, x, p)) :=
  comp(C)(p1, h) = f ∧ comp(C)(p2, h) = g
requires product : IsProduct(C, a, b, p, p1, p2)
requires xInO : x ∈ obj(C)
requires fHom : f ∈ hom(C, x, a)
requires gHom : g ∈ hom(C, x, b)
proof
  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=
    IsProduct.universal with product, xInO, fHom, gHom
  refine ⟨h, hHom, firstLaw, secondLaw⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=
    IsProduct.universal with product, xInO, fHom, gHom
  have uEqual := unique with u, hu, first.left, first.right
  have vEqual := unique with v, hv, second.left, second.right
  cc

section ProductLaws
variable (C a b p p1 p2 : Set)
hypothesis category : Category(C)
hypothesis product : IsProduct(C, a, b, p, p1, p2)

theorem pairing.hom (x f g : Set)
  requires xInO : x ∈ obj(C)
  requires fHom : f ∈ hom(C, x, a)
  requires gHom : g ∈ hom(C, x, b)
  shows pairing(C, a, b, p, p1, p2, x, f, g) ∈
    hom(C, x, p)
proof
  have selected := pairing.selected at C, a, b, p, p1, p2, x, f, g with
    product, xInO, fHom, gHom
  exact selected.left

theorem pairing.first (x f g : Set)
  requires xInO : x ∈ obj(C)
  requires fHom : f ∈ hom(C, x, a)
  requires gHom : g ∈ hom(C, x, b)
  shows p1 ∘ pairing(C, a, b, p, p1, p2, x, f, g) = f
proof
  have selected := pairing.selected at C, a, b, p, p1, p2, x, f, g with
    product, xInO, fHom, gHom
  exact selected.right.left

theorem pairing.second (x f g : Set)
  requires xInO : x ∈ obj(C)
  requires fHom : f ∈ hom(C, x, a)
  requires gHom : g ∈ hom(C, x, b)
  shows p2 ∘ pairing(C, a, b, p, p1, p2, x, f, g) = g
proof
  have selected := pairing.selected at C, a, b, p, p1, p2, x, f, g with
    product, xInO, fHom, gHom
  exact selected.right.right

theorem pairing.eq (x f g k : Set)
  requires xInO : x ∈ obj(C)
  requires fHom : f ∈ hom(C, x, a)
  requires gHom : g ∈ hom(C, x, b)
  requires kHom : k ∈ hom(C, x, p)
  requires firstLaw : p1 ∘ k = f
  requires secondLaw : p2 ∘ k = g
  shows k = pairing(C, a, b, p, p1, p2, x, f, g)
proof
  have pairingHom := pairing.hom with category, product, xInO, fHom, gHom
  have pairingFirst := pairing.first with category, product, xInO, fHom, gHom
  have pairingSecond := pairing.second with category, product, xInO, fHom, gHom
  have sameFirst : p1 ∘ k = p1 ∘ pairing(C, a, b, p,
      p1, p2, x, f, g)
    calc
      p1 ∘ k = f := firstLaw
      _ = p1 ∘ pairing(C, a, b, p, p1, p2, x, f,
          g) := by rw pairingFirst
  have sameSecond : p2 ∘ k = p2 ∘ pairing(C, a, b, p,
      p1, p2, x, f, g)
    calc
      p2 ∘ k = g := secondLaw
      _ = p2 ∘ pairing(C, a, b, p, p1, p2, x, f,
          g) := by rw pairingSecond
  exact IsProduct.ext with
    category, product, xInO, kHom, pairingHom, sameFirst, sameSecond

-- Pairing the projections gives the identity of the product.
theorem pairing.projections
  shows pairing(C, a, b, p, p1, p2, p, p1, p2) = id(C)(p)
proof
  have pInO := IsProduct.object with product
  have firstHom := IsProduct.first with product
  have secondHom := IsProduct.second with product
  have idHom := hom.id with category, pInO
  have firstLaw := Category.id_right_hom with category, firstHom
  have secondLaw := Category.id_right_hom with category, secondHom
  have equal := pairing.eq with category, product, pInO, firstHom, secondHom,
    idHom, firstLaw, secondLaw
  symm
  exact equal

-- Pairing is natural in the source object.
theorem pairing.comp (x y f g u : Set)
  requires xInO : x ∈ obj(C)
  requires yInO : y ∈ obj(C)
  requires fHom : f ∈ hom(C, x, a)
  requires gHom : g ∈ hom(C, x, b)
  requires uHom : u ∈ hom(C, y, x)
  shows pairing(C, a, b, p, p1, p2, x, f, g) ∘ u =
    pairing(C, a, b, p, p1, p2, y, f ∘ u, g ∘ u)
proof
  have pairingHom := pairing.hom with category, product, xInO, fHom, gHom
  have pairingFirst := pairing.first with category, product, xInO, fHom, gHom
  have pairingSecond := pairing.second with category, product, xInO, fHom, gHom
  have firstHom := IsProduct.first with product
  have secondHom := IsProduct.second with product
  have fuHom := hom.comp with category, fHom, uHom
  have guHom := hom.comp with category, gHom, uHom
  have compositeHom := hom.comp with category, pairingHom, uHom
  have assocFirst := Category.assoc_hom with
    category, firstHom, pairingHom, uHom
  have assocSecond := Category.assoc_hom with
    category, secondHom, pairingHom, uHom
  have firstLaw : p1 ∘ (pairing(C, a, b, p, p1, p2, x,
      f, g) ∘ u) = f ∘ u
    calc
      p1 ∘ (pairing(C, a, b, p, p1, p2, x, f, g) ∘ u) =
          (p1 ∘ pairing(C, a, b, p, p1, p2, x, f,
              g)) ∘ u := by rw assocFirst
      _ = f ∘ u := by rw pairingFirst
  have secondLaw : p2 ∘ (pairing(C, a, b, p, p1, p2, x,
      f, g) ∘ u) = g ∘ u
    calc
      p2 ∘ (pairing(C, a, b, p, p1, p2, x, f, g) ∘ u) =
          (p2 ∘ pairing(C, a, b, p, p1, p2, x, f,
              g)) ∘ u := by rw assocSecond
      _ = g ∘ u := by rw pairingSecond
  exact pairing.eq with category, product, yInO, fuHom, guHom, compositeHom,
    firstLaw, secondLaw

theorem IsProduct.swap
  shows IsProduct(C, b, a, p, p2, p1)
proof
  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product
  unfold IsProduct
  refine ⟨pInO, secondHom, firstHom, ?_⟩
  intros x xInO g gHom f fHom
  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=
    universal with x, xInO, f, fHom, g, gHom
  refine ⟨h, hHom, secondLaw, firstLaw, ?_⟩
  intros k kHom kSecond kFirst
  exact unique with k, kHom, kFirst, kSecond

-- Products of the same objects are isomorphic through the pairings.
theorem IsProduct.inverse_pair (q q1 q2 : Set)
  requires other : IsProduct(C, a, b, q, q1, q2)
  shows InversePair(C, pairing(C, a, b, q, q1, q2, p, p1, p2),
    pairing(C, a, b, p, p1, p2, q, q1, q2))
proof
  have pInO := IsProduct.object with product
  have qInO := IsProduct.object with other
  have firstP := IsProduct.first with product
  have secondP := IsProduct.second with product
  have firstQ := IsProduct.first with other
  have secondQ := IsProduct.second with other
  have hHom := pairing.hom with category, other, pInO, firstP, secondP
  have hFirst := pairing.first with category, other, pInO, firstP, secondP
  have hSecond := pairing.second with category, other, pInO, firstP, secondP
  have kHom := pairing.hom with category, product, qInO, firstQ, secondQ
  have kFirst := pairing.first with category, product, qInO, firstQ, secondQ
  have kSecond := pairing.second with category, product, qInO, firstQ, secondQ
  have khHom := hom.comp with category, kHom, hHom
  have hkHom := hom.comp with category, hHom, kHom
  have idP := hom.id with category, pInO
  have idQ := hom.id with category, qInO
  have assocPFirst := Category.assoc_hom with category, firstP, kHom, hHom
  have assocPSecond := Category.assoc_hom with category, secondP, kHom, hHom
  have assocQFirst := Category.assoc_hom with category, firstQ, hHom, kHom
  have assocQSecond := Category.assoc_hom with category, secondQ, hHom, kHom
  have unitPFirst := Category.id_right_hom with category, firstP
  have unitPSecond := Category.id_right_hom with category, secondP
  have unitQFirst := Category.id_right_hom with category, firstQ
  have unitQSecond := Category.id_right_hom with category, secondQ
  have khFirst : p1 ∘ (pairing(C, a, b, p, p1, p2, q,
      q1, q2) ∘
      pairing(C, a, b, q, q1, q2, p, p1,
          p2)) = p1 ∘ id(C)(p)
    calc
      p1 ∘ (pairing(C, a, b, p, p1, p2, q, q1, q2) ∘
          pairing(C, a, b, q, q1, q2, p, p1, p2)) =
        (p1 ∘ pairing(C, a, b, p, p1, p2, q, q1, q2)) ∘
          pairing(C, a, b, q, q1, q2, p, p1,
              p2) := by rw assocPFirst
      _ = q1 ∘ pairing(C, a, b, q, q1, q2, p, p1,
          p2) := by rw kFirst
      _ = p1 := hFirst
      _ = p1 ∘ id(C)(p) := by rw unitPFirst
  have khSecond : p2 ∘ (pairing(C, a, b, p, p1, p2, q,
      q1, q2) ∘
      pairing(C, a, b, q, q1, q2, p, p1,
          p2)) = p2 ∘ id(C)(p)
    calc
      p2 ∘ (pairing(C, a, b, p, p1, p2, q, q1, q2) ∘
          pairing(C, a, b, q, q1, q2, p, p1, p2)) =
        (p2 ∘ pairing(C, a, b, p, p1, p2, q, q1, q2)) ∘
          pairing(C, a, b, q, q1, q2, p, p1,
              p2) := by rw assocPSecond
      _ = q2 ∘ pairing(C, a, b, q, q1, q2, p, p1,
          p2) := by rw kSecond
      _ = p2 := hSecond
      _ = p2 ∘ id(C)(p) := by rw unitPSecond
  have khId := IsProduct.ext with
    category, product, pInO, khHom, idP, khFirst, khSecond
  have hkFirst : q1 ∘ (pairing(C, a, b, q, q1, q2, p,
      p1, p2) ∘
      pairing(C, a, b, p, p1, p2, q, q1,
          q2)) = q1 ∘ id(C)(q)
    calc
      q1 ∘ (pairing(C, a, b, q, q1, q2, p, p1, p2) ∘
          pairing(C, a, b, p, p1, p2, q, q1, q2)) =
        (q1 ∘ pairing(C, a, b, q, q1, q2, p, p1, p2)) ∘
          pairing(C, a, b, p, p1, p2, q, q1,
              q2) := by rw assocQFirst
      _ = p1 ∘ pairing(C, a, b, p, p1, p2, q, q1,
          q2) := by rw hFirst
      _ = q1 := kFirst
      _ = q1 ∘ id(C)(q) := by rw unitQFirst
  have hkSecond : q2 ∘ (pairing(C, a, b, q, q1, q2, p,
      p1, p2) ∘
      pairing(C, a, b, p, p1, p2, q, q1,
          q2)) = q2 ∘ id(C)(q)
    calc
      q2 ∘ (pairing(C, a, b, q, q1, q2, p, p1, p2) ∘
          pairing(C, a, b, p, p1, p2, q, q1, q2)) =
        (q2 ∘ pairing(C, a, b, q, q1, q2, p, p1, p2)) ∘
          pairing(C, a, b, p, p1, p2, q, q1,
              q2) := by rw assocQSecond
      _ = p2 ∘ pairing(C, a, b, p, p1, p2, q, q1,
          q2) := by rw hSecond
      _ = q2 := kSecond
      _ = q2 ∘ id(C)(q) := by rw unitQSecond
  have hkId := IsProduct.ext with
    category, other, qInO, hkHom, idQ, hkFirst, hkSecond
  have hInM := hom.in_morphisms with hHom
  have kInM := hom.in_morphisms with kHom
  have domH := hom.dom with hHom
  have codH := hom.cod with hHom
  have domK := hom.dom with kHom
  have codK := hom.cod with kHom
  unfold InversePair
  refine ⟨hInM, kInM, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . calc
      pairing(C, a, b, p, p1, p2, q, q1, q2) ∘
          pairing(C, a, b, q, q1, q2, p, p1,
              p2) = id(C)(p) := khId
      _ = id(C)(dom(C)(pairing(C, a, b, q, q1, q2, p, p1,
          p2))) := by rw domH
  . calc
      pairing(C, a, b, q, q1, q2, p, p1, p2) ∘
          pairing(C, a, b, p, p1, p2, q, q1,
              q2) = id(C)(q) := hkId
      _ = id(C)(cod(C)(pairing(C, a, b, q, q1, q2, p, p1,
          p2))) := by rw codH

theorem IsProduct.isomorphic (q q1 q2 : Set)
  requires other : IsProduct(C, a, b, q, q1, q2)
  shows Isomorphic(C, p, q)
proof
  have pInO := IsProduct.object with product
  have firstP := IsProduct.first with product
  have secondP := IsProduct.second with product
  have hHom := pairing.hom with category, other, pInO, firstP, secondP
  have pair := IsProduct.inverse_pair with category, product, other
  have iso := Isomorphism.of_pair with pair
  exact Isomorphic.of_hom with hHom, iso

-- The product is commutative up to isomorphism.
theorem IsProduct.commutative (q q1 q2 : Set)
  requires other : IsProduct(C, b, a, q, q1, q2)
  shows Isomorphic(C, p, q)
proof
  have swapped := IsProduct.swap with category, product
  exact IsProduct.isomorphic with category, swapped, other

-- A product transported along an isomorphism is a product.
theorem IsProduct.of_inverse_pair (q u v : Set)
  requires pair : InversePair(C, u, v)
  requires uHom : u ∈ hom(C, q, p)
  shows IsProduct(C, a, b, q, p1 ∘ u, p2 ∘ u)
proof
  have pInO := IsProduct.object with product
  have firstP := IsProduct.first with product
  have secondP := IsProduct.second with product
  have vHom := InversePair.in_hom with pair, uHom
  have uInM := hom.in_morphisms with uHom
  have qInO : q ∈ obj(C)
    have domIn := Category.dom_closed with category, uInM
    have domU := hom.dom with uHom
    rwa domU at domIn
  have firstHom := hom.comp with category, firstP, uHom
  have secondHom := hom.comp with category, secondP, uHom
  have vu := InversePair.left with pair
  have uv := InversePair.right with pair
  have domU := hom.dom with uHom
  have codU := hom.cod with uHom
  unfold IsProduct
  refine ⟨qInO, firstHom, secondHom, ?_⟩
  intros x xInO f fHom g gHom
  have hHom := pairing.hom with category, product, xInO, fHom, gHom
  have hFirst := pairing.first with category, product, xInO, fHom, gHom
  have hSecond := pairing.second with category, product, xInO, fHom, gHom
  have vhHom := hom.comp with category, vHom, hHom
  have uvhHom := hom.comp with category, uHom, vhHom
  have assocU := Category.assoc_hom with category, uHom, vHom, hHom
  have unitH := Category.id_left_hom with category, hHom
  have uvId : u ∘ v = id(C)(p)
    rwa codU at uv
  have vuId : v ∘ u = id(C)(q)
    rwa domU at vu
  have uvh : u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f,
      g)) =
      pairing(C, a, b, p, p1, p2, x, f, g)
    calc
      u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f, g)) =
          (u ∘ v) ∘ pairing(C, a, b, p, p1, p2, x, f,
              g) := by rw assocU
      _ = id(C)(p) ∘ pairing(C, a, b, p, p1, p2, x, f,
          g) := by rw uvId
      _ = pairing(C, a, b, p, p1, p2, x, f, g) := unitH
  have assocFirst := Category.assoc_hom with category, firstP, uHom, vhHom
  have assocSecond := Category.assoc_hom with category, secondP, uHom, vhHom
  refine ⟨v ∘ pairing(C, a, b, p, p1, p2, x, f, g),
    vhHom, ?_, ?_, ?_⟩
  . calc
      (p1 ∘ u) ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f,
          g)) =
          p1 ∘ (u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x,
              f, g))) :=
        assocFirst
      _ = p1 ∘ pairing(C, a, b, p, p1, p2, x, f,
          g) := by rw uvh
      _ = f := hFirst
  . calc
      (p2 ∘ u) ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f,
          g)) =
          p2 ∘ (u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x,
              f, g))) :=
        assocSecond
      _ = p2 ∘ pairing(C, a, b, p, p1, p2, x, f,
          g) := by rw uvh
      _ = g := hSecond
  . intros k kHom kFirst kSecond
    have ukHom := hom.comp with category, uHom, kHom
    have assocKFirst := Category.assoc_hom with category, firstP, uHom, kHom
    have assocKSecond := Category.assoc_hom with category, secondP, uHom, kHom
    have ukFirst : p1 ∘ (u ∘ k) = f
      calc
        p1 ∘ (u ∘ k) = (p1 ∘ u) ∘ k := by rw assocKFirst
        _ = f := kFirst
    have ukSecond : p2 ∘ (u ∘ k) = g
      calc
        p2 ∘ (u ∘ k) = (p2 ∘ u) ∘ k := by rw assocKSecond
        _ = g := kSecond
    have ukEqual := pairing.eq with
      category, product, xInO, fHom, gHom, ukHom, ukFirst, ukSecond
    have assocVU := Category.assoc_hom with category, vHom, uHom, kHom
    have unitK := Category.id_left_hom with category, kHom
    calc
      k = id(C)(q) ∘ k := by rw unitK
      _ = (v ∘ u) ∘ k := by rw vuId
      _ = v ∘ (u ∘ k) := assocVU
      _ = v ∘ pairing(C, a, b, p, p1, p2, x, f,
          g) := by rw ukEqual

end ProductLaws

-- The diagonal of an object through a product of it with itself.
theorem IsProduct.diagonal_first (C a p p1 p2 : Set)
  requires category : Category(C)
  requires product : IsProduct(C, a, a, p, p1, p2)
  requires aInO : a ∈ obj(C)
  shows p1 ∘ pairing(C, a, a, p, p1, p2, a,
    id(C)(a), id(C)(a)) = id(C)(a)
proof
  have idHom := hom.id with category, aInO
  exact pairing.first with category, product, aInO, idHom, idHom

theorem IsProduct.diagonal_second (C a p p1 p2 : Set)
  requires category : Category(C)
  requires product : IsProduct(C, a, a, p, p1, p2)
  requires aInO : a ∈ obj(C)
  shows p2 ∘ pairing(C, a, a, p, p1, p2, a,
    id(C)(a), id(C)(a)) = id(C)(a)
proof
  have idHom := hom.id with category, aInO
  exact pairing.second with category, product, aInO, idHom, idHom

theorem IsProduct.diagonal_split_mono (C a p p1 p2 : Set)
  requires category : Category(C)
  requires product : IsProduct(C, a, a, p, p1, p2)
  requires aInO : a ∈ obj(C)
  shows SplitMonomorphism(C, pairing(C, a, a, p, p1, p2, a, id(C)(a), id(C)(a)))
proof
  have idHom := hom.id with category, aInO
  have diagonalHom := pairing.hom with category, product, aInO, idHom, idHom
  have firstLaw := IsProduct.diagonal_first with category, product, aInO
  have firstP := IsProduct.first with product
  have diagonalInM := hom.in_morphisms with diagonalHom
  have firstInM := hom.in_morphisms with firstP
  have domDiagonal := hom.dom with diagonalHom
  have codDiagonal := hom.cod with diagonalHom
  have domFirst := hom.dom with firstP
  have codFirst := hom.cod with firstP
  have retraction : Retraction(C, pairing(C, a, a, p, p1, p2, a, id(C)(a), id(C)(a)), p1)
    unfold Retraction
    refine ⟨diagonalInM, firstInM, ?_, ?_, ?_⟩
    . cc
    . cc
    . cc
  exact SplitMonomorphism.of_retraction with retraction

-- A terminal object is a unit for the product.
theorem IsProduct.terminal (C a t : Set)
  requires category : Category(C)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  shows IsProduct(C, a, t, a, id(C)(a),
    terminalMorphism(C, t, a))
proof
  have idHom := hom.id with category, aInO
  have toTerminal := terminalMorphism.hom with terminal, aInO
  unfold IsProduct
  refine ⟨aInO, idHom, toTerminal, ?_⟩
  intros x xInO f fHom g gHom
  have unitF := Category.id_left_hom with category, fHom
  have composite := terminalMorphism.comp with category, terminal, xInO, fHom
  have gEqual := terminalMorphism.eq with terminal, xInO, gHom
  refine ⟨f, fHom, unitF, ?_, ?_⟩
  . calc
      terminalMorphism(C, t, a) ∘ f =
          terminalMorphism(C, t, x) := composite
      _ = g := by rw gEqual
  . intros k kHom kFirst kSecond
    have unitK := Category.id_left_hom with category, kHom
    calc
      k = id(C)(a) ∘ k := by rw unitK
      _ = f := kFirst

-- Coproducts, through the opposite category.
theorem IsCoproduct.object (C a b p i1 i2 : Set)
  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)
  shows p ∈ obj(C)
proof
  unfold IsCoproduct at coproduct
  have pIn := IsProduct.object with coproduct
  rwa opposite.obj at pIn

theorem IsCoproduct.first (C a b p i1 i2 : Set)
  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)
  shows i1 ∈ hom(C, a, p)
proof
  unfold IsCoproduct at coproduct
  have firstHom := IsProduct.first with coproduct
  have homs := hom.opposite at C, p, a
  rwa homs at firstHom

theorem IsCoproduct.second (C a b p i1 i2 : Set)
  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)
  shows i2 ∈ hom(C, b, p)
proof
  unfold IsCoproduct at coproduct
  have secondHom := IsProduct.second with coproduct
  have homs := hom.opposite at C, p, b
  rwa homs at secondHom

theorem IsCoproduct.universal (C a b p i1 i2 x f g : Set)
  requires category : Category(C)
  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)
  requires xInO : x ∈ obj(C)
  requires fHom : f ∈ hom(C, a, x)
  requires gHom : g ∈ hom(C, b, x)
  shows ∃ h ∈ hom(C, p, x), h ∘ i1 = f ∧ h ∘ i2 = g
proof
  have firstHom := IsCoproduct.first with coproduct
  have secondHom := IsCoproduct.second with coproduct
  unfold IsCoproduct at coproduct
  have homsF := hom.opposite at C, x, a
  have homsG := hom.opposite at C, x, b
  have homsH := hom.opposite at C, x, p
  rw ← homsF at fHom
  rw ← homsG at gHom
  have xInOpposite : x ∈ obj(opposite(C))
    rw opposite.obj
    exact xInO
  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=
    IsProduct.universal with coproduct, xInOpposite, fHom, gHom
  rw homsH at hHom
  rw opposite.comp at firstLaw
  rw opposite.comp at secondLaw
  have firstComposable := hom.composable with hHom, firstHom
  have secondComposable := hom.composable with hHom, secondHom
  have firstReversed : cod(C)(i1) = dom(C)(h) by cc
  have secondReversed : cod(C)(i2) = dom(C)(h) by cc
  have hInM := hom.in_morphisms with hHom
  have firstInM := hom.in_morphisms with firstHom
  have secondInM := hom.in_morphisms with secondHom
  have firstValue := oppositeComposition.apply with
    category, firstInM, hInM, firstReversed
  have secondValue := oppositeComposition.apply with
    category, secondInM, hInM, secondReversed
  refine ⟨h, hHom, ?_, ?_⟩
  . calc
      comp(C)(h, i1) =
          oppositeComposition(C)(i1, h) := by rw firstValue
      _ = f := firstLaw
  . calc
      comp(C)(h, i2) =
          oppositeComposition(C)(i2, h) := by rw secondValue
      _ = g := secondLaw

theorem IsCoproduct.swap (C a b p i1 i2 : Set)
  requires category : Category(C)
  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)
  shows IsCoproduct(C, b, a, p, i2, i1)
proof
  have opposite := Category.opposite with category
  unfold IsCoproduct at coproduct
  unfold IsCoproduct
  exact IsProduct.swap with opposite, coproduct

theorem IsCoproduct.isomorphic (C a b p i1 i2 q j1 j2 : Set)
  requires category : Category(C)
  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)
  requires other : IsCoproduct(C, a, b, q, j1, j2)
  shows Isomorphic(C, p, q)
proof
  have opposite := Category.opposite with category
  unfold IsCoproduct at coproduct
  unfold IsCoproduct at other
  have iso := IsProduct.isomorphic with opposite, coproduct, other
  have bridge := Isomorphic.opposite at C, q, p with
    category
  have back := bridge.backward with iso
  exact Isomorphic.symmetric with back

theorem IsCoproduct.initial (C a i : Set)
  requires category : Category(C)
  requires initial : Initial(C, i)
  requires aInO : a ∈ obj(C)
  shows IsCoproduct(C, a, i, a, id(C)(a),
    initialMorphism(C, i, a))
proof
  have opposite := Category.opposite with category
  have bridge := Initial.opposite at C, i with category
  have terminal := bridge.forward with initial
  have aInOpposite : a ∈ obj(opposite(C)) by opposite_projections
  unfold IsCoproduct
  have product := IsProduct.terminal with opposite, terminal, aInOpposite
  have fromInitial := initialMorphism.hom with initial, aInO
  have homs := hom.opposite at C, a, i
  rw ← homs at fromInitial
  have equal := terminalMorphism.eq with terminal, aInOpposite, fromInitial
  have identities := opposite.id at C
  rw [← equal, identities] at product
  exact product