-- 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 : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Eq (α := Set (↑Z : Type u))
    (Set.range (ι :=
      (↑(TopCat.of
            { p :
              (↑Z : Type u) ×
                (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                      { as := WalkingPair.left : Discrete WalkingPair }) :
                  Type u) //
              Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) f :
                      (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    p.1 :
                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (X :=
                          Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair })
                          (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                          (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair } ⟶
                              Functor.obj
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                { as := WalkingPair.left : Discrete WalkingPair }) :
                        C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair }) :
                            Type u),
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                      (a :
                          (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                { as := WalkingPair.left }) :
                            Type u)) →
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    p.2 :
                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X :=
            TopCat.of
              { p :
                (↑Z : Type u) ×
                  (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                        { as := WalkingPair.left : Discrete WalkingPair }) :
                    Type u) //
                Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) f :
                        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.1 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) (X :=
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.left : Discrete WalkingPair })
                            (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                            (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                Functor.obj
                                  (Functor.obj (Functor.const (Discrete WalkingPair))
                                    (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                          C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                              Type u),
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                        (a :
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.left }) :
                              Type u)) →
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.2 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
            (TopCat.pullbackFst f
              (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))) :
        (a :
            (↑(TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj { as := WalkingPair.left }) :
                        Type u) //
                    (ConcreteCategory.hom f :
                          (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.1 =
                      (ConcreteCategory.hom ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl :
                          (a :
                              (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                    { as := WalkingPair.left }) :
                                Type u)) →
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.2 }) :
              Type u)) →
          (↑Z : Type u)))
    (Set.preimage (β := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
      (Set.range Sum.inl))
h₂ :
  Eq (α := Set (↑Z : Type u))
    (Set.range (ι :=
      (↑(TopCat.of
            { p :
              (↑Z : Type u) ×
                (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                      { as := WalkingPair.right : Discrete WalkingPair }) :
                  Type u) //
              Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) f :
                      (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    p.1 :
                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (X :=
                          Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.right : Discrete WalkingPair })
                          (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                          (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.right : Discrete WalkingPair } ⟶
                              Functor.obj
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                { as := WalkingPair.right : Discrete WalkingPair }) :
                        C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.right : Discrete WalkingPair }) :
                            Type u),
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                      (a :
                          (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                { as := WalkingPair.right }) :
                            Type u)) →
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    p.2 :
                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X :=
            TopCat.of
              { p :
                (↑Z : Type u) ×
                  (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                        { as := WalkingPair.right : Discrete WalkingPair }) :
                    Type u) //
                Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) f :
                        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.1 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) (X :=
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.right : Discrete WalkingPair })
                            (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                            (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                Functor.obj
                                  (Functor.obj (Functor.const (Discrete WalkingPair))
                                    (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                          C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                              Type u),
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                        (a :
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.right }) :
                              Type u)) →
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.2 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
            (TopCat.pullbackFst f
              (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))) :
        (a :
            (↑(TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj { as := WalkingPair.right }) :
                        Type u) //
                    (ConcreteCategory.hom f :
                          (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.1 =
                      (ConcreteCategory.hom ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr :
                          (a :
                              (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                    { as := WalkingPair.right }) :
                                Type u)) →
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.2 }) :
              Type u)) →
          (↑Z : Type u)))
    (Set.preimage (β := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f) :
        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
      (Set.range Sum.inr))
