-- Cartesian products and cardinal multiplication
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Cardinal.Product
import Sum

-- The direct product of two set-valued function graphs. The graph is a
-- bounded Separation subset of (A × B) × (C × D).
def productMap (f g A B C D : Set) : Set := { p ∈ (A × B) × (C × D) | ∃ x ∈ A, ∃ y ∈ B, ∃ z ∈ C, ∃ w ∈ D, relates(f, x, z) ∧ relates(g, y, w) ∧ p = ((x, y) ↦ (z, w)) }

theorem productMap.relates (f g A B C D x y z w : Set)
  requires hx : x ∈ A
  requires hy : y ∈ B
  requires hz : z ∈ C
  requires hw : w ∈ D
  requires hf : relates(f, x, z)
  requires hg : relates(g, y, w)
  shows relates(productMap(f, g, A, B, C, D), (x, y), (z, w))
proof
  simp [relates, productMap.membership, product.pair]

theorem productMap.factors (f g A B C D u v : Set)
  requires h : relates(productMap(f, g, A, B, C, D), u, v)
  shows ∃ x ∈ A, ∃ y ∈ B, ∃ z ∈ C, ∃ w ∈ D, u = (x, y) ∧ v = (z, w) ∧ relates(f, x, z) ∧ relates(g, y, w)
proof
  unfold relates at h
  obtain ⟨bounded, x, hxA, y, hyB, z, hzC, w, hwD, hf, hg, pairShape⟩ := productMap.membership.forward with h
  obtain (source, target) := orderedPair.injective with pairShape
  refine ⟨x, hxA, y, hyB, z, hzC, w, hwD, source, target, hf, hg⟩

theorem productMap.relation (f g A B C D : Set)
  shows RelationBetween(productMap(f, g, A, B, C, D), A × B, C × D)
proof
  simp [RelationBetween, Subset]

theorem productMap.total (f g A B C D : Set)
  requires hf : f : A → C
  requires hg : g : B → D
  shows TotalBetween(productMap(f, g, A, B, C, D), A × B, C × D)
proof
  intros u hu
  obtain ⟨sourceBound, x, hxA, y, hyB, sourceShape⟩ := product.membership.forward with hu
  obtain ⟨z, hzC, hfxz⟩ := FunctionBetween.exists_value with hf, hxA
  obtain ⟨w, hwD, hgyw⟩ := FunctionBetween.exists_value with hg, hyB
  witness (z, w)
  constructor
  . have targetPair := product.pair at z, w, C, D
    exact targetPair with hzC, hwD
  . rw sourceShape
    exact productMap.relates with hxA, hyB, hzC, hwD, hfxz, hgyw

theorem productMap.functional (f g A B C D : Set)
  requires hf : f : A → C
  requires hg : g : B → D
  shows Functional(productMap(f, g, A, B, C, D))
proof
  intros u v huv q huq
  obtain ⟨x1, hx1A, y1, hy1B, z1, hz1C, w1, hw1D, source1, target1, hfxz1, hgyw1⟩ := productMap.factors with huv
  obtain ⟨x2, hx2A, y2, hy2B, z2, hz2C, w2, hw2D, source2, target2, hfxz2, hgyw2⟩ := productMap.factors with huq
  rw source1 at source2
  obtain (sameX, sameY) := orderedPair.injective with source2
  rw ← sameX at hfxz2
  rw ← sameY at hgyw2
  have fUnique := FunctionBetween.functional with hf, x1, z1, hfxz1, z2, hfxz2
  have gUnique := FunctionBetween.functional with hg, y1, w1, hgyw1, w2, hgyw2
  rw [target1, target2, fUnique, gUnique]
  rfl

theorem productMap.function (f g A B C D : Set)
  requires hf : f : A → C
  requires hg : g : B → D
  shows productMap(f, g, A, B, C, D) : A × B → C × D
proof
  constructor
  . exact productMap.relation at f, g, A, B, C, D
  . constructor
    . have functional := productMap.functional at f, g, A, B, C, D
      exact functional with hf, hg
    . exact productMap.total with hf, hg

