A Lean Companion to Conceptual Mathematics

Session 23: More on universal mapping propertiesπŸ”—

1. A category of pairs of mapsπŸ”—

Exercise 1 (p. 256)

Formulate and prove in two ways the theorem of uniqueness of the product of two objects B_1 and B_2 of the category π’ž. (One way is the direct proof and the other way is to define the category π’ž_{B_{1}B_{2}}, to prove that it is a category, to prove that its terminal object is the same as a product of B_1 and B_2 in π’ž, and to appeal to the theorem on uniqueness of terminal objects.)

Solution: Exercise 1

The direct proof was already given in Article IV. In Exercise 12 of Article IV, we proved uniqueness of the product in the case of two objects, and on p. 221 we proved uniqueness in the case of an arbitrary family of objects.

We now give the second proof, starting with the definition of the category π’ž_{B_{1}B_{2}}.

variable {π’ž : Type u} [Category.{v, u} π’ž] structure PairOfMaps (B₁ Bβ‚‚ : π’ž) where carrier : π’ž p₁ : carrier ⟢ B₁ pβ‚‚ : carrier ⟢ Bβ‚‚

We show that π’ž_{B_{1}B_{2}} is a valid category.

instance {B₁ Bβ‚‚ : π’ž} : Category (PairOfMaps B₁ Bβ‚‚) where Hom X Y := { f : X.carrier ⟢ Y.carrier // Y.p₁ ⊚ f = X.p₁ ∧ Y.pβ‚‚ ⊚ f = X.pβ‚‚ } id X := βŸ¨πŸ™ X.carrier, π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX:PairOfMaps B₁ Bβ‚‚βŠ’ X.p₁ ⊚ πŸ™ X.carrier = X.p₁ ∧ X.pβ‚‚ ⊚ πŸ™ X.carrier = X.pβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX:PairOfMaps B₁ Bβ‚‚βŠ’ X.p₁ ⊚ πŸ™ X.carrier = X.pβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX:PairOfMaps B₁ Bβ‚‚βŠ’ X.pβ‚‚ ⊚ πŸ™ X.carrier = X.pβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX:PairOfMaps B₁ Bβ‚‚βŠ’ X.p₁ ⊚ πŸ™ X.carrier = X.pβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX:PairOfMaps B₁ Bβ‚‚βŠ’ X.pβ‚‚ ⊚ πŸ™ X.carrier = X.pβ‚‚ All goals completed! πŸ™βŸ© comp f g := ⟨g.val ⊚ f.val, π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX✝:PairOfMaps B₁ Bβ‚‚Y✝:PairOfMaps B₁ Bβ‚‚Z✝:PairOfMaps B₁ Bβ‚‚f:{ f // Y✝.p₁ ⊚ f = X✝.p₁ ∧ Y✝.pβ‚‚ ⊚ f = X✝.pβ‚‚ }g:{ f // Z✝.p₁ ⊚ f = Y✝.p₁ ∧ Z✝.pβ‚‚ ⊚ f = Y✝.pβ‚‚ }⊒ Z✝.p₁ ⊚ ↑g ⊚ ↑f = X✝.p₁ ∧ Z✝.pβ‚‚ ⊚ ↑g ⊚ ↑f = X✝.pβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX✝:PairOfMaps B₁ Bβ‚‚Y✝:PairOfMaps B₁ Bβ‚‚Z✝:PairOfMaps B₁ Bβ‚‚f:{ f // Y✝.p₁ ⊚ f = X✝.p₁ ∧ Y✝.pβ‚‚ ⊚ f = X✝.pβ‚‚ }g:{ f // Z✝.p₁ ⊚ f = Y✝.p₁ ∧ Z✝.pβ‚‚ ⊚ f = Y✝.pβ‚‚ }⊒ Z✝.p₁ ⊚ ↑g ⊚ ↑f = X✝.pβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX✝:PairOfMaps B₁ Bβ‚‚Y✝:PairOfMaps B₁ Bβ‚‚Z✝:PairOfMaps B₁ Bβ‚‚f:{ f // Y✝.p₁ ⊚ f = X✝.p₁ ∧ Y✝.pβ‚‚ ⊚ f = X✝.pβ‚‚ }g:{ f // Z✝.p₁ ⊚ f = Y✝.p₁ ∧ Z✝.pβ‚‚ ⊚ f = Y✝.pβ‚‚ }⊒ Z✝.pβ‚‚ ⊚ ↑g ⊚ ↑f = X✝.pβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX✝:PairOfMaps B₁ Bβ‚‚Y✝:PairOfMaps B₁ Bβ‚‚Z✝:PairOfMaps B₁ Bβ‚‚f:{ f // Y✝.p₁ ⊚ f = X✝.p₁ ∧ Y✝.pβ‚‚ ⊚ f = X✝.pβ‚‚ }g:{ f // Z✝.p₁ ⊚ f = Y✝.p₁ ∧ Z✝.pβ‚‚ ⊚ f = Y✝.pβ‚‚ }⊒ Z✝.p₁ ⊚ ↑g ⊚ ↑f = X✝.p₁ All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žX✝:PairOfMaps B₁ Bβ‚‚Y✝:PairOfMaps B₁ Bβ‚‚Z✝:PairOfMaps B₁ Bβ‚‚f:{ f // Y✝.p₁ ⊚ f = X✝.p₁ ∧ Y✝.pβ‚‚ ⊚ f = X✝.pβ‚‚ }g:{ f // Z✝.p₁ ⊚ f = Y✝.p₁ ∧ Z✝.pβ‚‚ ⊚ f = Y✝.pβ‚‚ }⊒ Z✝.pβ‚‚ ⊚ ↑g ⊚ ↑f = X✝.pβ‚‚ All goals completed! πŸ™βŸ©

Next we show that the terminal object of π’ž_{B_{1}B_{2}} is the same as a product of B_1 and B_2 in π’ž.

example {B₁ Bβ‚‚ : π’ž} {T : PairOfMaps B₁ Bβ‚‚} (hT : IsTerminal T) : βˆ€ (X : π’ž) (f₁ : X ⟢ B₁) (fβ‚‚ : X ⟢ Bβ‚‚), βˆƒ! f : X ⟢ T.carrier, T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚ := π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal T⊒ βˆ€ (X : π’ž) (f₁ : X ⟢ B₁) (fβ‚‚ : X ⟢ Bβ‚‚), βˆƒ! f, T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚ intro X π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ Bβ‚βŠ’ βˆ€ (fβ‚‚ : X ⟢ Bβ‚‚), βˆƒ! f, T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚βŠ’ βˆƒ! f, T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }⊒ βˆƒ! f, T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XP⊒ βˆƒ! f, T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XP⊒ (fun f ↦ T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚) ↑fP ∧ βˆ€ (y : X ⟢ T.carrier), (fun f ↦ T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚) y β†’ y = ↑fP π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XP⊒ (fun f ↦ T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚) ↑fPπ’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XP⊒ βˆ€ (y : X ⟢ T.carrier), (fun f ↦ T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚) y β†’ y = ↑fP π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XP⊒ (fun f ↦ T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚) ↑fP All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XP⊒ βˆ€ (y : X ⟢ T.carrier), (fun f ↦ T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚) y β†’ y = ↑fP intro f π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XPf:X ⟢ T.carrierhf:T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚βŠ’ f = ↑fP π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT:PairOfMaps B₁ Bβ‚‚hT:IsTerminal TX:π’žf₁:X ⟢ B₁fβ‚‚:X ⟢ Bβ‚‚XP:PairOfMaps B₁ Bβ‚‚ := { carrier := X, p₁ := f₁, pβ‚‚ := fβ‚‚ }fP:XP ⟢ T := hT.from XPf:X ⟢ T.carrierhf:T.p₁ ⊚ f = f₁ ∧ T.pβ‚‚ ⊚ f = fβ‚‚fP':XP ⟢ T := ⟨f, hf⟩⊒ f = ↑fP All goals completed! πŸ™

