A Lean Companion to Conceptual Mathematics

Test 4πŸ”—

Problem 1 (p. 300)

Show that if {B \times C = \mathbf{1}}, then {B = \mathbf{1}}.

Your demonstration should work in any category.

Hint: First explain what '{B \times C = \mathbf{1}}' means!

Solution: Problem 1

Since {B \times C} is both a product and a terminal object, we have

noncomputable example {π’ž : Type u} [Category.{v, u} π’ž] [HasTerminal π’ž] {B C : π’ž} [HasBinaryProduct B C] (h : B β¨― C β‰… ⊀_ π’ž) : B β‰… ⊀_ π’ž := π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasTerminal π’žB:π’žC:π’žinst✝:HasBinaryProduct B Ch:B β¨― C β‰… ⊀_ π’žβŠ’ B β‰… ⊀_ π’ž π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasTerminal π’žB:π’žC:π’žinst✝:HasBinaryProduct B Ch:B β¨― C β‰… ⊀_ π’žtBxC:IsTerminal (B β¨― C) := terminalIsTerminal.ofIso h.symm⊒ B β‰… ⊀_ π’ž π’ž:Type uinst✝²:Category.{v, u} π’žinst✝¹:HasTerminal π’žB:π’žC:π’žinst✝:HasBinaryProduct B Ch:B β¨― C β‰… ⊀_ π’žtBxC:IsTerminal (B β¨― C) := terminalIsTerminal.ofIso h.symmiso:B β‰… B β¨― C := { hom := prod.lift (πŸ™ B) (prod.snd ⊚ tBxC.from B), inv := prod.fst, hom_inv_id := β‹―, inv_hom_id := β‹― }⊒ B β‰… ⊀_ π’ž All goals completed! πŸ™
Problem 2 (p. 300)

All parts of this problem are in π‘Ίβ‡Š, the category of irreflexive graphs.

abbrev IrreflexiveGraph.D : IrreflexiveGraph := { carrierA := Empty carrierD := Unit toSrc := Empty.elim toTgt := Empty.elim } abbrev IrreflexiveGraph.A : IrreflexiveGraph := { carrierA := Unit carrierD := Fin 2 toSrc := fun _ ↦ 0 toTgt := fun _ ↦ 1 } def B : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 2 toSrc := fun | 0 => 0 | 1 => 0 toTgt := fun | 0 => 0 | 1 => 1 } def C : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 3 toSrc := fun | 0 => 1 | 1 => 1 toTgt := fun | 0 => 0 | 1 => 2 }

(a) Find the number of maps {\mathbf{1} \rightarrow B + D} and the number of maps {\mathbf{1} \rightarrow C}.

(b) 'Calculate' {A \times B}, {A \times D}, and {A \times C}. (Draw picturesβ€”internal diagramsβ€”of them.)

(c) Use the distributive law, and results from (b), to calculate A \times (B + D)

(d) Show that {A \times (B + D)} is isomorphic to {A \times C}.

Note: Comparing (a) and (d) illustrates the failure of 'cancellation':

From '{A \times (B + D) = A \times C}' we cannot cancel A and conclude that '{B + D = C}'.

Solution: Problem 2

(a) Since {B + D} has a single loop, there is exactly one map {\mathbf{1} \rightarrow B + D}.