theorem productMap.apply (f g A B C D x y : Set)
  requires functionF : f : A → C
  requires functionG : g : B → D
  requires hx : x ∈ A
  requires hy : y ∈ B
  shows productMap(f, g, A, B, C, D)((x, y)) = (f(x), g(y))
proof
  have function := productMap.function with functionF, functionG
  have input := product.pair with hx, hy
  have valueF := FunctionBetween.apply_closed with hx
  have valueG := FunctionBetween.apply_closed with hy
  have output := product.pair with valueF, valueG
  have edgeF := FunctionBetween.relates_apply with hx
  have edgeG := FunctionBetween.relates_apply with hy
  have edge := productMap.relates with hx, hy
  exact FunctionBetween.apply_value with *

theorem productMap.injective (f g A B C D : Set)
  requires hf : InjectiveBetween(f, A, C)
  requires hg : InjectiveBetween(g, B, D)
  shows InjectiveBetween(productMap(f, g, A, B, C, D), A × B, C × D)
proof
  constructor
  . have fFunction := Injective.function with hf
    have gFunction := Injective.function with hg
    exact productMap.function with fFunction, gFunction
  . intros u hu v hv q hq huq hvq
    obtain ⟨x1, hx1A, y1, hy1B, z1, hz1C, w1, hw1D, source1, target1, hfxz1, hgyw1⟩ := productMap.factors with huq
    obtain ⟨x2, hx2A, y2, hy2B, z2, hz2C, w2, hw2D, source2, target2, hfxz2, hgyw2⟩ := productMap.factors with hvq
    rw target1 at target2
    obtain (sameZ, sameW) := orderedPair.injective with target2
    rw ← sameZ at hfxz2
    rw ← sameW at hgyw2
    have sameX := Injective.cancel with hf, hx1A, hx2A, hz1C, hfxz1, hfxz2
    have sameY := Injective.cancel with hg, hy1B, hy2B, hw1D, hgyw1, hgyw2
    rw [source1, source2, sameX, sameY]
    rfl

theorem productMap.surjective (f g A B C D : Set)
  requires hf : SurjectiveBetween(f, A, C)
  requires hg : SurjectiveBetween(g, B, D)
  shows SurjectiveBetween(productMap(f, g, A, B, C, D), A × B, C × D)
proof
  constructor
  . have fFunction := Surjective.function with hf
    have gFunction := Surjective.function with hg
    exact productMap.function with fFunction, gFunction
  . intros q hq
    obtain ⟨targetBound, z, hzC, w, hwD, targetShape⟩ := product.membership.forward with hq
    rcases hf with (fFunctionAgain, fOnto)
    specialize fOnto with z, hzC
    obtain ⟨x, hxA, hfxz⟩ := fOnto
    rcases hg with (gFunctionAgain, gOnto)
    specialize gOnto with w, hwD
    obtain ⟨y, hyB, hgyw⟩ := gOnto
    witness (x, y)
    constructor
    . have sourcePair := product.pair at x, y, A, B
      exact sourcePair with hxA, hyB
    . rw targetShape
      exact productMap.relates with hxA, hyB, hzC, hwD, hfxz, hgyw

theorem productMap.bijective (f g A B C D : Set)
  requires hf : BijectiveBetween(f, A, C)
  requires hg : BijectiveBetween(g, B, D)
  shows BijectiveBetween(productMap(f, g, A, B, C, D), A × B, C × D)
proof
  --! Split the product bijection into its two obligations.
  --| Each coordinate is transported by its own set-valued graph.
  constructor
  . --! Injectivity coordinatewise
    have fInjective := Bijective.injective with hf
    have gInjective := Bijective.injective with hg
    exact productMap.injective with fInjective, gInjective
  . --! Surjectivity coordinatewise
    have fSurjective := Bijective.surjective with hf
    have gSurjective := Bijective.surjective with hg
    exact productMap.surjective with fSurjective, gSurjective

theorem Equipotent.product (A B C D : Set)
  requires hAC : A ≃ C
  requires hBD : B ≃ D
  shows (A × B) ≃ (C × D)
proof
  obtain (f, hf) := hAC
  obtain (g, hg) := hBD
  witness productMap(f, g, A, B, C, D)
  exact productMap.bijective with hf, hg

