Grace/Cumulus/Category/Product.g17

Open in Workbench Download source

Imports

Opposite

Declarations

Source

1-- Products and coproducts by their universal property2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Category.Product8import Opposite910-- (p, p1, p2) is a product of a and b: every pair f : x → a, g : x → b11-- factors uniquely through p.12predicate IsProduct (C a b p p1 p2 : Set) :=13  p ∈ Category.obj(C) ∧ p1 ∈ hom(C, p, a) ∧ p2 ∈ hom(C, p, b) ∧14  (∀ x ∈ obj(C), ∀ f ∈ hom(C, x, a), ∀ g ∈ hom(C, x, b),15    ∃ h ∈ hom(C, x, p), comp(C)(p1, h) = f ∧ comp(C)(p2, h) = g ∧16      (∀ k ∈ hom(C, x, p), comp(C)(p1, k) = f → comp(C)(p2, k) = g → k = h))1718notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis IsProduct(C, a, b, p, p1, p2) for C.mor1920-- A coproduct is a product in the opposite category.21predicate IsCoproduct (C a b p i1 i2 : Set) :=22  IsProduct(opposite(C), a, b, p, i1, i2)2324theorem IsProduct.object (C a b p p1 p2 : Set)25  requires product : IsProduct(C, a, b, p, p1, p2)26  shows p ∈ obj(C)27proof28  obtain ⟨pInO, rest⟩ := product29  exact pInO3031theorem IsProduct.first (C a b p p1 p2 : Set)32  requires product : IsProduct(C, a, b, p, p1, p2)33  shows p1 ∈ hom(C, p, a)34proof35  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product36  exact firstHom3738theorem IsProduct.second (C a b p p1 p2 : Set)39  requires product : IsProduct(C, a, b, p, p1, p2)40  shows p2 ∈ hom(C, p, b)41proof42  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product43  exact secondHom4445theorem IsProduct.universal (C a b p p1 p2 x f g : Set)46  requires product : IsProduct(C, a, b, p, p1, p2)47  requires xInO : x ∈ obj(C)48  requires fHom : f ∈ hom(C, x, a)49  requires gHom : g ∈ hom(C, x, b)50  shows ∃ h ∈ hom(C, x, p), p1 ∘ h = f ∧ p2 ∘ h = g ∧51    (∀ k ∈ hom(C, x, p), p1 ∘ k = f → p2 ∘ k = g → k = h)52proof53  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product54  exact universal with x, xInO, f, fHom, g, gHom5556-- Two morphisms into a product with the same components are equal.57theorem IsProduct.ext (C a b p p1 p2 x h k : Set)58  requires category : Category(C)59  requires product : IsProduct(C, a, b, p, p1, p2)60  requires xInO : x ∈ obj(C)61  requires hHom : h ∈ hom(C, x, p)62  requires kHom : k ∈ hom(C, x, p)63  requires sameFirst : p1 ∘ h = p1 ∘ k64  requires sameSecond : p2 ∘ h = p2 ∘ k65  shows h = k66proof67  have firstHom := IsProduct.first with product68  have secondHom := IsProduct.second with product69  have fHom := hom.comp with category, firstHom, hHom70  have gHom := hom.comp with category, secondHom, hHom71  obtain ⟨u, uHom, firstLaw, secondLaw, unique⟩ :=72    IsProduct.universal with product, xInO, fHom, gHom73  have hFirst : p1 ∘ h = p1 ∘ h by rfl74  have hSecond : p2 ∘ h = p2 ∘ h by rfl75  have hEqual := unique with h, hHom, hFirst, hSecond76  have kFirst : p1 ∘ k = p1 ∘ h by cc77  have kSecond : p2 ∘ k = p2 ∘ h by cc78  have kEqual := unique with k, kHom, kFirst, kSecond79  calc80    h = u := hEqual81    _ = k := by rw kEqual8283-- The pairing of f : x → a and g : x → b through the product.84defunique pairing (C a b p p1 p2 x f g : Set) (h ∈ hom(C, x, p)) :=85  comp(C)(p1, h) = f ∧ comp(C)(p2, h) = g86requires product : IsProduct(C, a, b, p, p1, p2)87requires xInO : x ∈ obj(C)88requires fHom : f ∈ hom(C, x, a)89requires gHom : g ∈ hom(C, x, b)90proof91  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=92    IsProduct.universal with product, xInO, fHom, gHom93  refine ⟨h, hHom, firstLaw, secondLaw⟩94uniqueness95  intros u hu first v hv second96  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=97    IsProduct.universal with product, xInO, fHom, gHom98  have uEqual := unique with u, hu, first.left, first.right99  have vEqual := unique with v, hv, second.left, second.right100  cc101102section ProductLaws103variable (C a b p p1 p2 : Set)104hypothesis category : Category(C)105hypothesis product : IsProduct(C, a, b, p, p1, p2)106107theorem pairing.hom (x f g : Set)108  requires xInO : x ∈ obj(C)109  requires fHom : f ∈ hom(C, x, a)110  requires gHom : g ∈ hom(C, x, b)111  shows pairing(C, a, b, p, p1, p2, x, f, g) ∈112    hom(C, x, p)113proof114  have selected := pairing.selected at C, a, b, p, p1, p2, x, f, g with115    product, xInO, fHom, gHom116  exact selected.left117118theorem pairing.first (x f g : Set)119  requires xInO : x ∈ obj(C)120  requires fHom : f ∈ hom(C, x, a)121  requires gHom : g ∈ hom(C, x, b)122  shows p1 ∘ pairing(C, a, b, p, p1, p2, x, f, g) = f123proof124  have selected := pairing.selected at C, a, b, p, p1, p2, x, f, g with125    product, xInO, fHom, gHom126  exact selected.right.left127128theorem pairing.second (x f g : Set)129  requires xInO : x ∈ obj(C)130  requires fHom : f ∈ hom(C, x, a)131  requires gHom : g ∈ hom(C, x, b)132  shows p2 ∘ pairing(C, a, b, p, p1, p2, x, f, g) = g133proof134  have selected := pairing.selected at C, a, b, p, p1, p2, x, f, g with135    product, xInO, fHom, gHom136  exact selected.right.right137138theorem pairing.eq (x f g k : Set)139  requires xInO : x ∈ obj(C)140  requires fHom : f ∈ hom(C, x, a)141  requires gHom : g ∈ hom(C, x, b)142  requires kHom : k ∈ hom(C, x, p)143  requires firstLaw : p1 ∘ k = f144  requires secondLaw : p2 ∘ k = g145  shows k = pairing(C, a, b, p, p1, p2, x, f, g)146proof147  have pairingHom := pairing.hom with category, product, xInO, fHom, gHom148  have pairingFirst := pairing.first with category, product, xInO, fHom, gHom149  have pairingSecond := pairing.second with category, product, xInO, fHom, gHom150  have sameFirst : p1 ∘ k = p1 ∘ pairing(C, a, b, p,151      p1, p2, x, f, g)152    calc153      p1 ∘ k = f := firstLaw154      _ = p1 ∘ pairing(C, a, b, p, p1, p2, x, f,155          g) := by rw pairingFirst156  have sameSecond : p2 ∘ k = p2 ∘ pairing(C, a, b, p,157      p1, p2, x, f, g)158    calc159      p2 ∘ k = g := secondLaw160      _ = p2 ∘ pairing(C, a, b, p, p1, p2, x, f,161          g) := by rw pairingSecond162  exact IsProduct.ext with163    category, product, xInO, kHom, pairingHom, sameFirst, sameSecond164165-- Pairing the projections gives the identity of the product.166theorem pairing.projections167  shows pairing(C, a, b, p, p1, p2, p, p1, p2) = id(C)(p)168proof169  have pInO := IsProduct.object with product170  have firstHom := IsProduct.first with product171  have secondHom := IsProduct.second with product172  have idHom := hom.id with category, pInO173  have firstLaw := Category.id_right_hom with category, firstHom174  have secondLaw := Category.id_right_hom with category, secondHom175  have equal := pairing.eq with category, product, pInO, firstHom, secondHom,176    idHom, firstLaw, secondLaw177  symm178  exact equal179180-- Pairing is natural in the source object.181theorem pairing.comp (x y f g u : Set)182  requires xInO : x ∈ obj(C)183  requires yInO : y ∈ obj(C)184  requires fHom : f ∈ hom(C, x, a)185  requires gHom : g ∈ hom(C, x, b)186  requires uHom : u ∈ hom(C, y, x)187  shows pairing(C, a, b, p, p1, p2, x, f, g) ∘ u =188    pairing(C, a, b, p, p1, p2, y, f ∘ u, g ∘ u)189proof190  have pairingHom := pairing.hom with category, product, xInO, fHom, gHom191  have pairingFirst := pairing.first with category, product, xInO, fHom, gHom192  have pairingSecond := pairing.second with category, product, xInO, fHom, gHom193  have firstHom := IsProduct.first with product194  have secondHom := IsProduct.second with product195  have fuHom := hom.comp with category, fHom, uHom196  have guHom := hom.comp with category, gHom, uHom197  have compositeHom := hom.comp with category, pairingHom, uHom198  have assocFirst := Category.assoc_hom with199    category, firstHom, pairingHom, uHom200  have assocSecond := Category.assoc_hom with201    category, secondHom, pairingHom, uHom202  have firstLaw : p1 ∘ (pairing(C, a, b, p, p1, p2, x,203      f, g) ∘ u) = f ∘ u204    calc205      p1 ∘ (pairing(C, a, b, p, p1, p2, x, f, g) ∘ u) =206          (p1 ∘ pairing(C, a, b, p, p1, p2, x, f,207              g)) ∘ u := by rw assocFirst208      _ = f ∘ u := by rw pairingFirst209  have secondLaw : p2 ∘ (pairing(C, a, b, p, p1, p2, x,210      f, g) ∘ u) = g ∘ u211    calc212      p2 ∘ (pairing(C, a, b, p, p1, p2, x, f, g) ∘ u) =213          (p2 ∘ pairing(C, a, b, p, p1, p2, x, f,214              g)) ∘ u := by rw assocSecond215      _ = g ∘ u := by rw pairingSecond216  exact pairing.eq with category, product, yInO, fuHom, guHom, compositeHom,217    firstLaw, secondLaw218219theorem IsProduct.swap220  shows IsProduct(C, b, a, p, p2, p1)221proof222  obtain ⟨pInO, firstHom, secondHom, universal⟩ := product223  unfold IsProduct224  refine ⟨pInO, secondHom, firstHom, ?_⟩225  intros x xInO g gHom f fHom226  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=227    universal with x, xInO, f, fHom, g, gHom228  refine ⟨h, hHom, secondLaw, firstLaw, ?_⟩229  intros k kHom kSecond kFirst230  exact unique with k, kHom, kFirst, kSecond231232-- Products of the same objects are isomorphic through the pairings.233theorem IsProduct.inverse_pair (q q1 q2 : Set)234  requires other : IsProduct(C, a, b, q, q1, q2)235  shows InversePair(C, pairing(C, a, b, q, q1, q2, p, p1, p2),236    pairing(C, a, b, p, p1, p2, q, q1, q2))237proof238  have pInO := IsProduct.object with product239  have qInO := IsProduct.object with other240  have firstP := IsProduct.first with product241  have secondP := IsProduct.second with product242  have firstQ := IsProduct.first with other243  have secondQ := IsProduct.second with other244  have hHom := pairing.hom with category, other, pInO, firstP, secondP245  have hFirst := pairing.first with category, other, pInO, firstP, secondP246  have hSecond := pairing.second with category, other, pInO, firstP, secondP247  have kHom := pairing.hom with category, product, qInO, firstQ, secondQ248  have kFirst := pairing.first with category, product, qInO, firstQ, secondQ249  have kSecond := pairing.second with category, product, qInO, firstQ, secondQ250  have khHom := hom.comp with category, kHom, hHom251  have hkHom := hom.comp with category, hHom, kHom252  have idP := hom.id with category, pInO253  have idQ := hom.id with category, qInO254  have assocPFirst := Category.assoc_hom with category, firstP, kHom, hHom255  have assocPSecond := Category.assoc_hom with category, secondP, kHom, hHom256  have assocQFirst := Category.assoc_hom with category, firstQ, hHom, kHom257  have assocQSecond := Category.assoc_hom with category, secondQ, hHom, kHom258  have unitPFirst := Category.id_right_hom with category, firstP259  have unitPSecond := Category.id_right_hom with category, secondP260  have unitQFirst := Category.id_right_hom with category, firstQ261  have unitQSecond := Category.id_right_hom with category, secondQ262  have khFirst : p1 ∘ (pairing(C, a, b, p, p1, p2, q,263      q1, q2) ∘264      pairing(C, a, b, q, q1, q2, p, p1,265          p2)) = p1 ∘ id(C)(p)266    calc267      p1 ∘ (pairing(C, a, b, p, p1, p2, q, q1, q2) ∘268          pairing(C, a, b, q, q1, q2, p, p1, p2)) =269        (p1 ∘ pairing(C, a, b, p, p1, p2, q, q1, q2)) ∘270          pairing(C, a, b, q, q1, q2, p, p1,271              p2) := by rw assocPFirst272      _ = q1 ∘ pairing(C, a, b, q, q1, q2, p, p1,273          p2) := by rw kFirst274      _ = p1 := hFirst275      _ = p1 ∘ id(C)(p) := by rw unitPFirst276  have khSecond : p2 ∘ (pairing(C, a, b, p, p1, p2, q,277      q1, q2) ∘278      pairing(C, a, b, q, q1, q2, p, p1,279          p2)) = p2 ∘ id(C)(p)280    calc281      p2 ∘ (pairing(C, a, b, p, p1, p2, q, q1, q2) ∘282          pairing(C, a, b, q, q1, q2, p, p1, p2)) =283        (p2 ∘ pairing(C, a, b, p, p1, p2, q, q1, q2)) ∘284          pairing(C, a, b, q, q1, q2, p, p1,285              p2) := by rw assocPSecond286      _ = q2 ∘ pairing(C, a, b, q, q1, q2, p, p1,287          p2) := by rw kSecond288      _ = p2 := hSecond289      _ = p2 ∘ id(C)(p) := by rw unitPSecond290  have khId := IsProduct.ext with291    category, product, pInO, khHom, idP, khFirst, khSecond292  have hkFirst : q1 ∘ (pairing(C, a, b, q, q1, q2, p,293      p1, p2) ∘294      pairing(C, a, b, p, p1, p2, q, q1,295          q2)) = q1 ∘ id(C)(q)296    calc297      q1 ∘ (pairing(C, a, b, q, q1, q2, p, p1, p2) ∘298          pairing(C, a, b, p, p1, p2, q, q1, q2)) =299        (q1 ∘ pairing(C, a, b, q, q1, q2, p, p1, p2)) ∘300          pairing(C, a, b, p, p1, p2, q, q1,301              q2) := by rw assocQFirst302      _ = p1 ∘ pairing(C, a, b, p, p1, p2, q, q1,303          q2) := by rw hFirst304      _ = q1 := kFirst305      _ = q1 ∘ id(C)(q) := by rw unitQFirst306  have hkSecond : q2 ∘ (pairing(C, a, b, q, q1, q2, p,307      p1, p2) ∘308      pairing(C, a, b, p, p1, p2, q, q1,309          q2)) = q2 ∘ id(C)(q)310    calc311      q2 ∘ (pairing(C, a, b, q, q1, q2, p, p1, p2) ∘312          pairing(C, a, b, p, p1, p2, q, q1, q2)) =313        (q2 ∘ pairing(C, a, b, q, q1, q2, p, p1, p2)) ∘314          pairing(C, a, b, p, p1, p2, q, q1,315              q2) := by rw assocQSecond316      _ = p2 ∘ pairing(C, a, b, p, p1, p2, q, q1,317          q2) := by rw hSecond318      _ = q2 := kSecond319      _ = q2 ∘ id(C)(q) := by rw unitQSecond320  have hkId := IsProduct.ext with321    category, other, qInO, hkHom, idQ, hkFirst, hkSecond322  have hInM := hom.in_morphisms with hHom323  have kInM := hom.in_morphisms with kHom324  have domH := hom.dom with hHom325  have codH := hom.cod with hHom326  have domK := hom.dom with kHom327  have codK := hom.cod with kHom328  unfold InversePair329  refine ⟨hInM, kInM, ?_, ?_, ?_, ?_⟩330  . cc331  . cc332  . calc333      pairing(C, a, b, p, p1, p2, q, q1, q2) ∘334          pairing(C, a, b, q, q1, q2, p, p1,335              p2) = id(C)(p) := khId336      _ = id(C)(dom(C)(pairing(C, a, b, q, q1, q2, p, p1,337          p2))) := by rw domH338  . calc339      pairing(C, a, b, q, q1, q2, p, p1, p2) ∘340          pairing(C, a, b, p, p1, p2, q, q1,341              q2) = id(C)(q) := hkId342      _ = id(C)(cod(C)(pairing(C, a, b, q, q1, q2, p, p1,343          p2))) := by rw codH344345theorem IsProduct.isomorphic (q q1 q2 : Set)346  requires other : IsProduct(C, a, b, q, q1, q2)347  shows Isomorphic(C, p, q)348proof349  have pInO := IsProduct.object with product350  have firstP := IsProduct.first with product351  have secondP := IsProduct.second with product352  have hHom := pairing.hom with category, other, pInO, firstP, secondP353  have pair := IsProduct.inverse_pair with category, product, other354  have iso := Isomorphism.of_pair with pair355  exact Isomorphic.of_hom with hHom, iso356357-- The product is commutative up to isomorphism.358theorem IsProduct.commutative (q q1 q2 : Set)359  requires other : IsProduct(C, b, a, q, q1, q2)360  shows Isomorphic(C, p, q)361proof362  have swapped := IsProduct.swap with category, product363  exact IsProduct.isomorphic with category, swapped, other364365-- A product transported along an isomorphism is a product.366theorem IsProduct.of_inverse_pair (q u v : Set)367  requires pair : InversePair(C, u, v)368  requires uHom : u ∈ hom(C, q, p)369  shows IsProduct(C, a, b, q, p1 ∘ u, p2 ∘ u)370proof371  have pInO := IsProduct.object with product372  have firstP := IsProduct.first with product373  have secondP := IsProduct.second with product374  have vHom := InversePair.in_hom with pair, uHom375  have uInM := hom.in_morphisms with uHom376  have qInO : q ∈ obj(C)377    have domIn := Category.dom_closed with category, uInM378    have domU := hom.dom with uHom379    rwa domU at domIn380  have firstHom := hom.comp with category, firstP, uHom381  have secondHom := hom.comp with category, secondP, uHom382  have vu := InversePair.left with pair383  have uv := InversePair.right with pair384  have domU := hom.dom with uHom385  have codU := hom.cod with uHom386  unfold IsProduct387  refine ⟨qInO, firstHom, secondHom, ?_⟩388  intros x xInO f fHom g gHom389  have hHom := pairing.hom with category, product, xInO, fHom, gHom390  have hFirst := pairing.first with category, product, xInO, fHom, gHom391  have hSecond := pairing.second with category, product, xInO, fHom, gHom392  have vhHom := hom.comp with category, vHom, hHom393  have uvhHom := hom.comp with category, uHom, vhHom394  have assocU := Category.assoc_hom with category, uHom, vHom, hHom395  have unitH := Category.id_left_hom with category, hHom396  have uvId : u ∘ v = id(C)(p)397    rwa codU at uv398  have vuId : v ∘ u = id(C)(q)399    rwa domU at vu400  have uvh : u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f,401      g)) =402      pairing(C, a, b, p, p1, p2, x, f, g)403    calc404      u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f, g)) =405          (u ∘ v) ∘ pairing(C, a, b, p, p1, p2, x, f,406              g) := by rw assocU407      _ = id(C)(p) ∘ pairing(C, a, b, p, p1, p2, x, f,408          g) := by rw uvId409      _ = pairing(C, a, b, p, p1, p2, x, f, g) := unitH410  have assocFirst := Category.assoc_hom with category, firstP, uHom, vhHom411  have assocSecond := Category.assoc_hom with category, secondP, uHom, vhHom412  refine ⟨v ∘ pairing(C, a, b, p, p1, p2, x, f, g),413    vhHom, ?_, ?_, ?_⟩414  . calc415      (p1 ∘ u) ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f,416          g)) =417          p1 ∘ (u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x,418              f, g))) :=419        assocFirst420      _ = p1 ∘ pairing(C, a, b, p, p1, p2, x, f,421          g) := by rw uvh422      _ = f := hFirst423  . calc424      (p2 ∘ u) ∘ (v ∘ pairing(C, a, b, p, p1, p2, x, f,425          g)) =426          p2 ∘ (u ∘ (v ∘ pairing(C, a, b, p, p1, p2, x,427              f, g))) :=428        assocSecond429      _ = p2 ∘ pairing(C, a, b, p, p1, p2, x, f,430          g) := by rw uvh431      _ = g := hSecond432  . intros k kHom kFirst kSecond433    have ukHom := hom.comp with category, uHom, kHom434    have assocKFirst := Category.assoc_hom with category, firstP, uHom, kHom435    have assocKSecond := Category.assoc_hom with category, secondP, uHom, kHom436    have ukFirst : p1 ∘ (u ∘ k) = f437      calc438        p1 ∘ (u ∘ k) = (p1 ∘ u) ∘ k := by rw assocKFirst439        _ = f := kFirst440    have ukSecond : p2 ∘ (u ∘ k) = g441      calc442        p2 ∘ (u ∘ k) = (p2 ∘ u) ∘ k := by rw assocKSecond443        _ = g := kSecond444    have ukEqual := pairing.eq with445      category, product, xInO, fHom, gHom, ukHom, ukFirst, ukSecond446    have assocVU := Category.assoc_hom with category, vHom, uHom, kHom447    have unitK := Category.id_left_hom with category, kHom448    calc449      k = id(C)(q) ∘ k := by rw unitK450      _ = (v ∘ u) ∘ k := by rw vuId451      _ = v ∘ (u ∘ k) := assocVU452      _ = v ∘ pairing(C, a, b, p, p1, p2, x, f,453          g) := by rw ukEqual454455end ProductLaws456457-- The diagonal of an object through a product of it with itself.458theorem IsProduct.diagonal_first (C a p p1 p2 : Set)459  requires category : Category(C)460  requires product : IsProduct(C, a, a, p, p1, p2)461  requires aInO : a ∈ obj(C)462  shows p1 ∘ pairing(C, a, a, p, p1, p2, a,463    id(C)(a), id(C)(a)) = id(C)(a)464proof465  have idHom := hom.id with category, aInO466  exact pairing.first with category, product, aInO, idHom, idHom467468theorem IsProduct.diagonal_second (C a p p1 p2 : Set)469  requires category : Category(C)470  requires product : IsProduct(C, a, a, p, p1, p2)471  requires aInO : a ∈ obj(C)472  shows p2 ∘ pairing(C, a, a, p, p1, p2, a,473    id(C)(a), id(C)(a)) = id(C)(a)474proof475  have idHom := hom.id with category, aInO476  exact pairing.second with category, product, aInO, idHom, idHom477478theorem IsProduct.diagonal_split_mono (C a p p1 p2 : Set)479  requires category : Category(C)480  requires product : IsProduct(C, a, a, p, p1, p2)481  requires aInO : a ∈ obj(C)482  shows SplitMonomorphism(C, pairing(C, a, a, p, p1, p2, a, id(C)(a), id(C)(a)))483proof484  have idHom := hom.id with category, aInO485  have diagonalHom := pairing.hom with category, product, aInO, idHom, idHom486  have firstLaw := IsProduct.diagonal_first with category, product, aInO487  have firstP := IsProduct.first with product488  have diagonalInM := hom.in_morphisms with diagonalHom489  have firstInM := hom.in_morphisms with firstP490  have domDiagonal := hom.dom with diagonalHom491  have codDiagonal := hom.cod with diagonalHom492  have domFirst := hom.dom with firstP493  have codFirst := hom.cod with firstP494  have retraction : Retraction(C, pairing(C, a, a, p, p1, p2, a, id(C)(a), id(C)(a)), p1)495    unfold Retraction496    refine ⟨diagonalInM, firstInM, ?_, ?_, ?_⟩497    . cc498    . cc499    . cc500  exact SplitMonomorphism.of_retraction with retraction501502-- A terminal object is a unit for the product.503theorem IsProduct.terminal (C a t : Set)504  requires category : Category(C)505  requires terminal : Terminal(C, t)506  requires aInO : a ∈ obj(C)507  shows IsProduct(C, a, t, a, id(C)(a),508    terminalMorphism(C, t, a))509proof510  have idHom := hom.id with category, aInO511  have toTerminal := terminalMorphism.hom with terminal, aInO512  unfold IsProduct513  refine ⟨aInO, idHom, toTerminal, ?_⟩514  intros x xInO f fHom g gHom515  have unitF := Category.id_left_hom with category, fHom516  have composite := terminalMorphism.comp with category, terminal, xInO, fHom517  have gEqual := terminalMorphism.eq with terminal, xInO, gHom518  refine ⟨f, fHom, unitF, ?_, ?_⟩519  . calc520      terminalMorphism(C, t, a) ∘ f =521          terminalMorphism(C, t, x) := composite522      _ = g := by rw gEqual523  . intros k kHom kFirst kSecond524    have unitK := Category.id_left_hom with category, kHom525    calc526      k = id(C)(a) ∘ k := by rw unitK527      _ = f := kFirst528529-- Coproducts, through the opposite category.530theorem IsCoproduct.object (C a b p i1 i2 : Set)531  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)532  shows p ∈ obj(C)533proof534  unfold IsCoproduct at coproduct535  have pIn := IsProduct.object with coproduct536  rwa opposite.obj at pIn537538theorem IsCoproduct.first (C a b p i1 i2 : Set)539  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)540  shows i1 ∈ hom(C, a, p)541proof542  unfold IsCoproduct at coproduct543  have firstHom := IsProduct.first with coproduct544  have homs := hom.opposite at C, p, a545  rwa homs at firstHom546547theorem IsCoproduct.second (C a b p i1 i2 : Set)548  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)549  shows i2 ∈ hom(C, b, p)550proof551  unfold IsCoproduct at coproduct552  have secondHom := IsProduct.second with coproduct553  have homs := hom.opposite at C, p, b554  rwa homs at secondHom555556theorem IsCoproduct.universal (C a b p i1 i2 x f g : Set)557  requires category : Category(C)558  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)559  requires xInO : x ∈ obj(C)560  requires fHom : f ∈ hom(C, a, x)561  requires gHom : g ∈ hom(C, b, x)562  shows ∃ h ∈ hom(C, p, x), h ∘ i1 = f ∧ h ∘ i2 = g563proof564  have firstHom := IsCoproduct.first with coproduct565  have secondHom := IsCoproduct.second with coproduct566  unfold IsCoproduct at coproduct567  have homsF := hom.opposite at C, x, a568  have homsG := hom.opposite at C, x, b569  have homsH := hom.opposite at C, x, p570  rw ← homsF at fHom571  rw ← homsG at gHom572  have xInOpposite : x ∈ obj(opposite(C))573    rw opposite.obj574    exact xInO575  obtain ⟨h, hHom, firstLaw, secondLaw, unique⟩ :=576    IsProduct.universal with coproduct, xInOpposite, fHom, gHom577  rw homsH at hHom578  rw opposite.comp at firstLaw579  rw opposite.comp at secondLaw580  have firstComposable := hom.composable with hHom, firstHom581  have secondComposable := hom.composable with hHom, secondHom582  have firstReversed : cod(C)(i1) = dom(C)(h) by cc583  have secondReversed : cod(C)(i2) = dom(C)(h) by cc584  have hInM := hom.in_morphisms with hHom585  have firstInM := hom.in_morphisms with firstHom586  have secondInM := hom.in_morphisms with secondHom587  have firstValue := oppositeComposition.apply with588    category, firstInM, hInM, firstReversed589  have secondValue := oppositeComposition.apply with590    category, secondInM, hInM, secondReversed591  refine ⟨h, hHom, ?_, ?_⟩592  . calc593      comp(C)(h, i1) =594          oppositeComposition(C)(i1, h) := by rw firstValue595      _ = f := firstLaw596  . calc597      comp(C)(h, i2) =598          oppositeComposition(C)(i2, h) := by rw secondValue599      _ = g := secondLaw600601theorem IsCoproduct.swap (C a b p i1 i2 : Set)602  requires category : Category(C)603  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)604  shows IsCoproduct(C, b, a, p, i2, i1)605proof606  have opposite := Category.opposite with category607  unfold IsCoproduct at coproduct608  unfold IsCoproduct609  exact IsProduct.swap with opposite, coproduct610611theorem IsCoproduct.isomorphic (C a b p i1 i2 q j1 j2 : Set)612  requires category : Category(C)613  requires coproduct : IsCoproduct(C, a, b, p, i1, i2)614  requires other : IsCoproduct(C, a, b, q, j1, j2)615  shows Isomorphic(C, p, q)616proof617  have opposite := Category.opposite with category618  unfold IsCoproduct at coproduct619  unfold IsCoproduct at other620  have iso := IsProduct.isomorphic with opposite, coproduct, other621  have bridge := Isomorphic.opposite at C, q, p with622    category623  have back := bridge.backward with iso624  exact Isomorphic.symmetric with back625626theorem IsCoproduct.initial (C a i : Set)627  requires category : Category(C)628  requires initial : Initial(C, i)629  requires aInO : a ∈ obj(C)630  shows IsCoproduct(C, a, i, a, id(C)(a),631    initialMorphism(C, i, a))632proof633  have opposite := Category.opposite with category634  have bridge := Initial.opposite at C, i with category635  have terminal := bridge.forward with initial636  have aInOpposite : a ∈ obj(opposite(C)) by opposite_projections637  unfold IsCoproduct638  have product := IsProduct.terminal with opposite, terminal, aInOpposite639  have fromInitial := initialMorphism.hom with initial, aInO640  have homs := hom.opposite at C, a, i641  rw ← homs at fromInitial642  have equal := terminalMorphism.eq with terminal, aInOpposite, fromInitial643  have identities := opposite.id at C644  rw [← equal, identities] at product645  exact product646