open IrreflexiveGraph def BuD : IrreflexiveGraph := { carrierA := Sum B.carrierA D.carrierA carrierD := Sum B.carrierD D.carrierD toSrc := fun | Sum.inl a => Sum.inl (B.toSrc a) | Sum.inr a => Sum.inr (D.toSrc a) toTgt := fun | Sum.inl a => Sum.inl (B.toTgt a) | Sum.inr a => Sum.inr (D.toTgt a) } example : Unique (termIG ⟢ BuD) := { default := ⟨ (fun _ ↦ Sum.inl (0 : Fin 2), fun _ ↦ Sum.inl (0 : Fin 2)), ⊒ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).2 ⊚ termIG.toSrc = BuD.toSrc ⊚ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).1 ∧ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).2 ⊚ termIG.toTgt = BuD.toTgt ⊚ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).1 ⊒ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).2 ⊚ termIG.toSrc = BuD.toSrc ⊚ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).1⊒ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).2 ⊚ termIG.toTgt = BuD.toTgt ⊚ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).1 ⊒ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).2 ⊚ termIG.toSrc = BuD.toSrc ⊚ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).1⊒ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).2 ⊚ termIG.toTgt = BuD.toTgt ⊚ (fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0).1 All goals completed! πŸ™ ⟩ uniq f := f:termIG ⟢ BuD⊒ f = ⟨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ© f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())⊒ f = ⟨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ© f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())hTgt:(↑f).2 () = BuD.toTgt ((↑f).1 ())⊒ f = ⟨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ© f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())hTgt:(↑f).2 () = BuD.toTgt ((↑f).1 ())h_eq:BuD.toSrc ((↑f).1 ()) = BuD.toTgt ((↑f).1 ())⊒ f = ⟨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ© f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())hTgt:(↑f).2 () = BuD.toTgt ((↑f).1 ())h_eq:BuD.toSrc ((↑f).1 ()) = BuD.toTgt ((↑f).1 ())⊒ (↑f).1 = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).1f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())hTgt:(↑f).2 () = BuD.toTgt ((↑f).1 ())h_eq:BuD.toSrc ((↑f).1 ()) = BuD.toTgt ((↑f).1 ())⊒ (↑f).2 = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 all_goals f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())hTgt:(↑f).2 () = BuD.toTgt ((↑f).1 ())h_eq:BuD.toSrc ((↑f).1 ()) = BuD.toTgt ((↑f).1 ())x:termIG.carrierD⊒ (↑f).2 x = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 x f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc ((↑f).1 ())hTgt:(↑f).2 () = BuD.toTgt ((↑f).1 ())h_eq:BuD.toSrc ((↑f).1 ()) = BuD.toTgt ((↑f).1 ())⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit f:termIG ⟢ BuDa:BuD.carrierAhSrc:(↑f).2 () = BuD.toSrc ahTgt:(↑f).2 () = BuD.toTgt ah_eq:BuD.toSrc a = BuD.toTgt a⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit f:termIG ⟢ BuDa:BuD.carrierAhSrc:(↑f).2 () = BuD.toSrc ahTgt:(↑f).2 () = BuD.toTgt ah_eq:BuD.toSrc a = BuD.toTgt a⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit cases a with f:termIG ⟢ BuDb:B.carrierAhSrc:(↑f).2 () = BuD.toSrc (Sum.inl b)hTgt:(↑f).2 () = BuD.toTgt (Sum.inl b)h_eq:BuD.toSrc (Sum.inl b) = BuD.toTgt (Sum.inl b)⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unitf:termIG ⟢ BuDb:B.carrierAhSrc:(↑f).2 () = BuD.toSrc (Sum.inl b)hTgt:(↑f).2 () = BuD.toTgt (Sum.inl b)h_eq:BuD.toSrc (Sum.inl b) = BuD.toTgt (Sum.inl b)⊒ Sum.inl b = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).1 PUnit.unit f:termIG ⟢ BuDb:Fin 2hSrc:(↑f).2 () = BuD.toSrc (Sum.inl b)hTgt:(↑f).2 () = BuD.toTgt (Sum.inl b)h_eq:BuD.toSrc (Sum.inl b) = BuD.toTgt (Sum.inl b)⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))hTgt:(↑f).2 () = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))h_eq:BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©)) = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unitf:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))hTgt:(↑f).2 () = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))h_eq:BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©)) = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))hTgt:(↑f).2 () = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))h_eq:BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©)) = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit first | f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))hTgt:(↑f).2 () = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))h_eq:BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©)) = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨0, β‹―βŸ©))⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit | All goals completed! πŸ™ f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))hTgt:(↑f).2 () = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))h_eq:BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©)) = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit f:termIG ⟢ BuDhSrc:(↑f).2 () = BuD.toSrc (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))hTgt:(↑f).2 () = BuD.toTgt (Sum.inl ((fun i ↦ i) ⟨1, β‹―βŸ©))h_eq:Sum.inl 0 = Sum.inl 1⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unit All goals completed! πŸ™ try All goals completed! πŸ™ f:termIG ⟢ BuDd:D.carrierAhSrc:(↑f).2 () = BuD.toSrc (Sum.inr d)hTgt:(↑f).2 () = BuD.toTgt (Sum.inr d)h_eq:BuD.toSrc (Sum.inr d) = BuD.toTgt (Sum.inr d)⊒ (↑f).2 PUnit.unit = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).2 PUnit.unitf:termIG ⟢ BuDd:D.carrierAhSrc:(↑f).2 () = BuD.toSrc (Sum.inr d)hTgt:(↑f).2 () = BuD.toTgt (Sum.inr d)h_eq:BuD.toSrc (Sum.inr d) = BuD.toTgt (Sum.inr d)⊒ Sum.inr d = (β†‘βŸ¨(fun x ↦ Sum.inl 0, fun x ↦ Sum.inl 0), β‹―βŸ©).1 PUnit.unit All goals completed! πŸ™ }

