-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun (X : Type u) ↦ X) Z),
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
              (a : (fun (X : Type u) ↦ X) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) ∨
      Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
              (a : (fun (X : Type u) ↦ X) Z) →
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
            x :
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
        (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1})
eX : { p : Z × PUnit.{u + 1} //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          p.1 :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } ≃
  { x : Z //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          x :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } :=
  {
    toFun :=
      fun
        (p :
          { p : Z × PUnit.{u + 1} //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  p.1 :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (x : Z) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              x :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (↑p : Z × PUnit.{u + 1}).1 ⋯,
    invFun :=
      fun
        (x :
          { x : Z //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  x :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (p : Z × PUnit.{u + 1}) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              p.1 :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (x.1, PUnit.unit) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
eY : { p : Z × PUnit.{u + 1} //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          p.1 :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } ≃
  { x : Z //
    Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
            (a : (fun (X : Type u) ↦ X) Z) →
              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          x :
        (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) } :=
  {
    toFun :=
      fun
        (p :
          { p : Z × PUnit.{u + 1} //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  p.1 :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (x : Z) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              x :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (↑p : Z × PUnit.{u + 1}).1 ⋯,
    invFun :=
      fun
        (x :
          { x : Z //
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  x :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }) ↦
      Subtype.mk (p := fun (p : Z × PUnit.{u + 1}) ↦
        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                (a : (fun (X : Type u) ↦ X) Z) →
                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              p.1 :
            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
          (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        (x.1, PUnit.unit) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
h₂ :
  ∀ (x : Z)
    (hx :
      Eq (α := (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
              (a : (fun (X : Type u) ↦ X) Z) → (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
            (x, PUnit.unit).1 :
          (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr) :
              (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
            (x, PUnit.unit).2 :
          (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))),
    TypeCat.Fun.toFun (X := Types.PullbackObj f (↾Sum.inr))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Z) (↾fun (p : Types.PullbackObj f (↾Sum.inr)) ↦ (↑p : Z × PUnit.{u + 1}).1)
            (↾fun (x : Z) ↦
              if h :
                  Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                          (a : (fun (X : Type u) ↦ X) Z) →
                            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        x :
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                    (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) then
                (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((pair (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))).obj
                            { as := WalkingPair.left })) →
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
                  ((eX.symm :
                        (a :
                            { x : Z //
                              (ConcreteCategory.hom f :
                                    (a : (fun (X : Type u) ↦ X) Z) →
                                      (fun (X : Type u) ↦ X)
                                        (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                                  x =
                                Sum.inl PUnit.unit }) →
                          { p : Z × PUnit.{u + 1} //
                            (ConcreteCategory.hom f :
                                  (a : (fun (X : Type u) ↦ X) Z) →
                                    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                                p.1 =
                              Sum.inl p.2 })
                      (Subtype.mk (p := fun (x : Z) ↦
                        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                                (a : (fun (X : Type u) ↦ X) Z) →
                                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                              x :
                            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                          (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                        x h) :
                    { p : Z × PUnit.{u + 1} //
                      Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                              (a : (fun (X : Type u) ↦ X) Z) →
                                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                            p.1 :
                          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) })
              else
                (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((pair (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))).obj
                            { as := WalkingPair.right })) →
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }))
                  ((eY.symm :
                        (a :
                            { x : Z //
                              (ConcreteCategory.hom f :
                                    (a : (fun (X : Type u) ↦ X) Z) →
                                      (fun (X : Type u) ↦ X)
                                        (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                                  x =
                                Sum.inr PUnit.unit }) →
                          { p : Z × PUnit.{u + 1} //
                            (ConcreteCategory.hom f :
                                  (a : (fun (X : Type u) ↦ X) Z) →
                                    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                                p.1 =
                              Sum.inr p.2 })
                      (Subtype.mk (p := fun (x : Z) ↦
                        Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                                (a : (fun (X : Type u) ↦ X) Z) →
                                  (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                              x :
                            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                          (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                        x ⋯) :
                    { p : Z × PUnit.{u + 1} //
                      Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                              (a : (fun (X : Type u) ↦ X) Z) →
                                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                            p.1 :
                          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) }))))
        (Subtype.mk (p := fun (p : Z × PUnit.{u + 1}) ↦
          Eq (α := (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u) ↦ X) Z) → (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                p.1 :
              (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr) :
                  (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                p.2 :
              (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1})))
          (x, PUnit.unit) hx) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr).toFun
        (Subtype.mk (p := fun (p : Z × PUnit.{u + 1}) ↦
          Eq (α := (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u) ↦ X) Z) → (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                p.1 :
              (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr) :
                  (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                p.2 :
              (fun (X : Type u) ↦ X) (PUnit.{u + 1} ⊕ PUnit.{u + 1})))
          (x, PUnit.unit) hx)
⊢ CategoryStruct.comp (Y := Z) (↾fun (p : Types.PullbackObj f (↾Sum.inr)) ↦ (↑p : Z × PUnit.{u + 1}).1)
      (↾fun (x : Z) ↦
        if h :
            Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                    (a : (fun (X : Type u) ↦ X) Z) →
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  x :
                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
              (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}) then
          (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((pair (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))).obj
                      { as := WalkingPair.left })) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }))
            ((eX.symm :
                  (a :
                      { x : Z //
                        (ConcreteCategory.hom f :
                              (a : (fun (X : Type u) ↦ X) Z) →
                                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                            x =
                          Sum.inl PUnit.unit }) →
                    { p : Z × PUnit.{u + 1} //
                      (ConcreteCategory.hom f :
                            (a : (fun (X : Type u) ↦ X) Z) →
                              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                          p.1 =
                        Sum.inl p.2 })
                (Subtype.mk (p := fun (x : Z) ↦
                  Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                          (a : (fun (X : Type u) ↦ X) Z) →
                            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        x :
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                    (Sum.inl PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                  x h) :
              { p : Z × PUnit.{u + 1} //
                Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                        (a : (fun (X : Type u) ↦ X) Z) →
                          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                      p.1 :
                    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  (Sum.inl p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) })
        else
          (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
              (a :
                  (fun (X : Type u) ↦ X)
                    ((pair (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))).obj
                      { as := WalkingPair.right })) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }))
            ((eY.symm :
                  (a :
                      { x : Z //
                        (ConcreteCategory.hom f :
                              (a : (fun (X : Type u) ↦ X) Z) →
                                (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                            x =
                          Sum.inr PUnit.unit }) →
                    { p : Z × PUnit.{u + 1} //
                      (ConcreteCategory.hom f :
                            (a : (fun (X : Type u) ↦ X) Z) →
                              (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                          p.1 =
                        Sum.inr p.2 })
                (Subtype.mk (p := fun (x : Z) ↦
                  Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                          (a : (fun (X : Type u) ↦ X) Z) →
                            (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                        x :
                      (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                    (Sum.inr PUnit.unit : PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                  x ⋯) :
              { p : Z × PUnit.{u + 1} //
                Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                        (a : (fun (X : Type u) ↦ X) Z) →
                          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                      p.1 :
                    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
                  (Sum.inr p.2 : PUnit.{u + 1} ⊕ PUnit.{u + 1}) })) =
    s.inr

Tactic:
ext ⟨⟨x, ⟨⟩⟩, hx⟩