∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.map h =
    match X, Y, h with
    | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) =>
      CategoryTheory.CategoryStruct.id
        (match x with
        | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingParallelFamily.zero
        | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingParallelFamily.one)
    | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one),
      CategoryTheory.Limits.WalkingParallelPairHom.left =>
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true }
    | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one),
      CategoryTheory.Limits.WalkingParallelPairHom.right =>
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false }