Since C has no loops, there are no maps {\mathbf{1} \rightarrow C}.

example : IsEmpty (termIG ⟢ C) := { false f := f:termIG ⟢ C⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:C.toSrc ((↑f).1 ()) = C.toTgt ((↑f).1 ())⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())a:C.carrierAh_eq:C.toSrc a = C.toTgt a⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())a:Fin 2h_eq:C.toSrc a = C.toTgt a⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:C.toSrc ((fun i ↦ i) ⟨0, β‹―βŸ©) = C.toTgt ((fun i ↦ i) ⟨0, β‹―βŸ©)⊒ Falsef:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:C.toSrc ((fun i ↦ i) ⟨1, β‹―βŸ©) = C.toTgt ((fun i ↦ i) ⟨1, β‹―βŸ©)⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:C.toSrc ((fun i ↦ i) ⟨0, β‹―βŸ©) = C.toTgt ((fun i ↦ i) ⟨0, β‹―βŸ©)⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:1 = 0⊒ False All goals completed! πŸ™ f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:C.toSrc ((fun i ↦ i) ⟨1, β‹―βŸ©) = C.toTgt ((fun i ↦ i) ⟨1, β‹―βŸ©)⊒ False f:termIG ⟢ ChSrc:(↑f).2 () = C.toSrc ((↑f).1 ())hTgt:(↑f).2 () = C.toTgt ((↑f).1 ())h_eq:1 = 2⊒ False All goals completed! πŸ™ }

(b) We can formalise the products {A \times B}, {A \times D}, and {A \times C} as follows:

def AxB : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 2 Γ— Fin 2 toSrc := fun _ ↦ (0, 0) toTgt := fun | 0 => (1, 0) | 1 => (1, 1) } def AxD : IrreflexiveGraph := { carrierA := Empty carrierD := Fin 2 toSrc := Empty.elim toTgt := Empty.elim } def AxC : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 2 Γ— Fin 3 toSrc := fun _ ↦ (0, 1) toTgt := fun | 0 => (1, 0) | 1 => (1, 2) }

(c) In the same manner as part (b), we can formalise {A \times (B + D)} as follows:

def AxBuD : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 2 Γ— Fin 3 toSrc := fun _ ↦ (0, 0) toTgt := fun | 0 => (1, 0) | 1 => (1, 1) }

(d) We can then use our definitions from parts (b) and (c) to show that {A \times (B + D)} is isomorphic to {A \times C}.

