[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ (fun f =>
        { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
          map_fst := (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
          map_snd :=
            (_ :
              (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                  (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                  (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
      ((fun f =>
          { toFun := f.toFun ∘ some,
            map_point :=
              (_ :
                Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                  (TwoP.toBipointed Y).toProd.fst) })
        f) =
    f
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
            map_fst :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                  (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                    (TwoP.toBipointed Y).toProd.fst) })
          f)).toFun =
    f.toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
x : (TwoP.toBipointed (pointedToTwoPFst.obj X)).X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
            map_fst :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                  (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                    (TwoP.toBipointed Y).toProd.fst) })
          f))
      x =
    Bipointed.Hom.toFun f x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
            map_fst :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                  (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                    (TwoP.toBipointed Y).toProd.fst) })
          f))
      none =
    Bipointed.Hom.toFun f none
case toFun.h.some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
            map_fst :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                  (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                    (TwoP.toBipointed Y).toProd.fst) })
          f))
      (some val✝) =
    Bipointed.Hom.toFun f (some val✝)
[PROOFSTEP]
exact f.map_snd.symm
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
            map_fst :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                  (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                    (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                    (TwoP.toBipointed Y).toProd.fst) })
          f))
      (some val✝) =
    Bipointed.Hom.toFun f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ ↑((fun X Y =>
              {
                toFun := fun f =>
                  { toFun := f.toFun ∘ some,
                    map_point :=
                      (_ :
                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                          (TwoP.toBipointed Y).toProd.fst) },
                invFun := fun f =>
                  { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                    map_fst :=
                      (_ :
                        Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                    map_snd :=
                      (_ :
                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                left_inv :=
                  (_ :
                    ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                      (fun f =>
                            { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                              map_fst :=
                                (_ :
                                  Pointed.Hom.toFun f X.point =
                                    ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                              map_snd :=
                                (_ :
                                  (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                      (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                      (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                          ((fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                      (TwoP.toBipointed Y).toProd.fst) })
                            f) =
                        f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                      (fun f =>
                            { toFun := f.toFun ∘ some,
                              map_point :=
                                (_ :
                                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                    (TwoP.toBipointed Y).toProd.fst) })
                          ((fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                map_fst :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                            f) =
                        f) })
            X'✝ Y✝).symm
      (f ≫ g) =
    pointedToTwoPFst.map f ≫
      ↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                            (TwoP.toBipointed Y).toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                      map_fst :=
                        (_ :
                          Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                map_fst :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                      (TwoP.toBipointed Y).toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              f) =
                          f) })
              X✝ Y✝).symm
        g
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                            (TwoP.toBipointed Y).toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                      map_fst :=
                        (_ :
                          Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                map_fst :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                      (TwoP.toBipointed Y).toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g)).toFun =
    (pointedToTwoPFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                              (TwoP.toBipointed Y).toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                        map_fst :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                              (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                          (TwoP.toBipointed Y).toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                    map_fst :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g).toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
x : (TwoP.toBipointed (pointedToTwoPFst.obj X'✝)).X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                            (TwoP.toBipointed Y).toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                      map_fst :=
                        (_ :
                          Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                map_fst :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                      (TwoP.toBipointed Y).toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      x =
    Bipointed.Hom.toFun
      (pointedToTwoPFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                              (TwoP.toBipointed Y).toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                        map_fst :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                              (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                          (TwoP.toBipointed Y).toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                    map_fst :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                            (TwoP.toBipointed Y).toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                      map_fst :=
                        (_ :
                          Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                map_fst :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                      (TwoP.toBipointed Y).toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      none =
    Bipointed.Hom.toFun
      (pointedToTwoPFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                              (TwoP.toBipointed Y).toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                        map_fst :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                              (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                          (TwoP.toBipointed Y).toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                    map_fst :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      none
[PROOFSTEP]
rfl
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
val✝ : X'✝.X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                            (TwoP.toBipointed Y).toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                      map_fst :=
                        (_ :
                          Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                              (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                map_fst :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                      (TwoP.toBipointed Y).toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      (some val✝) =
    Bipointed.Hom.toFun
      (pointedToTwoPFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                              (TwoP.toBipointed Y).toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                        map_fst :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                              (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                  map_fst :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                          (TwoP.toBipointed Y).toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.fst =
                                        (TwoP.toBipointed Y).toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.snd f.toFun,
                                    map_fst :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd =
                                          (fun o => Option.elim o Y.toTwoPointing.snd f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPFst.obj X)).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (fun f =>
        { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
          map_fst :=
            (_ :
              (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                  (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                  (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
          map_snd :=
            (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
      ((fun f =>
          { toFun := f.toFun ∘ some,
            map_point :=
              (_ :
                Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                  (TwoP.toBipointed Y).toProd.snd) })
        f) =
    f
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                  (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
            map_snd :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                    (TwoP.toBipointed Y).toProd.snd) })
          f)).toFun =
    f.toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
x : (TwoP.toBipointed (pointedToTwoPSnd.obj X)).X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                  (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
            map_snd :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                    (TwoP.toBipointed Y).toProd.snd) })
          f))
      x =
    Bipointed.Hom.toFun f x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                  (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
            map_snd :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                    (TwoP.toBipointed Y).toProd.snd) })
          f))
      none =
    Bipointed.Hom.toFun f none
case toFun.h.some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                  (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
            map_snd :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                    (TwoP.toBipointed Y).toProd.snd) })
          f))
      (some val✝) =
    Bipointed.Hom.toFun f (some val✝)
[PROOFSTEP]
exact f.map_fst.symm
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                  (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                    (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
            map_snd :=
              (_ : Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point :=
                (_ :
                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                    (TwoP.toBipointed Y).toProd.snd) })
          f))
      (some val✝) =
    Bipointed.Hom.toFun f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ ↑((fun X Y =>
              {
                toFun := fun f =>
                  { toFun := f.toFun ∘ some,
                    map_point :=
                      (_ :
                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                          (TwoP.toBipointed Y).toProd.snd) },
                invFun := fun f =>
                  { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                    map_fst :=
                      (_ :
                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                    map_snd :=
                      (_ :
                        Pointed.Hom.toFun f X.point = ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                left_inv :=
                  (_ :
                    ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                      (fun f =>
                            { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                              map_fst :=
                                (_ :
                                  (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                      (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                      (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                              map_snd :=
                                (_ :
                                  Pointed.Hom.toFun f X.point =
                                    ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                          ((fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                      (TwoP.toBipointed Y).toProd.snd) })
                            f) =
                        f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                      (fun f =>
                            { toFun := f.toFun ∘ some,
                              map_point :=
                                (_ :
                                  Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                    (TwoP.toBipointed Y).toProd.snd) })
                          ((fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                map_snd :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                            f) =
                        f) })
            X'✝ Y✝).symm
      (f ≫ g) =
    pointedToTwoPSnd.map f ≫
      ↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                            (TwoP.toBipointed Y).toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                      map_snd :=
                        (_ :
                          Pointed.Hom.toFun f X.point =
                            ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                map_snd :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                      (TwoP.toBipointed Y).toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              f) =
                          f) })
              X✝ Y✝).symm
        g
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                            (TwoP.toBipointed Y).toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                      map_snd :=
                        (_ :
                          Pointed.Hom.toFun f X.point =
                            ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                map_snd :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                      (TwoP.toBipointed Y).toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g)).toFun =
    (pointedToTwoPSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                              (TwoP.toBipointed Y).toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                              (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                        map_snd :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                          (TwoP.toBipointed Y).toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                    map_snd :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g).toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
x : (TwoP.toBipointed (pointedToTwoPSnd.obj X'✝)).X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                            (TwoP.toBipointed Y).toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                      map_snd :=
                        (_ :
                          Pointed.Hom.toFun f X.point =
                            ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                map_snd :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                      (TwoP.toBipointed Y).toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      x =
    Bipointed.Hom.toFun
      (pointedToTwoPSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                              (TwoP.toBipointed Y).toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                              (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                        map_snd :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                          (TwoP.toBipointed Y).toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                    map_snd :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                            (TwoP.toBipointed Y).toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                      map_snd :=
                        (_ :
                          Pointed.Hom.toFun f X.point =
                            ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                map_snd :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                      (TwoP.toBipointed Y).toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      none =
    Bipointed.Hom.toFun
      (pointedToTwoPSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                              (TwoP.toBipointed Y).toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                              (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                        map_snd :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                          (TwoP.toBipointed Y).toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                    map_snd :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      none
[PROOFSTEP]
rfl
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
val✝ : X'✝.X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ :
                          Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                            (TwoP.toBipointed Y).toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                              (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                      map_snd :=
                        (_ :
                          Pointed.Hom.toFun f X.point =
                            ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                        (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                map_snd :=
                                  (_ :
                                    Pointed.Hom.toFun f X.point =
                                      ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ :
                                    Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                      (TwoP.toBipointed Y).toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      (some val✝) =
    Bipointed.Hom.toFun
      (pointedToTwoPSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ :
                            Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                              (TwoP.toBipointed Y).toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                              (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                        map_snd :=
                          (_ :
                            Pointed.Hom.toFun f X.point =
                              ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToTwoPSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                          (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                  map_snd :=
                                    (_ :
                                      Pointed.Hom.toFun f X.point =
                                        ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                          (TwoP.toBipointed Y).toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.snd =
                                        (TwoP.toBipointed Y).toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toTwoPointing.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst =
                                          (fun o => Option.elim o Y.toTwoPointing.fst f.toFun)
                                            (TwoP.toBipointed (pointedToTwoPSnd.obj X)).toProd.fst),
                                    map_snd :=
                                      (_ :
                                        Pointed.Hom.toFun f X.point =
                                          ((forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      (some val✝)
[PROOFSTEP]
rfl
