A Lean Companion to Conceptual Mathematics

Session 24: Uniqueness of products and definition of sum🔗

2. The uniqueness theorem for products🔗

Theorem (uniqueness of products) (p. 263)

Suppose that both of B_1 \xleftarrow{p_1} P \xrightarrow{p_2} B_2 \quad\text{and}\quad {B_1 \xleftarrow{q_1} Q \xrightarrow{q_2} B_2} are product projection pairs (i.e. the ps as well as the qs satisfy the universal mapping property). Then there is exactly one map {P \xrightarrow{f} Q} for which q_1 f = p_1 \quad\text{and}\quad q_2 f = p_2 This map f is in fact an isomorphism.

See the previous formalisations provided in Exercise 12 of Article IV and on pp. 221 & 239.

3. Sum of two objects in a category🔗

Definition: Sum of two objects (p. 265–266)

A sum of two objects B_1, B_2 is an object S and a pair of maps B_1 \xrightarrow{j_1} S \xleftarrow{j_2} B_2 having the following universal mapping property: For any two maps B_1 \xrightarrow{f_1} X \xleftarrow{f_2} B_2 among all the maps {X \xleftarrow{f} S} there is exactly one that satisfies both f_1 = f j_1 \quad\text{and}\quad f_2 = f j_2 ...

See the earlier formalisation of sum on p. 222.

Exercise 1 (p. 266)

Formulate and prove the theorem of uniqueness of sums.

Solution: Exercise 1

Let S and T be two sums of B_1 and B_2, with injection maps {B_1 \xrightarrow{j_1} S \xleftarrow{j_2} B_2} and {B_1 \xrightarrow{k_1} T \xleftarrow{k_2} B_2}.

We first provide a proof of the theorem using the mathlib API for (binary) coproducts. For symmetry with our earlier proof of the uniqueness of products, we include the additional result that the unique map between any two sums of the same two objects in a category is an isomorphism.

From the formalisation in mathlib, we obtain the following mappings between the notation for this exercise given above and the data used in our proof:

S = coconeS.pt; j₁ = coconeS.ι.app ⟨WalkingPair.left⟩; j₂ = coconeS.ι.app ⟨WalkingPair.right⟩

T = coconeT.pt; k₁ = coconeT.ι.app ⟨WalkingPair.left⟩; k₂ = coconeT.ι.app ⟨WalkingPair.right⟩

theorem uniqueness_of_sums {𝒞 : Type u} [Category.{v, u} 𝒞] (B₁ B₂ : 𝒞) (coconeS coconeT : BinaryCofan B₁ B₂) (sumS : IsColimit coconeS) (sumT : IsColimit coconeT) : ∃! f : coconeS.pt coconeT.pt, (coconeT.ι.app WalkingPair.left = f coconeS.ι.app WalkingPair.left coconeT.ι.app WalkingPair.right = f coconeS.ι.app WalkingPair.right) IsIso f := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT∃! f, (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT(fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) (sumS.desc coconeT) (y : coconeS.pt coconeT.pt), (fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) y y = sumS.desc coconeT -- f 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.left } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.left }𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.right } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.right }𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTIsIso (sumS.desc coconeT)𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT (y : coconeS.pt coconeT.pt), (fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) y y = sumS.desc coconeT 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.left } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.left } -- Show that k₁ = f ⊚ j₁ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.right } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.right } -- Show that k₂ = f ⊚ j₂ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTIsIso (sumS.desc coconeT) -- Show that f is an isomorphism 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT inv, inv sumS.desc coconeT = 𝟙 coconeS.pt sumS.desc coconeT inv = 𝟙 coconeT.pt 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumT.desc coconeS sumS.desc coconeT = 𝟙 coconeS.pt sumS.desc coconeT sumT.desc coconeS = 𝟙 coconeT.pt -- f⁻¹ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumT.desc coconeS sumS.desc coconeT = 𝟙 coconeS.pt𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumS.desc coconeT sumT.desc coconeS = 𝟙 coconeT.pt 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumT.desc coconeS sumS.desc coconeT = 𝟙 coconeS.pt -- f⁻¹ ⊚ f = 𝟙 S 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumT.desc coconeS sumS.desc coconeT = sumS.desc coconeS 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT (j : Discrete WalkingPair), (sumT.desc coconeS sumS.desc coconeT) coconeS.ι.app j = coconeS.ι.app j 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTj:Discrete WalkingPair(sumT.desc coconeS sumS.desc coconeT) coconeS.ι.app j = coconeS.ι.app j erw [ Category.assoc, sumS.fac, sumT.facAll goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumS.desc coconeT sumT.desc coconeS = 𝟙 coconeT.pt -- f ⊚ f⁻¹ = 𝟙 T 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTsumS.desc coconeT sumT.desc coconeS = sumT.desc coconeT 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT (j : Discrete WalkingPair), (sumS.desc coconeT sumT.desc coconeS) coconeT.ι.app j = coconeT.ι.app j 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTj:Discrete WalkingPair(sumS.desc coconeT sumT.desc coconeS) coconeT.ι.app j = coconeT.ι.app j erw [ Category.assoc, sumT.fac, sumS.facAll goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT (y : coconeS.pt coconeT.pt), (fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) y y = sumS.desc coconeT -- Show that f is unique intro f 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff = sumS.desc coconeT 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso f (j : Discrete WalkingPair), f coconeS.ι.app j = coconeT.ι.app j 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso fj:Discrete WalkingPairf coconeS.ι.app j = coconeT.ι.app j 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.left } = coconeT.ι.app { as := WalkingPair.left }𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.right } = coconeT.ι.app { as := WalkingPair.right } 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.left } = coconeT.ι.app { as := WalkingPair.left } All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.right } = coconeT.ι.app { as := WalkingPair.right } All goals completed! 🐙