example : AxBuD β‰… AxC := ⊒ AxBuD β‰… AxC fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ AxBuD β‰… AxC exact { hom := ⟨(fun a ↦ a, fD), fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxBuD.toSrc = AxC.toSrc ⊚ (fun a ↦ a, fD).1 ∧ (fun a ↦ a, fD).2 ⊚ AxBuD.toTgt = AxC.toTgt ⊚ (fun a ↦ a, fD).1 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxBuD.toSrc = AxC.toSrc ⊚ (fun a ↦ a, fD).1fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxBuD.toTgt = AxC.toTgt ⊚ (fun a ↦ a, fD).1 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxBuD.toSrc = AxC.toSrc ⊚ (fun a ↦ a, fD).1 All goals completed! πŸ™ fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxBuD.toTgt = AxC.toTgt ⊚ (fun a ↦ a, fD).1 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:AxBuD.carrierA⊒ ((fun a ↦ a, fD).2 ⊚ AxBuD.toTgt) d = (AxC.toTgt ⊚ (fun a ↦ a, fD).1) d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:Fin 2⊒ ((fun a ↦ a, fD).2 ⊚ AxBuD.toTgt) d = (AxC.toTgt ⊚ (fun a ↦ a, fD).1) d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxBuD.toTgt) ((fun i ↦ i) ⟨0, β‹―βŸ©) = (AxC.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxBuD.toTgt) ((fun i ↦ i) ⟨1, β‹―βŸ©) = (AxC.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨1, β‹―βŸ©) fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxBuD.toTgt) ((fun i ↦ i) ⟨0, β‹―βŸ©) = (AxC.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxBuD.toTgt) ((fun i ↦ i) ⟨1, β‹―βŸ©) = (AxC.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨1, β‹―βŸ©) All goals completed! πŸ™βŸ© inv := ⟨(fun a ↦ a, fD), fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxC.toSrc = AxBuD.toSrc ⊚ (fun a ↦ a, fD).1 ∧ (fun a ↦ a, fD).2 ⊚ AxC.toTgt = AxBuD.toTgt ⊚ (fun a ↦ a, fD).1 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxC.toSrc = AxBuD.toSrc ⊚ (fun a ↦ a, fD).1fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxC.toTgt = AxBuD.toTgt ⊚ (fun a ↦ a, fD).1 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxC.toSrc = AxBuD.toSrc ⊚ (fun a ↦ a, fD).1 All goals completed! πŸ™ fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (fun a ↦ a, fD).2 ⊚ AxC.toTgt = AxBuD.toTgt ⊚ (fun a ↦ a, fD).1 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:AxC.carrierA⊒ ((fun a ↦ a, fD).2 ⊚ AxC.toTgt) d = (AxBuD.toTgt ⊚ (fun a ↦ a, fD).1) d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:Fin 2⊒ ((fun a ↦ a, fD).2 ⊚ AxC.toTgt) d = (AxBuD.toTgt ⊚ (fun a ↦ a, fD).1) d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxC.toTgt) ((fun i ↦ i) ⟨0, β‹―βŸ©) = (AxBuD.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxC.toTgt) ((fun i ↦ i) ⟨1, β‹―βŸ©) = (AxBuD.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨1, β‹―βŸ©) fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxC.toTgt) ((fun i ↦ i) ⟨0, β‹―βŸ©) = (AxBuD.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ((fun a ↦ a, fD).2 ⊚ AxC.toTgt) ((fun i ↦ i) ⟨1, β‹―βŸ©) = (AxBuD.toTgt ⊚ (fun a ↦ a, fD).1) ((fun i ↦ i) ⟨1, β‹―βŸ©) All goals completed! πŸ™βŸ© hom_inv_id := fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ© = πŸ™ AxBuD fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).1 = (↑(πŸ™ AxBuD)).1fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 = (↑(πŸ™ AxBuD)).2 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).1 = (↑(πŸ™ AxBuD)).1 All goals completed! πŸ™ fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 = (↑(πŸ™ AxBuD)).2 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:AxBuD.carrierD⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 d = (↑(πŸ™ AxBuD)).2 d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:Fin 2 Γ— Fin 3⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 d = (↑(πŸ™ AxBuD)).2 d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxBuD)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) All goals completed! πŸ™ inv_hom_id := fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ ⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ© = πŸ™ AxC fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).1 = (↑(πŸ™ AxC)).1fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 = (↑(πŸ™ AxC)).2 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).1 = (↑(πŸ™ AxC)).1 All goals completed! πŸ™ fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 = (↑(πŸ™ AxC)).2 fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:AxC.carrierD⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 d = (↑(πŸ™ AxC)).2 d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)d:Fin 2 Γ— Fin 3⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 d = (↑(πŸ™ AxC)).2 d fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)fD:Fin 2 Γ— Fin 3 ⟢ Fin 2 Γ— Fin 3 := fun x ↦ match x with | (0, 0) => (0, 1) | (0, 1) => (0, 0) | (1, 1) => (1, 2) | (1, 2) => (1, 1) | (d₁, dβ‚‚) => (d₁, dβ‚‚)⊒ (↑(⟨(fun a ↦ a, fD), β‹―βŸ© ⊚ ⟨(fun a ↦ a, fD), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ AxC)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) All goals completed! πŸ™ }