theorem product.zero_left (A : Set)
  shows 0 × A = 0
proof
  ext p
  constructor
  . intro hp
    obtain ⟨bounded, x, hxZero, rest⟩ := product.membership.forward with hp
    rw nat.zero at hxZero
    simp
  . intro hp
    rw nat.zero at hp
    simp

-- Adding the new point m to the first factor adds one complete row. This
-- graph separates the old rectangle from that row by the existing sum tags.
def productStepMap (m n : Set) : Set := { p ∈ (succ(m) × n) × ((m × n) ⊎ n) | (∃ x ∈ m, ∃ y ∈ n, p = ((x, y) ↦ inl((x, y)))) ∨ (∃ y ∈ n, p = ((m, y) ↦ inr(y))) }

theorem productStepMap.relates_old {m : Nat} (n x y : Set)
  requires hx : x ∈ m
  requires hy : y ∈ n
  shows relates(productStepMap(m, n), (x, y), inl((x, y)))
proof
  unfold relates
  apply productStepMap.membership.backward
  constructor
  . apply product.pair at (x, y), inl((x, y)), succ(m) × n, (m × n) ⊎ n
    . apply product.pair at x, y, succ(m), n
      . apply membership.successor_set{n := m}.backward at x
        left
        exact hx
      . exact hy
    . have pairMember := product.pair with hx, hy
      exact disjointSum.left with pairMember
  . left
    refine ⟨x, hx, y, hy, rfl⟩

theorem productStepMap.relates_new {m : Nat} (n y : Set)
  requires hy : y ∈ n
  shows relates(productStepMap(m, n), (m, y), inr(y))
proof
  unfold relates
  apply productStepMap.membership.backward
  constructor
  . apply product.pair at (m, y), inr(y), succ(m) × n, (m × n) ⊎ n
    . apply product.pair at m, y, succ(m), n
      . apply membership.successor_set{n := m}.backward at m
        right
        rfl
      . exact hy
    . have tagged := disjointSum.right at y, m × n, n
      exact tagged with hy
  . right
    refine ⟨y, hy, rfl⟩

theorem productStepMap.factors (m n u v : Set)
  requires h : relates(productStepMap(m, n), u, v)
  shows (∃ x ∈ m, ∃ y ∈ n, u = (x, y) ∧ v = inl((x, y))) ∨ (∃ y ∈ n, u = (m, y) ∧ v = inr(y))
proof
  unfold relates at h
  obtain (bounded, alternatives) := productStepMap.membership.forward with h
  cases alternatives with old | newest
  . obtain (x, hx) := old
    rcases hx with ⟨hxM, y, hyN, pairShape⟩
    obtain (source, target) := orderedPair.injective with pairShape
    left
    refine ⟨x, hxM, y, hyN, source, target⟩
  . obtain (yNew, hyNew) := newest
    rcases hyNew with (hyNewN, pairShapeNew)
    obtain (sourceNew, targetNew) := orderedPair.injective with pairShapeNew
    right
    refine ⟨yNew, hyNewN, sourceNew, targetNew⟩

theorem productStepMap.relation (m n : Set)
  shows RelationBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)
proof
  simp [RelationBetween, Subset]

theorem productStepMap.total {m : Nat} (n : Set)
  shows TotalBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)
proof
  intros u hu
  obtain ⟨bounded, x, hxSucc, y, hyN, source⟩ := product.membership.forward with hu
  have successorShape := membership.successor_set{n := m}.forward with hxSucc
  cases successorShape with old | newest
  . witness inl((x, y))
    constructor
    . have pairMember := product.pair with old, hyN
      exact disjointSum.left with pairMember
    . rw source
      exact productStepMap.relates_old{m := m} at n, x, y
  . witness inr(y)
    constructor
    . have tagged := disjointSum.right at y, m × n, n
      exact tagged with hyN
    . rw [source, newest]
      exact productStepMap.relates_new{m := m} at n, y

theorem productStepMap.functional {m : Nat} (n : Set)
  shows Functional(productStepMap(m, n))