Finally we appeal to the theorem on uniqueness of terminal objects.

example {B₁ Bβ‚‚ : π’ž} {T₁ Tβ‚‚ : PairOfMaps B₁ Bβ‚‚} (hT₁ : IsTerminal T₁) (hTβ‚‚ : IsTerminal Tβ‚‚) : Nonempty (T₁.carrier β‰… Tβ‚‚.carrier) := π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT₁:PairOfMaps B₁ Bβ‚‚Tβ‚‚:PairOfMaps B₁ Bβ‚‚hT₁:IsTerminal T₁hTβ‚‚:IsTerminal Tβ‚‚βŠ’ Nonempty (T₁.carrier β‰… Tβ‚‚.carrier) π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT₁:PairOfMaps B₁ Bβ‚‚Tβ‚‚:PairOfMaps B₁ Bβ‚‚hT₁:IsTerminal T₁hTβ‚‚:IsTerminal Tβ‚‚t:T₁ ⟢ Tβ‚‚ht_iso:IsIso tright✝:βˆ€ (y : T₁ ⟢ Tβ‚‚), (fun s ↦ IsIso s) y β†’ y = t⊒ Nonempty (T₁.carrier β‰… Tβ‚‚.carrier) π’ž:Type uinst✝:Category.{v, u} π’žB₁:π’žBβ‚‚:π’žT₁:PairOfMaps B₁ Bβ‚‚Tβ‚‚:PairOfMaps B₁ Bβ‚‚hT₁:IsTerminal T₁hTβ‚‚:IsTerminal Tβ‚‚t:T₁ ⟢ Tβ‚‚ht_iso:IsIso tright✝:βˆ€ (y : T₁ ⟢ Tβ‚‚), (fun s ↦ IsIso s) y β†’ y = t⊒ T₁.carrier β‰… Tβ‚‚.carrier All goals completed! πŸ™

