∀ (j : CategoryTheory.Limits.WalkingPair),
  (fun x =>
        match x with
        | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Limits.WalkingPair.right
        | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Limits.WalkingPair.left)
      ((fun x =>
          match x with
          | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Limits.WalkingPair.right
          | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Limits.WalkingPair.left)
        j) =
    j