proof
  intros u v huv q huq
  have first := productStepMap.factors with huv
  have second := productStepMap.factors with huq
  cases first with firstOld | firstNew
  . cases second with secondOld | secondNew
    . obtain (x1, hx1) := firstOld
      rcases hx1 with ⟨hx1M, y1, hy1N, source1, target1⟩
      obtain ⟨x2, hx2M, y2, hy2N, source2, target2⟩ := secondOld
      rw source1 at source2
      obtain (sameX, sameY) := orderedPair.injective with source2
      rw [target1, target2, sameX, sameY]
      rfl
    . obtain (xOld, hxOld) := firstOld
      rcases hxOld with ⟨hxOldM, yOld, hyOldN, sourceOld, targetOld⟩
      obtain ⟨yNew, hyNewN, sourceNew, targetNew⟩ := secondNew
      rw sourceOld at sourceNew
      have sameFirst := orderedPair.first with sourceNew
      rw sameFirst at hxOldM
      have irreflexive := membership.irreflexive with hxOldM
      contradiction
  . cases second with secondOldAfterNew | secondNewAfterNew
    . obtain (yNewFirst, hyNewFirst) := firstNew
      rcases hyNewFirst with ⟨hyNewFirstN, sourceNewFirst, targetNewFirst⟩
      obtain ⟨xOldSecond, hxOldSecondM, yOldSecond, hyOldSecondN, sourceOldSecond, targetOldSecond⟩ := secondOldAfterNew
      rw sourceOldSecond at sourceNewFirst
      have sameFirstReverse := orderedPair.first with sourceNewFirst
      rw sameFirstReverse at hxOldSecondM
      have irreflexiveReverse := membership.irreflexive with hxOldSecondM
      contradiction
    . obtain (yNew1, hyNew1) := firstNew
      rcases hyNew1 with ⟨hyNew1N, sourceNew1, targetNew1⟩
      obtain ⟨yNew2, hyNew2N, sourceNew2, targetNew2⟩ := secondNewAfterNew
      rw sourceNew1 at sourceNew2
      obtain (sameM, sameYNew) := orderedPair.injective with sourceNew2
      rw [targetNew1, targetNew2, sameYNew]
      rfl

theorem productStepMap.function {m : Nat} (n : Set)
  shows productStepMap(m, n) : succ(m) × n → (m × n) ⊎ n
proof
  constructor
  . exact productStepMap.relation at m, n
  . constructor
    . exact productStepMap.functional{m := m} at n
    . exact productStepMap.total{m := m} at n

theorem productStepMap.injective {m : Nat} (n : Set)
  shows InjectiveBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)
proof
  constructor
  . exact productStepMap.function{m := m} at n
  . intros u hu v hv q hq huq hvq
    have first := productStepMap.factors with huq
    have second := productStepMap.factors with hvq
    cases first with firstOld | firstNew
    . cases second with secondOld | secondNew
      . obtain (x1, hx1) := firstOld
        rcases hx1 with ⟨hx1M, y1, hy1N, source1, target1⟩
        obtain ⟨x2, hx2M, y2, hy2N, source2, target2⟩ := secondOld
        rw target1 at target2
        have samePair := inl.injective with target2
        rw source1
        rwa source2
      . obtain (xOld, hxOld) := firstOld
        rcases hxOld with ⟨hxOldM, yOld, hyOldN, sourceOld, targetOld⟩
        obtain ⟨yNew, hyNewN, sourceNew, targetNew⟩ := secondNew
        rw targetOld at targetNew
        have impossible := tags.disjoint with targetNew
        contradiction
    . cases second with secondOldAfterNew | secondNewAfterNew
      . obtain (yNewFirst, hyNewFirst) := firstNew
        rcases hyNewFirst with ⟨hyNewFirstN, sourceNewFirst, targetNewFirst⟩
        obtain ⟨xOldSecond, hxOldSecondM, yOldSecond, hyOldSecondN, sourceOldSecond, targetOldSecond⟩ := secondOldAfterNew
        rw targetOldSecond at targetNewFirst
        have impossibleReverse := tags.disjoint with targetNewFirst
        contradiction
      . obtain (yNew1, hyNew1) := firstNew
        rcases hyNew1 with ⟨hyNew1N, sourceNew1, targetNew1⟩
        obtain ⟨yNew2, hyNew2N, sourceNew2, targetNew2⟩ := secondNewAfterNew
        rw targetNew1 at targetNew2
        have sameY := inr.injective with targetNew2
        rw [sourceNew1, sourceNew2, sameY]
        rfl