refine_2 :
  IsOpen (X :=
    (↑(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair
                (TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u) //
                    Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) f :
                            (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.1 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) (X :=
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair })
                                (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                    Functor.obj
                                      (Functor.obj (Functor.const (Discrete WalkingPair))
                                        (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                      { as := WalkingPair.left : Discrete WalkingPair }) :
                              C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair }) :
                                  Type u),
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                            (a :
                                (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                      { as := WalkingPair.left }) :
                                  Type u)) →
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.2 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
                (TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.right : Discrete WalkingPair }) :
                        Type u) //
                    Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) f :
                            (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.1 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) (X :=
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair })
                                (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                    Functor.obj
                                      (Functor.obj (Functor.const (Discrete WalkingPair))
                                        (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                      { as := WalkingPair.right : Discrete WalkingPair }) :
                              C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair }) :
                                  Type u),
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                            (a :
                                (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                      { as := WalkingPair.right }) :
                                  Type u)) →
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.2 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
              (BinaryCofan.mk
                (TopCat.pullbackFst f
                  (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                (TopCat.pullbackFst f
                  (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))))
          { as := WalkingPair.right : Discrete WalkingPair }) :
      Type u))
    (Set.range (ι :=
      (↑(Functor.obj
            (pair
              (TopCat.of
                { p :
                  (↑Z : Type u) ×
                    (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                          { as := WalkingPair.left : Discrete WalkingPair }) :
                      Type u) //
                  Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) f :
                          (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.1 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) (X :=
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair })
                              (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                              (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                  Functor.obj
                                    (Functor.obj (Functor.const (Discrete WalkingPair))
                                      (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                    { as := WalkingPair.left : Discrete WalkingPair }) :
                            C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.left : Discrete WalkingPair }) :
                                Type u),
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                          (a :
                              (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                    { as := WalkingPair.left }) :
                                Type u)) →
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.2 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
              (TopCat.of
                { p :
                  (↑Z : Type u) ×
                    (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                          { as := WalkingPair.right : Discrete WalkingPair }) :
                      Type u) //
                  Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) f :
                          (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.1 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) (X :=
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.right : Discrete WalkingPair })
                              (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                              (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                  Functor.obj
                                    (Functor.obj (Functor.const (Discrete WalkingPair))
                                      (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                    { as := WalkingPair.right : Discrete WalkingPair }) :
                            C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.right : Discrete WalkingPair }) :
                                Type u),
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                          (a :
                              (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                    { as := WalkingPair.right }) :
                                Type u)) →
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.2 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
            { as := WalkingPair.right : Discrete WalkingPair }) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X :=
            Functor.obj
              (pair
                (TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u) //
                    Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) f :
                            (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.1 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) (X :=
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair })
                                (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                    Functor.obj
                                      (Functor.obj (Functor.const (Discrete WalkingPair))
                                        (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                      { as := WalkingPair.left : Discrete WalkingPair }) :
                              C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair }) :
                                  Type u),
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                            (a :
                                (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                      { as := WalkingPair.left }) :
                                  Type u)) →
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.2 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
                (TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.right : Discrete WalkingPair }) :
                        Type u) //
                    Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) f :
                            (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.1 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) (X :=
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair })
                                (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                    Functor.obj
                                      (Functor.obj (Functor.const (Discrete WalkingPair))
                                        (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                      { as := WalkingPair.right : Discrete WalkingPair }) :
                              C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair }) :
                                  Type u),
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                            (a :
                                (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                      { as := WalkingPair.right }) :
                                  Type u)) →
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.2 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
              { as := WalkingPair.right : Discrete WalkingPair })
            (Y :=
            Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F :=
                  pair
                    (TopCat.of
                      { p :
                        (↑Z : Type u) ×
                          (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair }) :
                            Type u) //
                        Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  TopCat.carrier) f :
                                (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.1 :
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                    (CC := TopCat.carrier) (X :=
                                    Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair })
                                    (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                      Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                        Functor.obj
                                          (Functor.obj (Functor.const (Discrete WalkingPair))
                                            (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                              ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                          { as := WalkingPair.left : Discrete WalkingPair }) :
                                  C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          { as := WalkingPair.left : Discrete WalkingPair }) :
                                      Type u),
                                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                                (a :
                                    (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                          { as := WalkingPair.left }) :
                                      Type u)) →
                                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.2 :
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
                    (TopCat.of
                      { p :
                        (↑Z : Type u) ×
                          (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.right : Discrete WalkingPair }) :
                            Type u) //
                        Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  TopCat.carrier) f :
                                (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.1 :
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                    (CC := TopCat.carrier) (X :=
                                    Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair })
                                    (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                      Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                        Functor.obj
                                          (Functor.obj (Functor.const (Discrete WalkingPair))
                                            (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                              ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                          { as := WalkingPair.right : Discrete WalkingPair }) :
                                  C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          { as := WalkingPair.right : Discrete WalkingPair }) :
                                      Type u),
                                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                                (a :
                                    (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                          { as := WalkingPair.right }) :
                                      Type u)) →
                                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.2 :
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
                  (BinaryCofan.mk
                    (TopCat.pullbackFst f
                      (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                    (TopCat.pullbackFst f
                      (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))))
              { as := WalkingPair.right : Discrete WalkingPair })
            (BinaryCofan.inr
              (BinaryCofan.mk
                (TopCat.pullbackFst f
                  (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                (TopCat.pullbackFst f
                  (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))))) :
        (a :
            (↑((pair
                      (TopCat.of
                        { p :
                          (↑Z : Type u) ×
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.left }) :
                              Type u) //
                          (ConcreteCategory.hom f :
                                (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.1 =
                            (ConcreteCategory.hom
                                  ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl :
                                (a :
                                    (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                          { as := WalkingPair.left }) :
                                      Type u)) →
                                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.2 })
                      (TopCat.of
                        { p :
                          (↑Z : Type u) ×
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.right }) :
                              Type u) //
                          (ConcreteCategory.hom f :
                                (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.1 =
                            (ConcreteCategory.hom
                                  ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr :
                                (a :
                                    (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                          { as := WalkingPair.right }) :
                                      Type u)) →
                                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                              p.2 })).obj
                  { as := WalkingPair.right }) :
              Type u)) →
          (↑(((Functor.const (Discrete WalkingPair)).obj
                    (BinaryCofan.mk
                        (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
                        (TopCat.pullbackFst f
                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).pt).obj
                { as := WalkingPair.right }) :
            Type u)))
