∀ (J : Type u_1),
  Function.LeftInverse
    (fun x =>
      match x with
      | none =>
        CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingParallelFamily.zero)
      | some none =>
        CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingParallelFamily.one)
      | some (some t) => CategoryTheory.Arrow.mk (CategoryTheory.Limits.WalkingParallelFamily.Hom.line t))
    fun f =>
    match f.left, f.right, f.hom with
    | CategoryTheory.Limits.WalkingParallelFamily.zero, .(CategoryTheory.Limits.WalkingParallelFamily.zero),
      CategoryTheory.Limits.WalkingParallelFamily.Hom.id
        .((CategoryTheory.Functor.id (CategoryTheory.Limits.WalkingParallelFamily J)).obj
            CategoryTheory.Limits.WalkingParallelFamily.zero) =>
      none
    | CategoryTheory.Limits.WalkingParallelFamily.one, .(CategoryTheory.Limits.WalkingParallelFamily.one),
      CategoryTheory.Limits.WalkingParallelFamily.Hom.id
        .((CategoryTheory.Functor.id (CategoryTheory.Limits.WalkingParallelFamily J)).obj
            CategoryTheory.Limits.WalkingParallelFamily.one) =>
      some none
    | CategoryTheory.Limits.WalkingParallelFamily.zero, CategoryTheory.Limits.WalkingParallelFamily.one,
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line t => some (some t)