We can use the mathlib lemma IsColimit.nonempty_isColimit_iff_isIso_desc to do much of the heavy lifting here. A revised version of the proof using this lemma is given below.

example {𝒞 : Type u} [Category.{v, u} 𝒞] (B₁ B₂ : 𝒞) (coconeS coconeT : BinaryCofan B₁ B₂) (sumS : IsColimit coconeS) (sumT : IsColimit coconeT) : ∃! f : coconeS.pt coconeT.pt, (coconeT.ι.app WalkingPair.left = f coconeS.ι.app WalkingPair.left coconeT.ι.app WalkingPair.right = f coconeS.ι.app WalkingPair.right) IsIso f := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT∃! f, (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT(fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) (sumS.desc coconeT) (y : coconeS.pt coconeT.pt), (fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) y y = sumS.desc coconeT 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.left } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.left }𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.right } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.right }𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTIsIso (sumS.desc coconeT)𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT (y : coconeS.pt coconeT.pt), (fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) y y = sumS.desc coconeT 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.left } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.left } -- Show that k₁ = f ⊚ j₁ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTcoconeT.ι.app { as := WalkingPair.right } = sumS.desc coconeT coconeS.ι.app { as := WalkingPair.right } -- Show that k₂ = f ⊚ j₂ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTIsIso (sumS.desc coconeT) -- Show that f is an isomorphism All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeT (y : coconeS.pt coconeT.pt), (fun f (coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left } coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }) IsIso f) y y = sumS.desc coconeT -- Show that f is unique intro f 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff = sumS.desc coconeT 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso f (j : Discrete WalkingPair), f coconeS.ι.app j = coconeT.ι.app j 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso fj:Discrete WalkingPairf coconeS.ι.app j = coconeT.ι.app j 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.left } = coconeT.ι.app { as := WalkingPair.left }𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.right } = coconeT.ι.app { as := WalkingPair.right } 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.left } = coconeT.ι.app { as := WalkingPair.left } All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞coconeS:BinaryCofan B₁ B₂coconeT:BinaryCofan B₁ B₂sumS:IsColimit coconeSsumT:IsColimit coconeTf:coconeS.pt coconeT.pth_left:coconeT.ι.app { as := WalkingPair.left } = f coconeS.ι.app { as := WalkingPair.left }h_right:coconeT.ι.app { as := WalkingPair.right } = f coconeS.ι.app { as := WalkingPair.right }right✝:IsIso ff coconeS.ι.app { as := WalkingPair.right } = coconeT.ι.app { as := WalkingPair.right } All goals completed! 🐙

We next provide a proof using only the book definition of sum.