theorem productStepMap.surjective {m : Nat} (n : Set)
  shows SurjectiveBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)
proof
  constructor
  . exact productStepMap.function{m := m} at n
  . intros q hq
    have targetShape := disjointSum.membership.forward with hq
    cases targetShape with old | newest
    . obtain (pairXY, hpairXY) := old
      rcases hpairXY with (pairMember, qShape)
      obtain ⟨pairBound, x, hxM, y, hyN, pairShape⟩ := product.membership.forward with pairMember
      witness (x, y)
      constructor
      . apply product.pair at x, y, succ(m), n
        . apply membership.successor_set{n := m}.backward at x
          left
          exact hxM
        . exact hyN
      . rw [qShape, pairShape]
        exact productStepMap.relates_old{m := m} at n, x, y
    . obtain (yNew, hyNew) := newest
      rcases hyNew with (hyNewN, qShapeNew)
      witness (m, yNew)
      constructor
      . apply product.pair at m, yNew, succ(m), n
        . apply membership.successor_set{n := m}.backward at m
          right
          rfl
        . exact hyNewN
      . rw qShapeNew
        exact productStepMap.relates_new{m := m} at n, yNew

theorem productStepMap.bijective {m : Nat} (n : Set)
  shows BijectiveBetween(productStepMap(m, n), succ(m) × n, (m × n) ⊎ n)
proof
  --! Split a successor rectangle into its old part and newest row.
  --| The tags make the two images disjoint without imposing an order on n.
  constructor
  . --! Each tagged output has one source pair
    exact productStepMap.injective{m := m} at n
  . --! Every old pair ∨ newest-row element is reached
    exact productStepMap.surjective{m := m} at n

-- Recursively assemble the concrete graph witnessing m × n ≃ m*n. At a
-- successor, productStepMap exposes the old rectangle plus one row, sumMap
-- transports the induction hypothesis, and natSumEquiv packs the two blocks
-- into the next native numeral.
def natProductEquiv (m n : Nat) → Set
  | zero, n => identity(0)
  | succ(m), n => compose(natSumEquiv(m * n, n), compose(sumMap(natProductEquiv(m, n), identity(n), m × n, n, m * n, n), productStepMap(m, n), succ(m) × n, (m × n) ⊎ n, (m * n) ⊎ n), succ(m) × n, (m * n) ⊎ n, m * n + n)

theorem BijectiveBetween.codomain_eq (f X Y Z : Set)
  requires h : BijectiveBetween(f, X, Y)
  requires hYZ : Y = Z
  shows BijectiveBetween(f, X, Z)
proof
  simp

theorem natProductEquiv.bijective (n m : Nat)
  shows BijectiveBetween(natProductEquiv(m, n), m × n, mul(m, n))
proof
  induction m
  | zero =>
    rw [natProductEquiv, mul, product.zero_left]
    exact identity.bijective
  | succ(k) using ih =>
    --! Decompose the successor rectangle.
    --| The old rectangle and newest row are separated by productStepMap.
    rw [natProductEquiv, mul]
    --! Transport the old block and the new row.
    have step := productStepMap.bijective{m := k} at n
    have identityN := identity.bijective at n
    have lifted := sumMap.bijective with ih, identityN
    have middle := compose.bijective with step, lifted
    --! Pack the two finite blocks into multiplication.
    apply BijectiveBetween.codomain_eq at compose(natSumEquiv(k * n, n), compose(sumMap(natProductEquiv(k, n), identity(n), k × n, n, k * n, n), productStepMap(k, n), succ(k) × n, (k × n) ⊎ n, (k * n) ⊎ n), succ(k) × n, (k * n) ⊎ n, k * n + n), succ(k) × n, k * n + n, n + k * n
    . apply compose.bijective at natSumEquiv(k * n, n), compose(sumMap(natProductEquiv(k, n), identity(n), k × n, n, k * n, n), productStepMap(k, n), succ(k) × n, (k × n) ⊎ n, (k * n) ⊎ n), succ(k) × n, (k * n) ⊎ n, k * n + n
      . exact middle
      . apply natSumEquiv.bijective at n, mul(k, n)
    . apply Grace.Core.Nat.Algebra.add.commutative at n, mul(k, n)

