-- Module: Mathlib.Topology.Category.TopCat.Limits.Konig
Goal:
J : Type u
inst : SmallCategory J
F : J ⥤ TopCat
intro intro₁ :
  ∀ (A B : FiniteDiagram J),
    ∃ (z : FiniteDiagram J),
      Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            A)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z) ∧
        Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            B)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z)
intro₂ intro₃ :
  ∀ (A B : FiniteDiagram J),
    ∃ (z : FiniteDiagram J),
      Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            A)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z) ∧
        Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            B)
          ((fun (G : FiniteDiagram J) ↦
              partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
            z)
refine_1 :
  ∀ (A B : FiniteDiagram J),
    let ιA :
      FiniteDiagramArrow (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) →
        FiniteDiagramArrow
          (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) :=
      fun (f : FiniteDiagramArrow (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) ↦
      PSigma.mk (β := fun (X : J) ↦
        (Y : J) ×'
          (_ :
            X ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (X ⟶ Y))
        (f.fst (β := fun (X : J) ↦
          (Y : J) ×'
            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)))
        (PSigma.mk (β := fun (Y : J) ↦
          (_ :
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                Y))
          (f.snd (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
            (β := fun (Y : J) ↦
            (_ :
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                (f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  Y)))
          (PSigma.mk (β :=
            fun
              (x :
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                  A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
            (_ :
              f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y))))
            ⋯
            (PSigma.mk (β :=
              fun
                (x :
                  f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)))
              ⋯
              (f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).snd
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)).snd
                    (β :=
                    fun
                      (x :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                    (_ :
                      f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)) ∈
                        A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)))).snd
                (β :=
                fun
                  (x :
                    f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  f.snd (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                    (β := fun (Y : J) ↦
                    (_ :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                          Y)))))));
    let ιB :
      FiniteDiagramArrow (B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) →
        FiniteDiagramArrow
          (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) :=
      fun (f : FiniteDiagramArrow (B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) ↦
      PSigma.mk (β := fun (X : J) ↦
        (Y : J) ×'
          (_ :
            X ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (X ⟶ Y))
        (f.fst (β := fun (X : J) ↦
          (Y : J) ×'
            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)))
        (PSigma.mk (β := fun (Y : J) ↦
          (_ :
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                Y))
          (f.snd (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
            (β := fun (Y : J) ↦
            (_ :
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                (f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  Y)))
          (PSigma.mk (β :=
            fun
              (x :
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                  A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
            (_ :
              f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y))))
            ⋯
            (PSigma.mk (β :=
              fun
                (x :
                  f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)))
              ⋯
              (f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).snd
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)).snd
                    (β :=
                    fun
                      (x :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                    (_ :
                      f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)) ∈
                        B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)))).snd
                (β :=
                fun
                  (x :
                    f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  f.snd (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                    (β := fun (Y : J) ↦
                    (_ :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                          Y)))))));
    Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
      ((fun (G : FiniteDiagram J) ↦ partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        A)
      ((fun (G : FiniteDiagram J) ↦ partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        (Sigma.mk (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))
          (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))
          (Finset.image ιA (A.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ⊔
            Finset.image ιB (B.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))))
refine_2 refine_2₁ :
  ∀ (A B : FiniteDiagram J),
    let ιA :
      FiniteDiagramArrow (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) →
        FiniteDiagramArrow
          (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) :=
      fun (f : FiniteDiagramArrow (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) ↦
      PSigma.mk (β := fun (X : J) ↦
        (Y : J) ×'
          (_ :
            X ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (X ⟶ Y))
        (f.fst (β := fun (X : J) ↦
          (Y : J) ×'
            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)))
        (PSigma.mk (β := fun (Y : J) ↦
          (_ :
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                Y))
          (f.snd (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
            (β := fun (Y : J) ↦
            (_ :
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                (f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  Y)))
          (PSigma.mk (β :=
            fun
              (x :
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                  A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
            (_ :
              f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y))))
            ⋯
            (PSigma.mk (β :=
              fun
                (x :
                  f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)))
              ⋯
              (f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).snd
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)).snd
                    (β :=
                    fun
                      (x :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                    (_ :
                      f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)) ∈
                        A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)))).snd
                (β :=
                fun
                  (x :
                    f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)) ∈
                      A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  f.snd (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                    (β := fun (Y : J) ↦
                    (_ :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                          Y)))))));
    let ιB :
      FiniteDiagramArrow (B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) →
        FiniteDiagramArrow
          (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) :=
      fun (f : FiniteDiagramArrow (B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))) ↦
      PSigma.mk (β := fun (X : J) ↦
        (Y : J) ×'
          (_ :
            X ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (X ⟶ Y))
        (f.fst (β := fun (X : J) ↦
          (Y : J) ×'
            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)))
        (PSigma.mk (β := fun (Y : J) ↦
          (_ :
            f.fst (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
              A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
            (_ :
              Y ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                Y))
          (f.snd (β := fun (X : J) ↦
                (Y : J) ×'
                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
            (β := fun (Y : J) ↦
            (_ :
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                (f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  Y)))
          (PSigma.mk (β :=
            fun
              (x :
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                  A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                    B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
            (_ :
              f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)) ∈
                A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                  B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
              (f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y))))
            ⋯
            (PSigma.mk (β :=
              fun
                (x :
                  f.snd (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                      (β := fun (Y : J) ↦
                      (_ :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ⟶
                            Y)) ∈
                    A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
              f.fst (β := fun (X : J) ↦
                  (Y : J) ×'
                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                f.snd (β := fun (X : J) ↦
                      (Y : J) ×'
                        (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                  (β := fun (Y : J) ↦
                  (_ :
                    f.fst (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        Y)))
              ⋯
              (f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).snd
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)).snd
                    (β :=
                    fun
                      (x :
                        f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                          B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                    (_ :
                      f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)) ∈
                        B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                        f.snd (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)).fst
                          (β := fun (Y : J) ↦
                          (_ :
                            f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ∈
                              B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (f.fst (β := fun (X : J) ↦
                                  (Y : J) ×'
                                    (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                        (X ⟶ Y)) ⟶
                                Y)))).snd
                (β :=
                fun
                  (x :
                    f.snd (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (X ⟶ Y)).fst
                        (β := fun (Y : J) ↦
                        (_ :
                          f.fst (β := fun (X : J) ↦
                              (Y : J) ×'
                                (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                  (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (X ⟶ Y)) ∈
                            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                          (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (f.fst (β := fun (X : J) ↦
                                (Y : J) ×'
                                  (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                    (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                      (X ⟶ Y)) ⟶
                              Y)) ∈
                      B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ↦
                f.fst (β := fun (X : J) ↦
                    (Y : J) ×'
                      (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                  f.snd (β := fun (X : J) ↦
                        (Y : J) ×'
                          (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                            (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)).fst
                    (β := fun (Y : J) ↦
                    (_ :
                      f.fst (β := fun (X : J) ↦
                          (Y : J) ×'
                            (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                              (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ∈
                        B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                      (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                        (f.fst (β := fun (X : J) ↦
                            (Y : J) ×'
                              (_ : X ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×'
                                (_ : Y ∈ B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ×' (X ⟶ Y)) ⟶
                          Y)))))));
    Superset (α := Set ((j : J) → (↑(F.obj j) : Type v)))
      ((fun (G : FiniteDiagram J) ↦ partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        B)
      ((fun (G : FiniteDiagram J) ↦ partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))
        (Sigma.mk (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))
          (A.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)) ⊔
            B.fst (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))
          (Finset.image ιA (A.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))) ⊔
            Finset.image ιB (B.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G))))))
⊢ Directed (α := Set ((j : J) → (↑(F.obj j) : Type v))) Superset fun (G : FiniteDiagram J) ↦
    partialSections F (G.snd (β := fun (G : Finset J) ↦ Finset (FiniteDiagramArrow G)))

Tactic:
classical
  intro A B
  let ιA : FiniteDiagramArrow A.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
    ⟨f.1, f.2.1, Finset.mem_union_left _ f.2.2.1, Finset.mem_union_left _ f.2.2.2.1, f.2.2.2.2⟩
  let ιB : FiniteDiagramArrow B.1 → FiniteDiagramArrow (A.1 ⊔ B.1) := fun f =>
    ⟨f.1, f.2.1, Finset.mem_union_right _ f.2.2.1, Finset.mem_union_right _ f.2.2.2.1, f.2.2.2.2⟩
  refine ⟨⟨A.1 ⊔ B.1, A.2.image ιA ⊔ B.2.image ιB⟩, ?_, ?_⟩
  · rintro u hu f hf
    have : ιA f ∈ A.2.image ιA ⊔ B.2.image ιB := by
      apply Finset.mem_union_left
      rw [Finset.mem_image]
      exact ⟨f, hf, rfl⟩
    exact hu this
  · rintro u hu f hf
    have : ιB f ∈ A.2.image ιA ⊔ B.2.image ιB := by
      apply Finset.mem_union_right
      rw [Finset.mem_image]
      exact ⟨f, hf, rfl⟩
    exact hu this