theorem uniqueness_of_sums' {𝒞 : Type u} [Category.{v, u} 𝒞] (B₁ B₂ S T : 𝒞) (j₁ : B₁ S) (j₂ : B₂ S) (hS : (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), (∃! f : S X, f₁ = f j₁ f₂ = f j₂)) (k₁ : B₁ T) (k₂ : B₂ T) (hT : (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), (∃! f : T X, f₁ = f k₁ f₂ = f k₂)) : Nonempty (S T) := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂Nonempty (S T) 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fNonempty (S T) 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gNonempty (S T) have hgf : g f = 𝟙 S := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂Nonempty (S T) 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = (g f) j₁ j₂ = (g f) j₂𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = 𝟙 S j₁ j₂ = 𝟙 S j₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = (g f) j₁ j₂ = (g f) j₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = (g f) j₁𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₂ = (g f) j₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = (g f) j₁ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = g(g f) j₁ = j₁ calc (g f) j₁ _ = g (f j₁) := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = g(g f) j₁ = g f j₁ All goals completed! 🐙 _ = g k₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gg f j₁ = g k₁ All goals completed! 🐙 _ = j₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gg k₁ = j₁ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₂ = (g f) j₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = g(g f) j₂ = j₂ calc (g f) j₂ _ = g (f j₂) := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = g(g f) j₂ = g f j₂ All goals completed! 🐙 _ = g k₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gg f j₂ = g k₂ All goals completed! 🐙 _ = j₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gg k₂ = j₂ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = 𝟙 S j₁ j₂ = 𝟙 S j₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = 𝟙 S j₁𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₂ = 𝟙 S j₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₁ = 𝟙 S j₁𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = gj₂ = 𝟙 S j₂ All goals completed! 🐙 have hfg : f g = 𝟙 T := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂Nonempty (S T) 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = (f g) k₁ k₂ = (f g) k₂𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = 𝟙 T k₁ k₂ = 𝟙 T k₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = (f g) k₁ k₂ = (f g) k₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = (f g) k₁𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₂ = (f g) k₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = (f g) k₁ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 S(f g) k₁ = k₁ calc (f g) k₁ _ = f (g k₁) := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 S(f g) k₁ = f g k₁ All goals completed! 🐙 _ = f j₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sf g k₁ = f j₁ All goals completed! 🐙 _ = k₁ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sf j₁ = k₁ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₂ = (f g) k₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 S(f g) k₂ = k₂ calc (f g) k₂ _ = f (g k₂) := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 S(f g) k₂ = f g k₂ All goals completed! 🐙 _ = f j₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sf g k₂ = f j₂ All goals completed! 🐙 _ = k₂ := 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sf j₂ = k₂ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = 𝟙 T k₁ k₂ = 𝟙 T k₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = 𝟙 T k₁𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₂ = 𝟙 T k₂ 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₁ = 𝟙 T k₁𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Sk₂ = 𝟙 T k₂ All goals completed! 🐙 𝒞:Type uinst✝:Category.{v, u} 𝒞B₁:𝒞B₂:𝒞S:𝒞T:𝒞j₁:B₁ Sj₂:B₂ ShS: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f j₁ f₂ = f j₂k₁:B₁ Tk₂:B₂ ThT: (X : 𝒞) (f₁ : B₁ X) (f₂ : B₂ X), ∃! f, f₁ = f k₁ f₂ = f k₂f:S Thf_comm:k₁ = f j₁ k₂ = f j₂right✝¹: (y : S T), (fun f k₁ = f j₁ k₂ = f j₂) y y = fg:T Shg_comm:j₁ = g k₁ j₂ = g k₂right✝: (y : T S), (fun f j₁ = f k₁ j₂ = f k₂) y y = ghgf:g f = 𝟙 Shfg:f g = 𝟙 TS T All goals completed! 🐙
Exercise 2 (p. 267)

Prove the following formulas:

(a) {D + D = 2 \times D}

(b) {D × D = D}

(c) {A × D = D + D}

Solution: Exercise 2

For part (a), we first formalise the graph 2.

def IG2 : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 2 toSrc := fun x x toTgt := fun x x }

We then show that {D + D = 2 \times D} (up to isomorphism).