2. How to calculate productsπŸ”—

Definition: ⟨f₁, fβ‚‚βŸ© (p. 257)

For any pair of maps {A \xrightarrow{f_1} B_1}, {A \xrightarrow{f_2} B_2}, {\langle f_1, f_2 \rangle} is the unique map {A \rightarrow B_1 \times B_2} that satisfies the equations {p_1 \langle f_1, f_2 \rangle = f_1} and {p_2 \langle f_1, f_2 \rangle = f_2}.

The relevant mathlib definition here is prod.lift, which we print below for reference.

@[reducible] def CategoryTheory.Limits.prod.lift.{v, u} : {C : Type u} β†’ [inst : Category.{v, u} C] β†’ {W X Y : C} β†’ [inst_1 : HasBinaryProduct X Y] β†’ (W ⟢ X) β†’ (W ⟢ Y) β†’ (W ⟢ X β¨― Y) := fun {C} [Category.{v, u} C] {W X Y} [HasBinaryProduct X Y] f g ↦ limit.lift (pair X Y) (BinaryFan.mk f g)#print prod.lift 
@[reducible] def CategoryTheory.Limits.prod.lift.{v, u} : {C : Type u} β†’
  [inst : Category.{v, u} C] β†’ {W X Y : C} β†’ [inst_1 : HasBinaryProduct X Y] β†’ (W ⟢ X) β†’ (W ⟢ Y) β†’ (W ⟢ X β¨― Y) :=
fun {C} [Category.{v, u} C] {W X Y} [HasBinaryProduct X Y] f g ↦ limit.lift (pair X Y) (BinaryFan.mk f g)
Exercise 2 (p. 260)

Try to create the definition of 'sum' of two objects, in terms of a universal mapping property 'dual' to that of product, by reversing all maps in the definition of product. Then verify that in the category of sets and in the category of graphs, this property actually is satisfied by the intuitive idea of sum: 'Put together with no overlap and no interaction'.

Solution: Exercise 2

We start by defining a CategorySum structure to represent the sum of two objects in an arbitrary category as the dual of the product.