⊢ IsOpenEmbedding (X :=
    (↑(Functor.obj
          (pair
            (TopCat.of
              { p :
                (↑Z : Type u) ×
                  (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                        { as := WalkingPair.left : Discrete WalkingPair }) :
                    Type u) //
                Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) f :
                        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.1 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) (X :=
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.left : Discrete WalkingPair })
                            (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                            (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                Functor.obj
                                  (Functor.obj (Functor.const (Discrete WalkingPair))
                                    (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                          C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                              Type u),
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                        (a :
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.left }) :
                              Type u)) →
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.2 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
            (TopCat.of
              { p :
                (↑Z : Type u) ×
                  (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                        { as := WalkingPair.right : Discrete WalkingPair }) :
                    Type u) //
                Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) f :
                        (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.1 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                  (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) (X :=
                            Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.right : Discrete WalkingPair })
                            (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                            (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                Functor.obj
                                  (Functor.obj (Functor.const (Discrete WalkingPair))
                                    (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                          C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                              Type u),
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                        (a :
                            (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                  { as := WalkingPair.right }) :
                              Type u)) →
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      p.2 :
                    (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
          { as := WalkingPair.right : Discrete WalkingPair }) :
      Type u))
    (Y :=
    (↑(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F :=
              pair
                (TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u) //
                    Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) f :
                            (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.1 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) (X :=
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.left : Discrete WalkingPair })
                                (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                    Functor.obj
                                      (Functor.obj (Functor.const (Discrete WalkingPair))
                                        (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                      { as := WalkingPair.left : Discrete WalkingPair }) :
                              C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.left : Discrete WalkingPair }) :
                                  Type u),
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                            (a :
                                (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                      { as := WalkingPair.left }) :
                                  Type u)) →
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.2 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
                (TopCat.of
                  { p :
                    (↑Z : Type u) ×
                      (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                            { as := WalkingPair.right : Discrete WalkingPair }) :
                        Type u) //
                    Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) f :
                            (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.1 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) (X :=
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                  { as := WalkingPair.right : Discrete WalkingPair })
                                (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                    Functor.obj
                                      (Functor.obj (Functor.const (Discrete WalkingPair))
                                        (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                      { as := WalkingPair.right : Discrete WalkingPair }) :
                              C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                      { as := WalkingPair.right : Discrete WalkingPair }) :
                                  Type u),
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                            (a :
                                (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                      { as := WalkingPair.right }) :
                                  Type u)) →
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                          p.2 :
                        (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
              (BinaryCofan.mk
                (TopCat.pullbackFst f
                  (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                (TopCat.pullbackFst f
                  (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))))
          { as := WalkingPair.right : Discrete WalkingPair }) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X :=
          Functor.obj
            (pair
              (TopCat.of
                { p :
                  (↑Z : Type u) ×
                    (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                          { as := WalkingPair.left : Discrete WalkingPair }) :
                      Type u) //
                  Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) f :
                          (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.1 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) (X :=
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.left : Discrete WalkingPair })
                              (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                              (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                  Functor.obj
                                    (Functor.obj (Functor.const (Discrete WalkingPair))
                                      (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                    { as := WalkingPair.left : Discrete WalkingPair }) :
                            C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.left : Discrete WalkingPair }) :
                                Type u),
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                          (a :
                              (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                    { as := WalkingPair.left }) :
                                Type u)) →
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.2 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
              (TopCat.of
                { p :
                  (↑Z : Type u) ×
                    (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                          { as := WalkingPair.right : Discrete WalkingPair }) :
                      Type u) //
                  Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            TopCat.carrier) f :
                          (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.1 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              TopCat.carrier) (X :=
                              Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                { as := WalkingPair.right : Discrete WalkingPair })
                              (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                              (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                  Functor.obj
                                    (Functor.obj (Functor.const (Discrete WalkingPair))
                                      (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                    { as := WalkingPair.right : Discrete WalkingPair }) :
                            C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.right : Discrete WalkingPair }) :
                                Type u),
                              (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                          (a :
                              (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                    { as := WalkingPair.right }) :
                                Type u)) →
                            (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        p.2 :
                      (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
            { as := WalkingPair.right : Discrete WalkingPair })
          (Y :=
          Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F :=
                pair
                  (TopCat.of
                    { p :
                      (↑Z : Type u) ×
                        (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                          Type u) //
                      Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) f :
                              (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.1 :
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  TopCat.carrier) (X :=
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.left : Discrete WalkingPair })
                                  (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                  (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                    Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        { as := WalkingPair.left : Discrete WalkingPair } ⟶
                                      Functor.obj
                                        (Functor.obj (Functor.const (Discrete WalkingPair))
                                          (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                            ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                        { as := WalkingPair.left : Discrete WalkingPair }) :
                                C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        { as := WalkingPair.left : Discrete WalkingPair }) :
                                    Type u),
                                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                              (a :
                                  (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                        { as := WalkingPair.left }) :
                                    Type u)) →
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.2 :
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) })
                  (TopCat.of
                    { p :
                      (↑Z : Type u) ×
                        (↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                              { as := WalkingPair.right : Discrete WalkingPair }) :
                          Type u) //
                      Eq (α := (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                TopCat.carrier) f :
                              (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.1 :
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                        (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                  TopCat.carrier) (X :=
                                  Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                    { as := WalkingPair.right : Discrete WalkingPair })
                                  (Y := TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1}))
                                  (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) :
                                    Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        { as := WalkingPair.right : Discrete WalkingPair } ⟶
                                      Functor.obj
                                        (Functor.obj (Functor.const (Discrete WalkingPair))
                                          (Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                            ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                                        { as := WalkingPair.right : Discrete WalkingPair }) :
                                C((↑(Functor.obj (pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
                                        { as := WalkingPair.right : Discrete WalkingPair }) :
                                    Type u),
                                  (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))) :
                              (a :
                                  (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                        { as := WalkingPair.right }) :
                                    Type u)) →
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.2 :
                          (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u)) }))
                (BinaryCofan.mk
                  (TopCat.pullbackFst f
                    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
                  (TopCat.pullbackFst f
                    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))))))
            { as := WalkingPair.right : Discrete WalkingPair })
          (BinaryCofan.inr
            (BinaryCofan.mk
              (TopCat.pullbackFst f (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))
              (TopCat.pullbackFst f
                (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))))))) :
      (a :
          (↑((pair
                    (TopCat.of
                      { p :
                        (↑Z : Type u) ×
                          (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                { as := WalkingPair.left }) :
                            Type u) //
                        (ConcreteCategory.hom f :
                              (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.1 =
                          (ConcreteCategory.hom ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl :
                              (a :
                                  (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                        { as := WalkingPair.left }) :
                                    Type u)) →
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.2 })
                    (TopCat.of
                      { p :
                        (↑Z : Type u) ×
                          (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                { as := WalkingPair.right }) :
                            Type u) //
                        (ConcreteCategory.hom f :
                              (a : (↑Z : Type u)) → (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.1 =
                          (ConcreteCategory.hom ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr :
                              (a :
                                  (↑((pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1})).obj
                                        { as := WalkingPair.right }) :
                                    Type u)) →
                                (↑(TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) : Type u))
                            p.2 })).obj
                { as := WalkingPair.right }) :
            Type u)) →
        (↑(((Functor.const (Discrete WalkingPair)).obj
                  (BinaryCofan.mk
                      (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
                      (TopCat.pullbackFst f
                        ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).pt).obj
              { as := WalkingPair.right }) :
          Type u))

Tactic:
refine ⟨(Homeomorph.prodPUnit Z).isEmbedding.comp .subtypeVal, ?_⟩