theorem Equipotent.nat_product (m n : Set)
  requires hm : Nat(m)
  requires hn : Nat(n)
  shows (m × n) ≃ mul(m, n)
proof
  witness natProductEquiv(m, n)
  exact natProductEquiv.bijective with hn, hm

theorem HasCardinality.product (A B m n : Set)
  requires hA : HasCardinality(A, m)
  requires hB : HasCardinality(B, n)
  shows HasCardinality(A × B, mul(m, n))
proof
  rcases hA with (hm, equipotentA)
  rcases hB with (hn, equipotentB)
  constructor
  . exact Grace.Core.Nat.Algebra.mul.closed at n, m
  . --! Lift the two cardinal witnesses coordinatewise.
    have lifted := Equipotent.product with equipotentA, equipotentB
    --! Identify the finite rectangle with native multiplication.
    have numeric := Equipotent.nat_product with hm, hn
    exact Equipotent.transitive with lifted, numeric

theorem Finite.product (A B : Set)
  requires finiteA : Finite(A)
  requires finiteB : Finite(B)
  shows Finite(A × B)
proof
  obtain (m, hA) := finiteA
  obtain (n, hB) := finiteB
  witness mul(m, n)
  exact HasCardinality.product with hA, hB

-- The canonical exchange of two Cartesian factors.
defunique swappedPair (A B p : Set) (q ∈ B × A) :=
  ∃ x ∈ A, ∃ y ∈ B, p = (x, y) ∧ q = (y, x)
requires pair : p ∈ A × B
proof
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair
  have output := product.pair with hy, hx
  refine ⟨(y, x), output, x, hx, y, hy, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨a, ha, b, hb, shapeU, valueU⟩ := first
  obtain ⟨c, hc, d, hd, shapeV, valueV⟩ := second
  have equal : (a, b) = (c, d) by cc
  have coordinates := orderedPair.injective with equal
  cc

defgraph productSwap (A B : Set) (p ∈ A × B) : B × A := swappedPair(A, B, p)
proof
  have selected := swappedPair.selected with member
  exact selected.left

theorem productSwap.pair (A B x y : Set)
  requires hx : x ∈ A
  requires hy : y ∈ B
  shows productSwap(A, B)((x, y)) = (y, x)
proof
  have pair := product.pair at x, y, A, B with *
  have selected := swappedPair.selected with pair
  obtain ⟨a, ha, b, hb, shape, output⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := productSwap.value with pair
  cc

theorem productSwap.involution (A B p : Set)
  requires pair : p ∈ A × B
  shows productSwap(B, A)(productSwap(A, B)(p)) = p
proof
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair
  have first := productSwap.pair with hx, hy
  have second := productSwap.pair with hy, hx
  cc

theorem productSwap.bijective (A B : Set)
  shows BijectiveBetween(productSwap(A, B), A × B, B × A)
proof
  have function := productSwap.function at A, B
  have reverse := productSwap.function at B, A
  constructor
  . unfold InjectiveBetween
    refine ⟨function, _⟩
    intros x hx y hy z hz edgeX edgeY
    have valueX := FunctionBetween.apply_value at productSwap(A, B), A × B, B × A, x, z with *
    have valueY := FunctionBetween.apply_value at productSwap(A, B), A × B, B × A, y, z with *
    have inverseX := productSwap.involution with hx
    have inverseY := productSwap.involution with hy
    cc
  . unfold SurjectiveBetween
    refine ⟨function, _⟩
    intros z hz
    have input := FunctionBetween.apply_closed at productSwap(B, A), B × A, A × B, z with *
    have inverse := productSwap.involution with hz
    have edge := FunctionBetween.relates_apply at productSwap(A, B), A × B, B × A, productSwap(B, A)(z) with *
    refine ⟨productSwap(B, A)(z), input, _⟩
    rwa inverse at edge