variable {π’ž : Type u} [Category.{v, u} π’ž] structure CategorySum (B₁ Bβ‚‚ : π’ž) where carrier : π’ž j₁ : B₁ ⟢ carrier jβ‚‚ : Bβ‚‚ ⟢ carrier h_univ : βˆ€ (Y : π’ž) (g₁ : B₁ ⟢ Y) (gβ‚‚ : Bβ‚‚ ⟢ Y), βˆƒ! g : carrier ⟢ Y, g ⊚ j₁ = g₁ ∧ g ⊚ jβ‚‚ = gβ‚‚

In the category of sets (types), the intuitive idea of sum as the disjoint union of two sets (types) is given by the Sum type, so we show that Sum satisfies the universal mapping property of our CategorySum structure.

example {B₁ Bβ‚‚ : Type} : CategorySum B₁ Bβ‚‚ := { carrier := Sum B₁ Bβ‚‚ j₁ := Sum.inl jβ‚‚ := Sum.inr h_univ Y g₁ gβ‚‚:= π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ βˆƒ! g, g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ ((fun g ↦ g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚) fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚) ∧ βˆ€ (y : B₁ βŠ• Bβ‚‚ ⟢ Y), (fun g ↦ g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚) y β†’ y = fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun g ↦ g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚) fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ βˆ€ (y : B₁ βŠ• Bβ‚‚ ⟢ Y), (fun g ↦ g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚) y β†’ y = fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun g ↦ g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚) fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚) ⊚ Sum.inl = gβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚) ⊚ Sum.inr = gβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚) ⊚ Sum.inl = gβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚) ⊚ Sum.inr = gβ‚‚ All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ βˆ€ (y : B₁ βŠ• Bβ‚‚ ⟢ Y), (fun g ↦ g ⊚ Sum.inl = g₁ ∧ g ⊚ Sum.inr = gβ‚‚) y β†’ y = fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ intro g π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:B₁ βŠ• Bβ‚‚ ⟢ Yhg₁:g ⊚ Sum.inl = g₁hgβ‚‚:g ⊚ Sum.inr = gβ‚‚βŠ’ g = fun x ↦ match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:B₁ βŠ• Bβ‚‚ ⟢ Yhg₁:g ⊚ Sum.inl = g₁hgβ‚‚:g ⊚ Sum.inr = gβ‚‚x:B₁ βŠ• Bβ‚‚βŠ’ g x = match x with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ cases x with π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:B₁ βŠ• Bβ‚‚ ⟢ Yhg₁:g ⊚ Sum.inl = g₁hgβ‚‚:g ⊚ Sum.inr = gβ‚‚b₁:Bβ‚βŠ’ g (Sum.inl b₁) = match Sum.inl b₁ with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:TypeBβ‚‚:TypeY:Typeg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:B₁ βŠ• Bβ‚‚ ⟢ Yhg₁:g ⊚ Sum.inl = g₁hgβ‚‚:g ⊚ Sum.inr = gβ‚‚bβ‚‚:Bβ‚‚βŠ’ g (Sum.inr bβ‚‚) = match Sum.inr bβ‚‚ with | Sum.inl b₁ => g₁ b₁ | Sum.inr bβ‚‚ => gβ‚‚ bβ‚‚ All goals completed! πŸ™ }

In the category of graphs, the intuitive idea of sum can be formalised as follows:

def IGSum (B₁ Bβ‚‚ : IrreflexiveGraph) : IrreflexiveGraph := { carrierA := Sum B₁.carrierA Bβ‚‚.carrierA carrierD := Sum B₁.carrierD Bβ‚‚.carrierD toSrc := fun | Sum.inl a₁ => Sum.inl (B₁.toSrc a₁) | Sum.inr aβ‚‚ => Sum.inr (Bβ‚‚.toSrc aβ‚‚) toTgt := fun | Sum.inl a₁ => Sum.inl (B₁.toTgt a₁) | Sum.inr aβ‚‚ => Sum.inr (Bβ‚‚.toTgt aβ‚‚) } def IGSum.inl {B₁ Bβ‚‚ : IrreflexiveGraph} : B₁ ⟢ IGSum B₁ Bβ‚‚ := ⟨ (Sum.inl, Sum.inl), π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inl, Sum.inl).2 ⊚ B₁.toSrc = (IGSum B₁ Bβ‚‚).toSrc ⊚ (Sum.inl, Sum.inl).1 ∧ (Sum.inl, Sum.inl).2 ⊚ B₁.toTgt = (IGSum B₁ Bβ‚‚).toTgt ⊚ (Sum.inl, Sum.inl).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inl, Sum.inl).2 ⊚ B₁.toSrc = (IGSum B₁ Bβ‚‚).toSrc ⊚ (Sum.inl, Sum.inl).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inl, Sum.inl).2 ⊚ B₁.toTgt = (IGSum B₁ Bβ‚‚).toTgt ⊚ (Sum.inl, Sum.inl).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inl, Sum.inl).2 ⊚ B₁.toSrc = (IGSum B₁ Bβ‚‚).toSrc ⊚ (Sum.inl, Sum.inl).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inl, Sum.inl).2 ⊚ B₁.toTgt = (IGSum B₁ Bβ‚‚).toTgt ⊚ (Sum.inl, Sum.inl).1 All goals completed! πŸ™ ⟩ def IGSum.inr {B₁ Bβ‚‚ : IrreflexiveGraph} : Bβ‚‚ ⟢ IGSum B₁ Bβ‚‚ := ⟨ (Sum.inr, Sum.inr), π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inr, Sum.inr).2 ⊚ Bβ‚‚.toSrc = (IGSum B₁ Bβ‚‚).toSrc ⊚ (Sum.inr, Sum.inr).1 ∧ (Sum.inr, Sum.inr).2 ⊚ Bβ‚‚.toTgt = (IGSum B₁ Bβ‚‚).toTgt ⊚ (Sum.inr, Sum.inr).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inr, Sum.inr).2 ⊚ Bβ‚‚.toSrc = (IGSum B₁ Bβ‚‚).toSrc ⊚ (Sum.inr, Sum.inr).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inr, Sum.inr).2 ⊚ Bβ‚‚.toTgt = (IGSum B₁ Bβ‚‚).toTgt ⊚ (Sum.inr, Sum.inr).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inr, Sum.inr).2 ⊚ Bβ‚‚.toSrc = (IGSum B₁ Bβ‚‚).toSrc ⊚ (Sum.inr, Sum.inr).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraph⊒ (Sum.inr, Sum.inr).2 ⊚ Bβ‚‚.toTgt = (IGSum B₁ Bβ‚‚).toTgt ⊚ (Sum.inr, Sum.inr).1 All goals completed! πŸ™ ⟩

We then show that IGSum satisfies the universal mapping property of our CategorySum structure.