open IrreflexiveGraph in noncomputable example {sumDD prod2D : IrreflexiveGraph} (j₁ : D sumDD) (j₂ : D sumDD) (h_sumDD : (X : IrreflexiveGraph) (f₁ : D X) (f₂ : D X), (∃! f : sumDD X, f₁ = f j₁ f₂ = f j₂)) (p₁ : prod2D IG2) (p₂ : prod2D D) (h_prod2D : (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), (∃! g : Y prod2D, g₁ = p₁ g g₂ = p₂ g)) : sumDD prod2D := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gsumDD prod2D -- Define graph G isomorphic to both sumDD and prod2D sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }sumDD prod2D -- Define injections to G let jG₁ : D G := { val := Empty.elim, fun _ 0 property := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x 0).2 D.toSrc = G.toSrc (Empty.elim, fun x 0).1 (Empty.elim, fun x 0).2 D.toTgt = G.toTgt (Empty.elim, fun x 0).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x 0).2 D.toSrc = G.toSrc (Empty.elim, fun x 0).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x 0).2 D.toTgt = G.toTgt (Empty.elim, fun x 0).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x 0).2 D.toSrc = G.toSrc (Empty.elim, fun x 0).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x 0).2 D.toTgt = G.toTgt (Empty.elim, fun x 0).1 (sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }x:D.carrierA((Empty.elim, fun x 0).2 D.toTgt) x = (G.toTgt (Empty.elim, fun x 0).1) x; All goals completed! 🐙) } let jG₂ : D G := { val := Empty.elim, fun _ 1 property := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toSrc = G.toSrc (Empty.elim, fun x 1).1 (Empty.elim, fun x 1).2 D.toTgt = G.toTgt (Empty.elim, fun x 1).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toSrc = G.toSrc (Empty.elim, fun x 1).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toTgt = G.toTgt (Empty.elim, fun x 1).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toSrc = G.toSrc (Empty.elim, fun x 1).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toTgt = G.toTgt (Empty.elim, fun x 1).1 (sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), x:D.carrierA((Empty.elim, fun x 1).2 D.toTgt) x = (G.toTgt (Empty.elim, fun x 1).1) x; All goals completed! 🐙) } -- Define projections from G let pG₁ : G IG2 := { val := Empty.elim, fun x x property := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), (Empty.elim, fun x x).2 G.toSrc = IG2.toSrc (Empty.elim, fun x x).1 (Empty.elim, fun x x).2 G.toTgt = IG2.toTgt (Empty.elim, fun x x).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), (Empty.elim, fun x x).2 G.toSrc = IG2.toSrc (Empty.elim, fun x x).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), (Empty.elim, fun x x).2 G.toTgt = IG2.toTgt (Empty.elim, fun x x).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), (Empty.elim, fun x x).2 G.toSrc = IG2.toSrc (Empty.elim, fun x x).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), (Empty.elim, fun x x).2 G.toTgt = IG2.toTgt (Empty.elim, fun x x).1 (sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), x:G.carrierA((Empty.elim, fun x x).2 G.toTgt) x = (IG2.toTgt (Empty.elim, fun x x).1) x; All goals completed! 🐙) } let pG₂ : G D := { val := Empty.elim, fun x () property := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toSrc = D.toSrc (Empty.elim, fun x ()).1 (Empty.elim, fun x ()).2 G.toTgt = D.toTgt (Empty.elim, fun x ()).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toSrc = D.toSrc (Empty.elim, fun x ()).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toTgt = D.toTgt (Empty.elim, fun x ()).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toSrc = D.toSrc (Empty.elim, fun x ()).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toTgt = D.toTgt (Empty.elim, fun x ()).1 (sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), x:G.carrierA((Empty.elim, fun x ()).2 G.toTgt) x = (D.toTgt (Empty.elim, fun x ()).1) x; All goals completed! 🐙) } -- Show that G satisfies universal property for sums have h_sumG : (X : IrreflexiveGraph) (f₁ : D X) (f₂ : D X), (∃! f : G X, f₁ = f jG₁ f₂ = f jG₂) := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gsumDD prod2D sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X∃! f, f₁ = f jG₁ f₂ = f jG₂ use { val := Empty.elim, fun | 0 => f₁.val.2 () | 1 => f₂.val.2 () property := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toSrc = X.toSrc (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt = X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toSrc = X.toSrc (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt = X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toSrc = X.toSrc (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt = X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 (sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xx:G.carrierA((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt) x = (X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1) x; All goals completed! 🐙) } sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(fun f f₁ = f jG₁ f₂ = f jG₂) (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X (y : G X), (fun f f₁ = f jG₁ f₂ = f jG₂) y y = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X(fun f f₁ = f jG₁ f₂ = f jG₂) (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf₁ = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₁sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf₂ = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂ all_goals sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xx:D.carrierA(↑f₂).1 x = (↑((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂)).1 xsumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xx:D.carrierD(↑f₂).2 x = (↑((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂)).2 x sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xx:D.carrierD(↑f₂).2 x = (↑((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂)).2 x All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D X (y : G X), (fun f f₁ = f jG₁ f₂ = f jG₂) y y = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂f = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierA(↑f).1 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).1 xsumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierD(↑f).2 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 x sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierA(↑f).1 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).1 x All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierD(↑f).2 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 x sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 0, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 0, )sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 1, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 1, ) sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 0, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 0, ) sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 0, ) = (↑(Empty.elim, fun x match x with | 0 => (↑(f jG₁)).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 0, ); All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 1, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 1, ) sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), X:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 1, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑(f jG₂)).2 ()), ).2 ((fun i i) 1, ); All goals completed! 🐙 -- Hence G is isomorphic to sumDD by uniqueness of sums sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDsumDD prod2D -- Show that G satisfies universal property for products have h_prodG : (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), (∃! g : Y G, g₁ = pG₁ g g₂ = pG₂ g) := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gsumDD prod2D sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D∃! g, g₁ = pG₁ g g₂ = pG₂ g use { val := g₂.val.1, g₁.val.2 property := sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toSrc = G.toSrc ((↑g₂).1, (↑g₁).2).1 ((↑g₂).1, (↑g₁).2).2 Y.toTgt = G.toTgt ((↑g₂).1, (↑g₁).2).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toSrc = G.toSrc ((↑g₂).1, (↑g₁).2).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toTgt = G.toTgt ((↑g₂).1, (↑g₁).2).1 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toSrc = G.toSrc ((↑g₂).1, (↑g₁).2).1sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toTgt = G.toTgt ((↑g₂).1, (↑g₁).2).1 (sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y De:Y.carrierA(((↑g₂).1, (↑g₁).2).2 Y.toTgt) e = (G.toTgt ((↑g₂).1, (↑g₁).2).1) e; All goals completed! 🐙) } sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D(fun g g₁ = pG₁ g g₂ = pG₂ g) ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D (y : Y G), (fun g g₁ = pG₁ g g₂ = pG₂ g) y y = ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D(fun g g₁ = pG₁ g g₂ = pG₂ g) ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg₁ = pG₁ ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg₂ = pG₂ ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg₁ = pG₁ ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y De:Y.carrierA(↑g₁).1 e = (↑(pG₁ ((↑g₂).1, (↑g₁).2), )).1 esumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y De:Y.carrierD(↑g₁).2 e = (↑(pG₁ ((↑g₂).1, (↑g₁).2), )).2 e sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y De:Y.carrierA(↑g₁).1 e = (↑(pG₁ ((↑g₂).1, (↑g₁).2), )).1 e All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y De:Y.carrierD(↑g₁).2 e = (↑(pG₁ ((↑g₂).1, (↑g₁).2), )).2 e All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg₂ = pG₂ ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y De:Y.carrierA(↑g₂).1 e = (↑(pG₂ ((↑g₂).1, (↑g₁).2), )).1 e All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y D (y : Y G), (fun g g₁ = pG₁ g g₂ = pG₂ g) y y = ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ gg = ((↑g₂).1, (↑g₁).2), sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierA(↑g).1 e = (↑((↑g₂).1, (↑g₁).2), ).1 esumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierD((↑g).2 e) = ((↑((↑g₂).1, (↑g₁).2), ).2 e) sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierA(↑g).1 e = (↑((↑g₂).1, (↑g₁).2), ).1 e All goals completed! 🐙 sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierD((↑g).2 e) = ((↑((↑g₂).1, (↑g₁).2), ).2 e) sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDY:IrreflexiveGraphg₁:Y IG2g₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierD((↑g).2 e) = ((↑((↑g₂).1, (↑(pG₁ g)).2), ).2 e); All goals completed! 🐙 -- Hence G is isomorphic to prod2D by uniqueness of products sumDD:IrreflexiveGraphprod2D:IrreflexiveGraphj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂p₁:prod2D IG2p₂:prod2D Dh_prod2D: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gG:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), pG₁:G IG2 := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), h_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDh_prodG: (Y : IrreflexiveGraph) (g₁ : Y IG2) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prod2DsumDD prod2D -- sumDD and prod2D are therefore isomorphic by transitivity All goals completed! 🐙