example {B₁ Bβ‚‚ : IrreflexiveGraph} : CategorySum B₁ Bβ‚‚ := { carrier := IGSum B₁ Bβ‚‚ j₁ := IGSum.inl jβ‚‚ := IGSum.inr h_univ Y g₁ gβ‚‚:= π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ βˆƒ! g, g ⊚ IGSum.inl = g₁ ∧ g ⊚ IGSum.inr = gβ‚‚ use ⟨ (fun | Sum.inl a₁ => g₁.val.1 a₁ | Sum.inr aβ‚‚ => gβ‚‚.val.1 aβ‚‚, fun | Sum.inl d₁ => g₁.val.2 d₁ | Sum.inr dβ‚‚ => gβ‚‚.val.2 dβ‚‚), π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toSrc = Y.toSrc ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1 ∧ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt = Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toSrc = Y.toSrc ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt = Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toSrc = Y.toSrc ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt = Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yx:(IGSum B₁ Bβ‚‚).carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt) x = (Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) x π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yx:(IGSum B₁ Bβ‚‚).carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toSrc) x = (Y.toSrc ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) x cases x with π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Ya₁:B₁.carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toSrc) (Sum.inl a₁) = (Y.toSrc ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) (Sum.inl a₁) All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yaβ‚‚:Bβ‚‚.carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toSrc) (Sum.inr aβ‚‚) = (Y.toSrc ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) (Sum.inr aβ‚‚) All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yx:(IGSum B₁ Bβ‚‚).carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt) x = (Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) x cases x with π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Ya₁:B₁.carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt) (Sum.inl a₁) = (Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) (Sum.inl a₁) All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yaβ‚‚:Bβ‚‚.carrierA⊒ ((fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).2 ⊚ (IGSum B₁ Bβ‚‚).toTgt) (Sum.inr aβ‚‚) = (Y.toTgt ⊚ (fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚).1) (Sum.inr aβ‚‚) All goals completed! πŸ™ ⟩ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun g ↦ g ⊚ IGSum.inl = g₁ ∧ g ⊚ IGSum.inr = gβ‚‚) ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ βˆ€ (y : IGSum B₁ Bβ‚‚ ⟢ Y), (fun g ↦ g ⊚ IGSum.inl = g₁ ∧ g ⊚ IGSum.inr = gβ‚‚) y β†’ y = ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ (fun g ↦ g ⊚ IGSum.inl = g₁ ∧ g ⊚ IGSum.inr = gβ‚‚) ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© ⊚ IGSum.inl = gβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© ⊚ IGSum.inr = gβ‚‚ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© ⊚ IGSum.inl = gβ‚π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© ⊚ IGSum.inr = gβ‚‚ All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Y⊒ βˆ€ (y : IGSum B₁ Bβ‚‚ ⟢ Y), (fun g ↦ g ⊚ IGSum.inl = g₁ ∧ g ⊚ IGSum.inr = gβ‚‚) y β†’ y = ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© intro g π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚βŠ’ g = ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2⊒ g = ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2⊒ g = ⟨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ© π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2⊒ (↑g).1 = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2⊒ (↑g).2 = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).2 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2⊒ (↑g).1 = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).1π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2⊒ (↑g).2 = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).2 π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2x:(IGSum B₁ Bβ‚‚).carrierD⊒ (↑g).2 x = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).2 x π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2x:(IGSum B₁ Bβ‚‚).carrierA⊒ (↑g).1 x = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).1 x cases x with π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2a₁:B₁.carrierA⊒ (↑g).1 (Sum.inl a₁) = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).1 (Sum.inl a₁) All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2aβ‚‚:Bβ‚‚.carrierA⊒ (↑g).1 (Sum.inr aβ‚‚) = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).1 (Sum.inr aβ‚‚) All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2x:(IGSum B₁ Bβ‚‚).carrierD⊒ (↑g).2 x = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).2 x cases x with π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2d₁:B₁.carrierD⊒ (↑g).2 (Sum.inl d₁) = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).2 (Sum.inl d₁) All goals completed! πŸ™ π’ž:Type uinst✝:Category.{v, u} π’žB₁:IrreflexiveGraphBβ‚‚:IrreflexiveGraphY:IrreflexiveGraphg₁:B₁ ⟢ Ygβ‚‚:Bβ‚‚ ⟢ Yg:IGSum B₁ Bβ‚‚ ⟢ Yhg₁:g ⊚ IGSum.inl = g₁hgβ‚‚:g ⊚ IGSum.inr = gβ‚‚hg₁1:(↑(g ⊚ IGSum.inl)).1 = (↑g₁).1hg₁2:(↑(g ⊚ IGSum.inl)).2 = (↑g₁).2hgβ‚‚1:(↑(g ⊚ IGSum.inr)).1 = (↑gβ‚‚).1hgβ‚‚2:(↑(g ⊚ IGSum.inr)).2 = (↑gβ‚‚).2dβ‚‚:Bβ‚‚.carrierD⊒ (↑g).2 (Sum.inr dβ‚‚) = (β†‘βŸ¨(fun x ↦ match x with | Sum.inl a₁ => (↑g₁).1 a₁ | Sum.inr aβ‚‚ => (↑gβ‚‚).1 aβ‚‚, fun x ↦ match x with | Sum.inl d₁ => (↑g₁).2 d₁ | Sum.inr dβ‚‚ => (↑gβ‚‚).2 dβ‚‚), β‹―βŸ©).2 (Sum.inr dβ‚‚) All goals completed! πŸ™ }