For part (b), we show that {D × D = D} (up to isomorphism).

open IrreflexiveGraph in noncomputable example {prodDD : IrreflexiveGraph} (p₁ : prodDD D) (p₂ : prodDD D) (h_prodDD : (Y : IrreflexiveGraph) (g₁ : Y D) (g₂ : Y D), (∃! g : Y prodDD, g₁ = p₁ g g₂ = p₂ g)) : prodDD D := { hom := { val := p₁.val.1, fun _ () property := prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ g((↑p₁).1, fun x ()).2 prodDD.toSrc = D.toSrc ((↑p₁).1, fun x ()).1 ((↑p₁).1, fun x ()).2 prodDD.toTgt = D.toTgt ((↑p₁).1, fun x ()).1 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ g((↑p₁).1, fun x ()).2 prodDD.toSrc = D.toSrc ((↑p₁).1, fun x ()).1prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ g((↑p₁).1, fun x ()).2 prodDD.toTgt = D.toTgt ((↑p₁).1, fun x ()).1 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ g((↑p₁).1, fun x ()).2 prodDD.toSrc = D.toSrc ((↑p₁).1, fun x ()).1prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ g((↑p₁).1, fun x ()).2 prodDD.toTgt = D.toTgt ((↑p₁).1, fun x ()).1 All goals completed! 🐙 } inv := Classical.choose (h_prodDD D (𝟙 D) (𝟙 D)).exists hom_inv_id := prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gClassical.choose ((↑p₁).1, fun x ()), = 𝟙 prodDD prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose Classical.choose ((↑p₁).1, fun x ()), = 𝟙 prodDD prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ Classical.choose ((↑p₁).1, fun x ()), p₂ = p₂ Classical.choose ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ 𝟙 prodDD p₂ = p₂ 𝟙 prodDD prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ Classical.choose ((↑p₁).1, fun x ()), p₂ = p₂ Classical.choose ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ Classical.choose ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₂ = p₂ Classical.choose ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ Classical.choose ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = ((↑p₁).1, fun x ()), All goals completed! 🐙 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₂ = p₂ Classical.choose ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₂ = ((↑p₁).1, fun x ()), prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose (↑p₂).1 = (↑((↑p₁).1, fun x ()), ).1prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose (↑p₂).2 = (↑((↑p₁).1, fun x ()), ).2 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose (↑p₂).1 = (↑((↑p₁).1, fun x ()), ).1 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose x:prodDD.carrierA(↑p₂).1 x = (↑((↑p₁).1, fun x ()), ).1 x All goals completed! 🐙 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose (↑p₂).2 = (↑((↑p₁).1, fun x ()), ).2 All goals completed! 🐙 prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ 𝟙 prodDD p₂ = p₂ 𝟙 prodDD prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ 𝟙 prodDDprodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₂ = p₂ 𝟙 prodDD prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₁ = p₁ 𝟙 prodDDprodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gh_finv_comm:𝟙 D = p₁ Classical.choose 𝟙 D = p₂ Classical.choose p₂ = p₂ 𝟙 prodDD All goals completed! 🐙 inv_hom_id := prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ g((↑p₁).1, fun x ()), Classical.choose = 𝟙 D prodDD:IrreflexiveGraphp₁:prodDD Dp₂:prodDD Dh_prodDD: (Y : IrreflexiveGraph) (g₁ g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gx:D.carrierA(↑(((↑p₁).1, fun x ()), Classical.choose )).1 x = (↑(𝟙 D)).1 x All goals completed! 🐙 }

The proof of {A × D = D + D} in part (c) is very similar to the proof of {D + D = 2 \times D} in part (a).

open IrreflexiveGraph in noncomputable example {prodAD sumDD : IrreflexiveGraph} (p₁ : prodAD A) (p₂ : prodAD D) (h_prodAD : (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), (∃! g : Y prodAD, g₁ = p₁ g g₂ = p₂ g)) (j₁ : D sumDD) (j₂ : D sumDD) (h_sumDD : (X : IrreflexiveGraph) (f₁ : D X) (f₂ : D X), (∃! f : sumDD X, f₁ = f j₁ f₂ = f j₂)) : prodAD sumDD := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂prodAD sumDD -- Define graph G isomorphic to both prodAD and sumDD prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }prodAD sumDD -- Define projections from G let pG₁ : G A := { val := Empty.elim, fun x x property := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x x).2 G.toSrc = A.toSrc (Empty.elim, fun x x).1 (Empty.elim, fun x x).2 G.toTgt = A.toTgt (Empty.elim, fun x x).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x x).2 G.toSrc = A.toSrc (Empty.elim, fun x x).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x x).2 G.toTgt = A.toTgt (Empty.elim, fun x x).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x x).2 G.toSrc = A.toSrc (Empty.elim, fun x x).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }(Empty.elim, fun x x).2 G.toTgt = A.toTgt (Empty.elim, fun x x).1 (prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }x:G.carrierA((Empty.elim, fun x x).2 G.toTgt) x = (A.toTgt (Empty.elim, fun x x).1) x; All goals completed! 🐙) } let pG₂ : G D := { val := Empty.elim, fun x () property := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toSrc = D.toSrc (Empty.elim, fun x ()).1 (Empty.elim, fun x ()).2 G.toTgt = D.toTgt (Empty.elim, fun x ()).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toSrc = D.toSrc (Empty.elim, fun x ()).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toTgt = D.toTgt (Empty.elim, fun x ()).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toSrc = D.toSrc (Empty.elim, fun x ()).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), (Empty.elim, fun x ()).2 G.toTgt = D.toTgt (Empty.elim, fun x ()).1 (prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), x:G.carrierA((Empty.elim, fun x ()).2 G.toTgt) x = (D.toTgt (Empty.elim, fun x ()).1) x; All goals completed! 🐙) } -- Define injections to G let jG₁ : D G := { val := Empty.elim, fun _ 0 property := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), (Empty.elim, fun x 0).2 D.toSrc = G.toSrc (Empty.elim, fun x 0).1 (Empty.elim, fun x 0).2 D.toTgt = G.toTgt (Empty.elim, fun x 0).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), (Empty.elim, fun x 0).2 D.toSrc = G.toSrc (Empty.elim, fun x 0).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), (Empty.elim, fun x 0).2 D.toTgt = G.toTgt (Empty.elim, fun x 0).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), (Empty.elim, fun x 0).2 D.toSrc = G.toSrc (Empty.elim, fun x 0).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), (Empty.elim, fun x 0).2 D.toTgt = G.toTgt (Empty.elim, fun x 0).1 (prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), x:D.carrierA((Empty.elim, fun x 0).2 D.toTgt) x = (G.toTgt (Empty.elim, fun x 0).1) x; All goals completed! 🐙) } let jG₂ : D G := { val := Empty.elim, fun _ 1 property := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toSrc = G.toSrc (Empty.elim, fun x 1).1 (Empty.elim, fun x 1).2 D.toTgt = G.toTgt (Empty.elim, fun x 1).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toSrc = G.toSrc (Empty.elim, fun x 1).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toTgt = G.toTgt (Empty.elim, fun x 1).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toSrc = G.toSrc (Empty.elim, fun x 1).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), (Empty.elim, fun x 1).2 D.toTgt = G.toTgt (Empty.elim, fun x 1).1 (prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), x:D.carrierA((Empty.elim, fun x 1).2 D.toTgt) x = (G.toTgt (Empty.elim, fun x 1).1) x; All goals completed! 🐙) } -- Show that G satisfies universal property for products have h_prodG : (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), (∃! g : Y G, g₁ = pG₁ g g₂ = pG₂ g) := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂prodAD sumDD prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D∃! g, g₁ = pG₁ g g₂ = pG₂ g use { val := g₂.val.1, g₁.val.2 property := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toSrc = G.toSrc ((↑g₂).1, (↑g₁).2).1 ((↑g₂).1, (↑g₁).2).2 Y.toTgt = G.toTgt ((↑g₂).1, (↑g₁).2).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toSrc = G.toSrc ((↑g₂).1, (↑g₁).2).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toTgt = G.toTgt ((↑g₂).1, (↑g₁).2).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toSrc = G.toSrc ((↑g₂).1, (↑g₁).2).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D((↑g₂).1, (↑g₁).2).2 Y.toTgt = G.toTgt ((↑g₂).1, (↑g₁).2).1 (prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y De:Y.carrierA(((↑g₂).1, (↑g₁).2).2 Y.toTgt) e = (G.toTgt ((↑g₂).1, (↑g₁).2).1) e; All goals completed! 🐙) } prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D(fun g g₁ = pG₁ g g₂ = pG₂ g) ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D (y : Y G), (fun g g₁ = pG₁ g g₂ = pG₂ g) y y = ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D(fun g g₁ = pG₁ g g₂ = pG₂ g) ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg₁ = pG₁ ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg₂ = pG₂ ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg₁ = pG₁ ((↑g₂).1, (↑g₁).2), All goals completed! 🐙 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg₂ = pG₂ ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y De:Y.carrierA(↑g₂).1 e = (↑(pG₂ ((↑g₂).1, (↑g₁).2), )).1 e All goals completed! 🐙 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y D (y : Y G), (fun g g₁ = pG₁ g g₂ = pG₂ g) y y = ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ gg = ((↑g₂).1, (↑g₁).2), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierA(↑g).1 e = (↑((↑g₂).1, (↑g₁).2), ).1 eprodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierD((↑g).2 e) = ((↑((↑g₂).1, (↑g₁).2), ).2 e) prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierA(↑g).1 e = (↑((↑g₂).1, (↑g₁).2), ).1 e All goals completed! 🐙 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierD((↑g).2 e) = ((↑((↑g₂).1, (↑g₁).2), ).2 e) prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), Y:IrreflexiveGraphg₁:Y Ag₂:Y Dg:Y Ghg:g₁ = pG₁ g g₂ = pG₂ ge:Y.carrierD((↑g).2 e) = ((↑((↑g₂).1, (↑(pG₁ g)).2), ).2 e); All goals completed! 🐙 -- Hence G is isomorphic to prodAD by uniqueness of products prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADprodAD sumDD -- Show that G satisfies universal property for sums have h_sumG : (X : IrreflexiveGraph) (f₁ : D X) (f₂ : D X), (∃! f : G X, f₁ = f jG₁ f₂ = f jG₂) := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂prodAD sumDD prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X∃! f, f₁ = f jG₁ f₂ = f jG₂ use { val := Empty.elim, fun | 0 => f₁.val.2 () | 1 => f₂.val.2 () property := prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toSrc = X.toSrc (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt = X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toSrc = X.toSrc (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt = X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toSrc = X.toSrc (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt = X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1 (prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xx:G.carrierA((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).2 G.toTgt) x = (X.toTgt (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()).1) x; All goals completed! 🐙) } prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(fun f f₁ = f jG₁ f₂ = f jG₂) (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X (y : G X), (fun f f₁ = f jG₁ f₂ = f jG₂) y y = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X(fun f f₁ = f jG₁ f₂ = f jG₂) (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf₁ = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₁prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf₂ = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂ all_goals prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xx:D.carrierA(↑f₂).1 x = (↑((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂)).1 xprodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xx:D.carrierD(↑f₂).2 x = (↑((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂)).2 x prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xx:D.carrierD(↑f₂).2 x = (↑((Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), jG₂)).2 x All goals completed! 🐙 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D X (y : G X), (fun f f₁ = f jG₁ f₂ = f jG₂) y y = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂f = (Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierA(↑f).1 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).1 xprodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierD(↑f).2 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 x prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierA(↑f).1 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).1 x All goals completed! 🐙 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂x:G.carrierD(↑f).2 x = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 x prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 0, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 0, )prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 1, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 1, ) prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 0, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 0, ) prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 0, ) = (↑(Empty.elim, fun x match x with | 0 => (↑(f jG₁)).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 0, ); All goals completed! 🐙 prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 1, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑f₂).2 ()), ).2 ((fun i i) 1, ) prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADX:IrreflexiveGraphf₁:D Xf₂:D Xf:G Xhf:f₁ = f jG₁ f₂ = f jG₂(↑f).2 ((fun i i) 1, ) = (↑(Empty.elim, fun x match x with | 0 => (↑f₁).2 () | 1 => (↑(f jG₂)).2 ()), ).2 ((fun i i) 1, ); All goals completed! 🐙 -- Hence G is isomorphic to sumDD by uniqueness of sums prodAD:IrreflexiveGraphsumDD:IrreflexiveGraphp₁:prodAD Ap₂:prodAD Dh_prodAD: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = p₁ g g₂ = p₂ gj₁:D sumDDj₂:D sumDDh_sumDD: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f j₁ f₂ = f j₂G:IrreflexiveGraph := { carrierA := Empty, carrierD := Fin 2, toSrc := Empty.elim, toTgt := Empty.elim }pG₁:G A := (Empty.elim, fun x x), pG₂:G D := (Empty.elim, fun x ()), jG₁:D G := (Empty.elim, fun x 0), jG₂:D G := (Empty.elim, fun x 1), h_prodG: (Y : IrreflexiveGraph) (g₁ : Y A) (g₂ : Y D), ∃! g, g₁ = pG₁ g g₂ = pG₂ gh_iso_prod:G prodADh_sumG: (X : IrreflexiveGraph) (f₁ f₂ : D X), ∃! f, f₁ = f jG₁ f₂ = f jG₂h_iso_sum:G sumDDprodAD sumDD -- prodAD and sumDD are therefore isomorphic by transitivity All goals completed! 🐙
Exercise 3 (p. 268)

Reread Section 5 of Session 15 and find a method, starting from presentations of X^{↻\alpha} and Y^{↻\beta}, to construct presentations of

(a) {X^{↻\alpha} + Y^{↻\beta}}

(b) {X^{↻\alpha} \times Y^{↻\beta}}

Part (b) is harder than part (a).

Solution: Exercise 3

(a) Given a presentation of X^{↻\alpha} with a list of generators (\mathbf{L}_X) and a list of relations (\mathbf{R}_X), and a presentation of Y^{↻\beta} with a list of generators (\mathbf{L}_Y) and a list of relations (\mathbf{R}_Y), then a presentation of {X^{↻\alpha} + Y^{↻\beta}} can be constructed simply from the disjoint union of generators (\mathbf{L}_X) and (\mathbf{L}_Y), together with the disjoint union of relations (\mathbf{R}_X) and (\mathbf{R}_Y) (with suitable relabelling of the generators and relations to avoid name clashes between generators injected from X^{↻\alpha} and those injected from Y^{↻\beta}).

TODO Exercise 24.3 (b)