-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst : Epi π
this_1 :
  CompactSpace
    (↑(S'
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞}))) :
      Type)
S'π : (n :
    (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)) →
  LightProfinite.of
      (↑(S'
            (⇑(ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type),
                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)))
                  (CC :=
                  fun
                    (X :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type))
                  π) :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    T) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (S ⊗ ℕ∪{∞}))) :
        Type) ⟶
    LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun
      (n :
        (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type)) ↦
    {
      hom :=
        TopCat.ofHom
          {
            toFun :=
              fun
                (x :
                  (↑(S'
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π) :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                T) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (S ⊗ ℕ∪{∞}))) :
                    Type)) ↦
              (↑x :
                  (x : OnePoint ℕ) →
                    (↑(Prod.snd ∘
                            (⇑(ConcreteCategory.hom π) :
                              (a :
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    T) →
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (S ⊗ ℕ∪{∞})) ⁻¹'
                          {x}) :
                      Type))
                n,
            continuous_toFun := ⋯ } }
y' : LightProfinite.of
    (↑(S'
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞}))) :
      Type) ⟶
  S :=
  ConcreteCategory.ofHom (FC :=
    fun
      (x1 x2 :
        CompHausLike fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type),
      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)))
    (CC :=
    fun
      (X :
        CompHausLike fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type))
    {
      toFun :=
        y
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞})),
      continuous_toFun := ⋯ }
π' : pullback (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
    (y' ▷ ℕ∪{∞}) ⟶
  tensorObj (𝒞 :=
    CompHausLike.category fun (X : TopCat.{0}) ↦
      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
    (LightProfinite.of
      (↑(S'
            (⇑(ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type),
                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)))
                  (CC :=
                  fun
                    (X :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type))
                  π) :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    T) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (S ⊗ ℕ∪{∞}))) :
        Type))
    ℕ∪{∞} :=
  pullback.snd (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
    π (y' ▷ ℕ∪{∞})
σ' : (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
    Type) →
  (↑((LightProfinite.of
              (↑(S'
                    (⇑(ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type),
                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type)))
                          (CC :=
                          fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                          π) :
                      (a :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            T) →
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          (S ⊗ ℕ∪{∞}))) :
                Type)).toTop
          (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type) →
    (↑((pullback (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})).toTop
          (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type) :=
  fun
      (n :
        (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type)) ↦
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type),
            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type))
          (Y :=
          pullback (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞}))
          (pullback.lift (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})
            (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
            (lift
              (𝟙
                (LightProfinite.of
                  (↑(S'
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π) :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                T) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (S ⊗ ℕ∪{∞}))) :
                    Type)))
              (CompHausLike.const (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                (LightProfinite.of
                  (↑(S'
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π) :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                T) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (S ⊗ ℕ∪{∞}))) :
                    Type))
                n))
            ⋯)) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑X.toTop : Type))
            (LightProfinite.of
              (↑(S'
                    (⇑(ConcreteCategory.hom π) :
                      (a :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            T) →
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          (S ⊗ ℕ∪{∞}))) :
                Type))) →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
            (↑X.toTop : Type))
          (pullback π (y' ▷ ℕ∪{∞})))
hσ :
  ∀
    (x :
      (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type))
    (s :
      (↑((LightProfinite.of
                (↑(S'
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π) :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              T) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (S ⊗ ℕ∪{∞}))) :
                  Type)).toTop
            (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)),
    ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type),
                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
              π' :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (pullback π (y' ▷ ℕ∪{∞}))) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (LightProfinite.of
                    (↑(S'
                          (⇑(ConcreteCategory.hom π) :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  T) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (S ⊗ ℕ∪{∞}))) :
                      Type) ⊗
                  ℕ∪{∞}))
          (σ' x s)).1 =
      s
hσ' :
  ∀
    (x :
      (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type))
    (s :
      (↑((LightProfinite.of
                (↑(S'
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π) :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              T) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (S ⊗ ℕ∪{∞}))) :
                  Type)).toTop
            (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)),
    ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type),
                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                Type))
              π' :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (pullback π (y' ▷ ℕ∪{∞}))) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (LightProfinite.of
                    (↑(S'
                          (⇑(ConcreteCategory.hom π) :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  T) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (S ⊗ ℕ∪{∞}))) :
                      Type) ⊗
                  ℕ∪{∞}))
          (σ' x s)).2 =
      x
this :
  CompactSpace
    (↑(fibres
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π') :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (pullback π (y' ▷ ℕ∪{∞}))) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (LightProfinite.of
                    (↑(S'
                          (⇑(ConcreteCategory.hom π) :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  T) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (S ⊗ ℕ∪{∞}))) :
                      Type) ⊗
                  ℕ∪{∞}))
          σ') :
      Type)
refine_1 :
  Epi (X :=
    LightProfinite.of
      (↑(fibres
            (⇑(ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type),
                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type)))
                  (CC :=
                  fun
                    (X :
                      CompHausLike fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type))
                  π') :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    (pullback π (y' ▷ ℕ∪{∞}))) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  (LightProfinite.of
                      (↑(S'
                            (⇑(ConcreteCategory.hom π) :
                              (a :
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    T) →
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (S ⊗ ℕ∪{∞}))) :
                        Type) ⊗
                    ℕ∪{∞}))
            σ') :
        Type))
    ({
        hom :=
          TopCat.ofHom
            {
              toFun :=
                Subtype.val (p :=
                  fun
                    (x :
                      (fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                        (pullback (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞}))) ↦
                  x ∈
                    fibres
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π') :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (pullback π (y' ▷ ℕ∪{∞}))) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (LightProfinite.of
                                (↑(S'
                                      (⇑(ConcreteCategory.hom π) :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              T) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (S ⊗ ℕ∪{∞}))) :
                                  Type) ⊗
                              ℕ∪{∞}))
                      σ'),
              continuous_toFun := ⋯ } } ≫
      π')
refine_2 : Epi y'
refine_3 :
  Eq (α :=
    LightProfinite.of
        (↑(fibres
              (⇑(ConcreteCategory.hom (FC :=
                    fun
                      (x1 x2 :
                        CompHausLike fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                        Type),
                      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                        Type)))
                    (CC :=
                    fun
                      (X :
                        CompHausLike fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type))
                    π') :
                (a :
                    (fun
                          (X :
                            CompHausLike fun (X : TopCat) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                        (↑X.toTop : Type))
                      (pullback π (y' ▷ ℕ∪{∞}))) →
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    (LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type) ⊗
                      ℕ∪{∞}))
              σ') :
          Type) ⟶
      tensorObj (𝒞 :=
        CompHausLike.category fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        S ℕ∪{∞})
    (({
          hom :=
            TopCat.ofHom
              {
                toFun :=
                  Subtype.val (p :=
                    fun
                      (x :
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                          (pullback (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                            (y' ▷ ℕ∪{∞}))) ↦
                    x ∈
                      fibres
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π') :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (pullback π (y' ▷ ℕ∪{∞}))) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (LightProfinite.of
                                  (↑(S'
                                        (⇑(ConcreteCategory.hom π) :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                T) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (S ⊗ ℕ∪{∞}))) :
                                    Type) ⊗
                                ℕ∪{∞}))
                        σ'),
                continuous_toFun := ⋯ :
                C((↑(fibres
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π') :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (pullback π (y' ▷ ℕ∪{∞}))) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (LightProfinite.of
                                  (↑(S'
                                        (⇑(ConcreteCategory.hom π) :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                T) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (S ⊗ ℕ∪{∞}))) :
                                    Type) ⊗
                                ℕ∪{∞}))
                        σ') :
                    Type),
                  (↑(pullback (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                          (y' ▷ ℕ∪{∞})).1 :
                    Type)) } :
          InducedCategory.Hom (D := TopCat) (F :=
            toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
            (LightProfinite.of
              (↑(fibres
                    (⇑(ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type),
                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type)))
                          (CC :=
                          fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                          π') :
                      (a :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (pullback π (y' ▷ ℕ∪{∞}))) →
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          (LightProfinite.of
                              (↑(S'
                                    (⇑(ConcreteCategory.hom π) :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            T) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (S ⊗ ℕ∪{∞}))) :
                                Type) ⊗
                            ℕ∪{∞}))
                    σ') :
                Type))
            (pullback (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})) } ≫
        π') ≫
      y' ▷ ℕ∪{∞})
    (CategoryStruct.comp (Y :=
        pullback (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞}))
        {
          hom :=
            TopCat.ofHom
              {
                toFun :=
                  Subtype.val (p :=
                    fun
                      (x :
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                          (pullback (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                            (y' ▷ ℕ∪{∞}))) ↦
                    x ∈
                      fibres
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π') :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (pullback π (y' ▷ ℕ∪{∞}))) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (LightProfinite.of
                                  (↑(S'
                                        (⇑(ConcreteCategory.hom π) :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                T) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (S ⊗ ℕ∪{∞}))) :
                                    Type) ⊗
                                ℕ∪{∞}))
                        σ'),
                continuous_toFun := ⋯ } }
        (pullback.fst (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})) ≫
      π)
refine_4 :
  IsSplitEpi (X :=
    LightProfinite.fibre (X :=
      LightProfinite.of
        (↑(fibres
              (⇑(ConcreteCategory.hom (FC :=
                    fun
                      (x1 x2 :
                        CompHausLike fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                        Type),
                      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                        Type)))
                    (CC :=
                    fun
                      (X :
                        CompHausLike fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                      Type))
                    π') :
                (a :
                    (fun
                          (X :
                            CompHausLike fun (X : TopCat) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                        (↑X.toTop : Type))
                      (pullback π (y' ▷ ℕ∪{∞}))) →
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                      (↑X.toTop : Type))
                    (LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type) ⊗
                      ℕ∪{∞}))
              σ') :
          Type))
      ∞
      (({
            hom :=
              TopCat.ofHom
                {
                  toFun :=
                    Subtype.val (p :=
                      fun
                        (x :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                            (pullback (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                              (y' ▷ ℕ∪{∞}))) ↦
                      x ∈
                        fibres
                          (⇑(ConcreteCategory.hom (FC :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type),
                                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type)))
                                (CC :=
                                fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                                π') :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (pullback π (y' ▷ ℕ∪{∞}))) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (LightProfinite.of
                                    (↑(S'
                                          (⇑(ConcreteCategory.hom π) :
                                            (a :
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  T) →
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (S ⊗ ℕ∪{∞}))) :
                                      Type) ⊗
                                  ℕ∪{∞}))
                          σ'),
                  continuous_toFun := ⋯ :
                  C((↑(fibres
                          (⇑(ConcreteCategory.hom (FC :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type),
                                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type)))
                                (CC :=
                                fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                                π') :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (pullback π (y' ▷ ℕ∪{∞}))) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (LightProfinite.of
                                    (↑(S'
                                          (⇑(ConcreteCategory.hom π) :
                                            (a :
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  T) →
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (S ⊗ ℕ∪{∞}))) :
                                      Type) ⊗
                                  ℕ∪{∞}))
                          σ') :
                      Type),
                    (↑(pullback (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                            (y' ▷ ℕ∪{∞})).1 :
                      Type)) } :
            InducedCategory.Hom (D := TopCat) (F :=
              toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
              (LightProfinite.of
                (↑(fibres
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π') :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (pullback π (y' ▷ ℕ∪{∞}))) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (LightProfinite.of
                                (↑(S'
                                      (⇑(ConcreteCategory.hom π) :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              T) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (S ⊗ ℕ∪{∞}))) :
                                  Type) ⊗
                              ℕ∪{∞}))
                      σ') :
                  Type))
              (pullback (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})) } ≫
          π') ≫
        snd
          (LightProfinite.of
            (↑(S'
                  (⇑(ConcreteCategory.hom (FC :=
                        fun
                          (x1 x2 :
                            CompHausLike fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                        C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type),
                          (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type)))
                        (CC :=
                        fun
                          (X :
                            CompHausLike fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                          Type))
                        π) :
                    (a :
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          T) →
                      (fun
                            (X :
                              CompHausLike fun (X : TopCat) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑X.toTop : Type))
                        (S ⊗ ℕ∪{∞}))) :
              Type))
          ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞
        (({
              hom :=
                TopCat.ofHom
                  {
                    toFun :=
                      Subtype.val (p :=
                        fun
                          (x :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                              (pullback (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                (y' ▷ ℕ∪{∞}))) ↦
                        x ∈
                          fibres
                            (⇑(ConcreteCategory.hom (FC :=
                                  fun
                                    (x1 x2 :
                                      CompHausLike fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type),
                                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type)))
                                  (CC :=
                                  fun
                                    (X :
                                      CompHausLike fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type))
                                  π') :
                              (a :
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (pullback π (y' ▷ ℕ∪{∞}))) →
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (LightProfinite.of
                                      (↑(S'
                                            (⇑(ConcreteCategory.hom π) :
                                              (a :
                                                  (fun
                                                        (X :
                                                          CompHausLike fun (X : TopCat) ↦
                                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                                              SecondCountableTopology (↑X : Type)) ↦
                                                      (↑X.toTop : Type))
                                                    T) →
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  (S ⊗ ℕ∪{∞}))) :
                                        Type) ⊗
                                    ℕ∪{∞}))
                            σ'),
                    continuous_toFun := ⋯ :
                    C((↑(fibres
                            (⇑(ConcreteCategory.hom (FC :=
                                  fun
                                    (x1 x2 :
                                      CompHausLike fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type),
                                    (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type)))
                                  (CC :=
                                  fun
                                    (X :
                                      CompHausLike fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type))
                                  π') :
                              (a :
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (pullback π (y' ▷ ℕ∪{∞}))) →
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (LightProfinite.of
                                      (↑(S'
                                            (⇑(ConcreteCategory.hom π) :
                                              (a :
                                                  (fun
                                                        (X :
                                                          CompHausLike fun (X : TopCat) ↦
                                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                                              SecondCountableTopology (↑X : Type)) ↦
                                                      (↑X.toTop : Type))
                                                    T) →
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  (S ⊗ ℕ∪{∞}))) :
                                        Type) ⊗
                                    ℕ∪{∞}))
                            σ') :
                        Type),
                      (↑(pullback (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                              (y' ▷ ℕ∪{∞})).1 :
                        Type)) } :
              InducedCategory.Hom (D := TopCat) (F :=
                toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                (LightProfinite.of
                  (↑(fibres
                        (⇑(ConcreteCategory.hom (FC :=
                              fun
                                (x1 x2 :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type),
                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type)))
                              (CC :=
                              fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                              π') :
                          (a :
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (pullback π (y' ▷ ℕ∪{∞}))) →
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (LightProfinite.of
                                  (↑(S'
                                        (⇑(ConcreteCategory.hom π) :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                T) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (S ⊗ ℕ∪{∞}))) :
                                    Type) ⊗
                                ℕ∪{∞}))
                        σ') :
                    Type))
                (pullback (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})) } ≫
            π') ≫
          snd
            (LightProfinite.of
              (↑(S'
                    (⇑(ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type),
                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type)))
                          (CC :=
                          fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                          π) :
                      (a :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            T) →
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          (S ⊗ ℕ∪{∞}))) :
                Type))
            ℕ∪{∞}) ≫
      ({
            hom :=
              TopCat.ofHom
                {
                  toFun :=
                    Subtype.val (p :=
                      fun
                        (x :
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type))
                            (pullback (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                              (y' ▷ ℕ∪{∞}))) ↦
                      x ∈
                        fibres
                          (⇑(ConcreteCategory.hom (FC :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type),
                                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type)))
                                (CC :=
                                fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                                π') :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (pullback π (y' ▷ ℕ∪{∞}))) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (LightProfinite.of
                                    (↑(S'
                                          (⇑(ConcreteCategory.hom π) :
                                            (a :
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  T) →
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (S ⊗ ℕ∪{∞}))) :
                                      Type) ⊗
                                  ℕ∪{∞}))
                          σ'),
                  continuous_toFun := ⋯ :
                  C((↑(fibres
                          (⇑(ConcreteCategory.hom (FC :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type),
                                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type)))
                                (CC :=
                                fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                                π') :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (pullback π (y' ▷ ℕ∪{∞}))) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (LightProfinite.of
                                    (↑(S'
                                          (⇑(ConcreteCategory.hom π) :
                                            (a :
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  T) →
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (S ⊗ ℕ∪{∞}))) :
                                      Type) ⊗
                                  ℕ∪{∞}))
                          σ') :
                      Type),
                    (↑(pullback (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                            (y' ▷ ℕ∪{∞})).1 :
                      Type)) } :
            InducedCategory.Hom (D := TopCat) (F :=
              toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
              (LightProfinite.of
                (↑(fibres
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π') :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (pullback π (y' ▷ ℕ∪{∞}))) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (LightProfinite.of
                                (↑(S'
                                      (⇑(ConcreteCategory.hom π) :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              T) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (S ⊗ ℕ∪{∞}))) :
                                  Type) ⊗
                              ℕ∪{∞}))
                      σ') :
                  Type))
              (pullback (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞})) } ≫
          π') ≫
        fst
          (LightProfinite.of
            (↑(S'
                  (⇑(ConcreteCategory.hom (FC :=
                        fun
                          (x1 x2 :
                            CompHausLike fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                        C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type),
                          (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type)))
                        (CC :=
                        fun
                          (X :
                            CompHausLike fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                          Type))
                        π) :
                    (a :
                        (fun
                              (X :
                                CompHausLike fun (X : TopCat) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑X.toTop : Type))
                          T) →
                      (fun
                            (X :
                              CompHausLike fun (X : TopCat) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑X.toTop : Type))
                        (S ⊗ ℕ∪{∞}))) :
              Type))
          ℕ∪{∞})
⊢ ∃ (S' : LightProfinite.{0}) (T' : LightProfinite.{0}) (y' : S' ⟶ S) (π' :
    T' ⟶
      tensorObj (𝒞 :=
        CompHausLike.category fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        S' ℕ∪{∞})
    (g' : T' ⟶ T),
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
              (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧
            Epi (cover π')
have refine_5 : Epi (X :=
  CompHausLike.of (fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
    ((↑((LightProfinite.of
                (↑(fibres
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π') :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (pullback π (y' ▷ ℕ∪{∞}))) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (LightProfinite.of
                                (↑(S'
                                      (⇑(ConcreteCategory.hom π) :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              T) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (S ⊗ ℕ∪{∞}))) :
                                  Type) ⊗
                              ℕ∪{∞}))
                      σ') :
                  Type)).toTop
            (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type) ⊕
      (↑((pullback (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) (X :=
                LightProfinite.fibre (X :=
                  LightProfinite.of
                    (↑(fibres
                          (⇑(ConcreteCategory.hom (FC :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type),
                                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type)))
                                (CC :=
                                fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                                π') :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (pullback π (y' ▷ ℕ∪{∞}))) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (LightProfinite.of
                                    (↑(S'
                                          (⇑(ConcreteCategory.hom π) :
                                            (a :
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  T) →
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (S ⊗ ℕ∪{∞}))) :
                                      Type) ⊗
                                  ℕ∪{∞}))
                          σ') :
                      Type))
                  ∞
                  (({
                        hom :=
                          TopCat.ofHom
                            {
                              toFun :=
                                Subtype.val (p :=
                                  fun
                                    (x :
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                        (pullback (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                          (y' ▷ ℕ∪{∞}))) ↦
                                  x ∈
                                    fibres
                                      (⇑(ConcreteCategory.hom (FC :=
                                            fun
                                              (x1 x2 :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type),
                                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type)))
                                            (CC :=
                                            fun
                                              (X :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type))
                                            π') :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (pullback π (y' ▷ ℕ∪{∞}))) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (LightProfinite.of
                                                (↑(S'
                                                      (⇑(ConcreteCategory.hom π) :
                                                        (a :
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              T) →
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            (S ⊗ ℕ∪{∞}))) :
                                                  Type) ⊗
                                              ℕ∪{∞}))
                                      σ'),
                              continuous_toFun := sorry :
                              C((↑(fibres
                                      (⇑(ConcreteCategory.hom (FC :=
                                            fun
                                              (x1 x2 :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type),
                                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type)))
                                            (CC :=
                                            fun
                                              (X :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type))
                                            π') :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (pullback π (y' ▷ ℕ∪{∞}))) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (LightProfinite.of
                                                (↑(S'
                                                      (⇑(ConcreteCategory.hom π) :
                                                        (a :
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              T) →
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            (S ⊗ ℕ∪{∞}))) :
                                                  Type) ⊗
                                              ℕ∪{∞}))
                                      σ') :
                                  Type),
                                (↑(pullback (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                        (y' ▷ ℕ∪{∞})).1 :
                                  Type)) } :
                        InducedCategory.Hom (D := TopCat) (F :=
                          toTop (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                          (LightProfinite.of
                            (↑(fibres
                                  (⇑(ConcreteCategory.hom (FC :=
                                        fun
                                          (x1 x2 :
                                            CompHausLike fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type),
                                          (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type)))
                                        (CC :=
                                        fun
                                          (X :
                                            CompHausLike fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type))
                                        π') :
                                    (a :
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (pullback π (y' ▷ ℕ∪{∞}))) →
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑X.toTop : Type))
                                        (LightProfinite.of
                                            (↑(S'
                                                  (⇑(ConcreteCategory.hom π) :
                                                    (a :
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          T) →
                                                      (fun
                                                            (X :
                                                              CompHausLike fun (X : TopCat) ↦
                                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                                  SecondCountableTopology (↑X : Type)) ↦
                                                          (↑X.toTop : Type))
                                                        (S ⊗ ℕ∪{∞}))) :
                                              Type) ⊗
                                          ℕ∪{∞}))
                                  σ') :
                              Type))
                          (pullback (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                            (y' ▷ ℕ∪{∞})) } ≫
                      π') ≫
                    snd
                      (LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom (FC :=
                                    fun
                                      (x1 x2 :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type),
                                      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type)))
                                    (CC :=
                                    fun
                                      (X :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type))
                                    π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type))
                      ℕ∪{∞}))
                (Y :=
                LightProfinite.fibre (X :=
                  LightProfinite.of
                    (↑(fibres
                          (⇑(ConcreteCategory.hom (FC :=
                                fun
                                  (x1 x2 :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type),
                                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                    Type)))
                                (CC :=
                                fun
                                  (X :
                                    CompHausLike fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                  Type))
                                π') :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑X.toTop : Type))
                                  (pullback π (y' ▷ ℕ∪{∞}))) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                  (↑X.toTop : Type))
                                (LightProfinite.of
                                    (↑(S'
                                          (⇑(ConcreteCategory.hom π) :
                                            (a :
                                                (fun
                                                      (X :
                                                        CompHausLike fun (X : TopCat) ↦
                                                          TotallyDisconnectedSpace (↑X : Type) ∧
                                                            SecondCountableTopology (↑X : Type)) ↦
                                                    (↑X.toTop : Type))
                                                  T) →
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (S ⊗ ℕ∪{∞}))) :
                                      Type) ⊗
                                  ℕ∪{∞}))
                          σ') :
                      Type))
                  ∞
                  (({
                        hom :=
                          TopCat.ofHom
                            {
                              toFun :=
                                Subtype.val (p :=
                                  fun
                                    (x :
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                        (pullback (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                          (y' ▷ ℕ∪{∞}))) ↦
                                  x ∈
                                    fibres
                                      (⇑(ConcreteCategory.hom (FC :=
                                            fun
                                              (x1 x2 :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type),
                                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type)))
                                            (CC :=
                                            fun
                                              (X :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type))
                                            π') :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (pullback π (y' ▷ ℕ∪{∞}))) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (LightProfinite.of
                                                (↑(S'
                                                      (⇑(ConcreteCategory.hom π) :
                                                        (a :
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              T) →
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            (S ⊗ ℕ∪{∞}))) :
                                                  Type) ⊗
                                              ℕ∪{∞}))
                                      σ'),
                              continuous_toFun := sorry :
                              C((↑(fibres
                                      (⇑(ConcreteCategory.hom (FC :=
                                            fun
                                              (x1 x2 :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type),
                                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type)))
                                            (CC :=
                                            fun
                                              (X :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type))
                                            π') :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (pullback π (y' ▷ ℕ∪{∞}))) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (LightProfinite.of
                                                (↑(S'
                                                      (⇑(ConcreteCategory.hom π) :
                                                        (a :
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              T) →
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            (S ⊗ ℕ∪{∞}))) :
                                                  Type) ⊗
                                              ℕ∪{∞}))
                                      σ') :
                                  Type),
                                (↑(pullback (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                        (y' ▷ ℕ∪{∞})).1 :
                                  Type)) } :
                        InducedCategory.Hom (D := TopCat) (F :=
                          toTop (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                          (LightProfinite.of
                            (↑(fibres
                                  (⇑(ConcreteCategory.hom (FC :=
                                        fun
                                          (x1 x2 :
                                            CompHausLike fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type),
                                          (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type)))
                                        (CC :=
                                        fun
                                          (X :
                                            CompHausLike fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type))
                                        π') :
                                    (a :
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (pullback π (y' ▷ ℕ∪{∞}))) →
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑X.toTop : Type))
                                        (LightProfinite.of
                                            (↑(S'
                                                  (⇑(ConcreteCategory.hom π) :
                                                    (a :
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          T) →
                                                      (fun
                                                            (X :
                                                              CompHausLike fun (X : TopCat) ↦
                                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                                  SecondCountableTopology (↑X : Type)) ↦
                                                          (↑X.toTop : Type))
                                                        (S ⊗ ℕ∪{∞}))) :
                                              Type) ⊗
                                          ℕ∪{∞}))
                                  σ') :
                              Type))
                          (pullback (P := fun (X : TopCat.{0}) ↦
                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                            (y' ▷ ℕ∪{∞})) } ≫
                      π') ≫
                    snd
                      (LightProfinite.of
                        (↑(S'
                              (⇑(ConcreteCategory.hom (FC :=
                                    fun
                                      (x1 x2 :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type),
                                      (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type)))
                                    (CC :=
                                    fun
                                      (X :
                                        CompHausLike fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                    (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                      Type))
                                    π) :
                                (a :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      T) →
                                  (fun
                                        (X :
                                          CompHausLike fun (X : TopCat) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑X.toTop : Type))
                                    (S ⊗ ℕ∪{∞}))) :
                          Type))
                      ℕ∪{∞}))
                (LightProfinite.fibreIncl ∞
                    (({
                          hom :=
                            TopCat.ofHom
                              {
                                toFun :=
                                  Subtype.val (p :=
                                    fun
                                      (x :
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type))
                                          (pullback (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                                            π (y' ▷ ℕ∪{∞}))) ↦
                                    x ∈
                                      fibres
                                        (⇑(ConcreteCategory.hom (FC :=
                                              fun
                                                (x1 x2 :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type),
                                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type)))
                                              (CC :=
                                              fun
                                                (X :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type))
                                              π') :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (pullback π (y' ▷ ℕ∪{∞}))) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (LightProfinite.of
                                                  (↑(S'
                                                        (⇑(ConcreteCategory.hom π) :
                                                          (a :
                                                              (fun
                                                                    (X :
                                                                      CompHausLike fun (X : TopCat) ↦
                                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                                          SecondCountableTopology (↑X : Type)) ↦
                                                                  (↑X.toTop : Type))
                                                                T) →
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              (S ⊗ ℕ∪{∞}))) :
                                                    Type) ⊗
                                                ℕ∪{∞}))
                                        σ'),
                                continuous_toFun := sorry :
                                C((↑(fibres
                                        (⇑(ConcreteCategory.hom (FC :=
                                              fun
                                                (x1 x2 :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type),
                                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type)))
                                              (CC :=
                                              fun
                                                (X :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type))
                                              π') :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (pullback π (y' ▷ ℕ∪{∞}))) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (LightProfinite.of
                                                  (↑(S'
                                                        (⇑(ConcreteCategory.hom π) :
                                                          (a :
                                                              (fun
                                                                    (X :
                                                                      CompHausLike fun (X : TopCat) ↦
                                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                                          SecondCountableTopology (↑X : Type)) ↦
                                                                  (↑X.toTop : Type))
                                                                T) →
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              (S ⊗ ℕ∪{∞}))) :
                                                    Type) ⊗
                                                ℕ∪{∞}))
                                        σ') :
                                    Type),
                                  (↑(pullback (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                          (y' ▷ ℕ∪{∞})).1 :
                                    Type)) } :
                          InducedCategory.Hom (D := TopCat) (F :=
                            toTop (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                            (LightProfinite.of
                              (↑(fibres
                                    (⇑(ConcreteCategory.hom (FC :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type),
                                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type)))
                                          (CC :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                          π') :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (pullback π (y' ▷ ℕ∪{∞}))) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (LightProfinite.of
                                              (↑(S'
                                                    (⇑(ConcreteCategory.hom π) :
                                                      (a :
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            T) →
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          (S ⊗ ℕ∪{∞}))) :
                                                Type) ⊗
                                            ℕ∪{∞}))
                                    σ') :
                                Type))
                            (pullback (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                              (y' ▷ ℕ∪{∞})) } ≫
                        π') ≫
                      snd
                        (LightProfinite.of
                          (↑(S'
                                (⇑(ConcreteCategory.hom (FC :=
                                      fun
                                        (x1 x2 :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type),
                                        (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type)))
                                      (CC :=
                                      fun
                                        (X :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type))
                                      π) :
                                  (a :
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑X.toTop : Type))
                                        T) →
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      (S ⊗ ℕ∪{∞}))) :
                            Type))
                        ℕ∪{∞}) ≫
                  {
                      hom :=
                        TopCat.ofHom
                          {
                            toFun :=
                              Subtype.val (p :=
                                fun
                                  (x :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type))
                                      (pullback (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                        (y' ▷ ℕ∪{∞}))) ↦
                                x ∈
                                  fibres
                                    (⇑(ConcreteCategory.hom (FC :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type),
                                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type)))
                                          (CC :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                          π') :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (pullback π (y' ▷ ℕ∪{∞}))) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (LightProfinite.of
                                              (↑(S'
                                                    (⇑(ConcreteCategory.hom π) :
                                                      (a :
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            T) →
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          (S ⊗ ℕ∪{∞}))) :
                                                Type) ⊗
                                            ℕ∪{∞}))
                                    σ'),
                            continuous_toFun := sorry :
                            C((↑(fibres
                                    (⇑(ConcreteCategory.hom (FC :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type),
                                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type)))
                                          (CC :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                          π') :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (pullback π (y' ▷ ℕ∪{∞}))) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (LightProfinite.of
                                              (↑(S'
                                                    (⇑(ConcreteCategory.hom π) :
                                                      (a :
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            T) →
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          (S ⊗ ℕ∪{∞}))) :
                                                Type) ⊗
                                            ℕ∪{∞}))
                                    σ') :
                                Type),
                              (↑(pullback (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                      (y' ▷ ℕ∪{∞})).1 :
                                Type)) } :
                      InducedCategory.Hom (D := TopCat) (F :=
                        toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                        (LightProfinite.of
                          (↑(fibres
                                (⇑(ConcreteCategory.hom (FC :=
                                      fun
                                        (x1 x2 :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type),
                                        (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type)))
                                      (CC :=
                                      fun
                                        (X :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type))
                                      π') :
                                  (a :
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑X.toTop : Type))
                                        (pullback π (y' ▷ ℕ∪{∞}))) →
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      (LightProfinite.of
                                          (↑(S'
                                                (⇑(ConcreteCategory.hom π) :
                                                  (a :
                                                      (fun
                                                            (X :
                                                              CompHausLike fun (X : TopCat) ↦
                                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                                  SecondCountableTopology (↑X : Type)) ↦
                                                          (↑X.toTop : Type))
                                                        T) →
                                                    (fun
                                                          (X :
                                                            CompHausLike fun (X : TopCat) ↦
                                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                                SecondCountableTopology (↑X : Type)) ↦
                                                        (↑X.toTop : Type))
                                                      (S ⊗ ℕ∪{∞}))) :
                                            Type) ⊗
                                        ℕ∪{∞}))
                                σ') :
                            Type))
                        (pullback (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                          (y' ▷ ℕ∪{∞})) } ≫
                    π')
                (LightProfinite.fibreIncl ∞
                    (({
                          hom :=
                            TopCat.ofHom
                              {
                                toFun :=
                                  Subtype.val (p :=
                                    fun
                                      (x :
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type))
                                          (pullback (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
                                            π (y' ▷ ℕ∪{∞}))) ↦
                                    x ∈
                                      fibres
                                        (⇑(ConcreteCategory.hom (FC :=
                                              fun
                                                (x1 x2 :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type),
                                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type)))
                                              (CC :=
                                              fun
                                                (X :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type))
                                              π') :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (pullback π (y' ▷ ℕ∪{∞}))) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (LightProfinite.of
                                                  (↑(S'
                                                        (⇑(ConcreteCategory.hom π) :
                                                          (a :
                                                              (fun
                                                                    (X :
                                                                      CompHausLike fun (X : TopCat) ↦
                                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                                          SecondCountableTopology (↑X : Type)) ↦
                                                                  (↑X.toTop : Type))
                                                                T) →
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              (S ⊗ ℕ∪{∞}))) :
                                                    Type) ⊗
                                                ℕ∪{∞}))
                                        σ'),
                                continuous_toFun := sorry :
                                C((↑(fibres
                                        (⇑(ConcreteCategory.hom (FC :=
                                              fun
                                                (x1 x2 :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type),
                                                (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type))) :
                                                  Type)))
                                              (CC :=
                                              fun
                                                (X :
                                                  CompHausLike fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type))) :
                                                Type))
                                              π') :
                                          (a :
                                              (fun
                                                    (X :
                                                      CompHausLike fun (X : TopCat) ↦
                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                          SecondCountableTopology (↑X : Type)) ↦
                                                  (↑X.toTop : Type))
                                                (pullback π (y' ▷ ℕ∪{∞}))) →
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              (LightProfinite.of
                                                  (↑(S'
                                                        (⇑(ConcreteCategory.hom π) :
                                                          (a :
                                                              (fun
                                                                    (X :
                                                                      CompHausLike fun (X : TopCat) ↦
                                                                        TotallyDisconnectedSpace (↑X : Type) ∧
                                                                          SecondCountableTopology (↑X : Type)) ↦
                                                                  (↑X.toTop : Type))
                                                                T) →
                                                            (fun
                                                                  (X :
                                                                    CompHausLike fun (X : TopCat) ↦
                                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                                        SecondCountableTopology (↑X : Type)) ↦
                                                                (↑X.toTop : Type))
                                                              (S ⊗ ℕ∪{∞}))) :
                                                    Type) ⊗
                                                ℕ∪{∞}))
                                        σ') :
                                    Type),
                                  (↑(pullback (P := fun (X : TopCat.{0}) ↦
                                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                          (y' ▷ ℕ∪{∞})).1 :
                                    Type)) } :
                          InducedCategory.Hom (D := TopCat) (F :=
                            toTop (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                            (LightProfinite.of
                              (↑(fibres
                                    (⇑(ConcreteCategory.hom (FC :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type),
                                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type)))
                                          (CC :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                          π') :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (pullback π (y' ▷ ℕ∪{∞}))) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (LightProfinite.of
                                              (↑(S'
                                                    (⇑(ConcreteCategory.hom π) :
                                                      (a :
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            T) →
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          (S ⊗ ℕ∪{∞}))) :
                                                Type) ⊗
                                            ℕ∪{∞}))
                                    σ') :
                                Type))
                            (pullback (P := fun (X : TopCat.{0}) ↦
                              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                              (y' ▷ ℕ∪{∞})) } ≫
                        π') ≫
                      snd
                        (LightProfinite.of
                          (↑(S'
                                (⇑(ConcreteCategory.hom (FC :=
                                      fun
                                        (x1 x2 :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type),
                                        (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type)))
                                      (CC :=
                                      fun
                                        (X :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type))
                                      π) :
                                  (a :
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑X.toTop : Type))
                                        T) →
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      (S ⊗ ℕ∪{∞}))) :
                            Type))
                        ℕ∪{∞}) ≫
                  {
                      hom :=
                        TopCat.ofHom
                          {
                            toFun :=
                              Subtype.val (p :=
                                fun
                                  (x :
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type))
                                      (pullback (P := fun (X : TopCat.{0}) ↦
                                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                        (y' ▷ ℕ∪{∞}))) ↦
                                x ∈
                                  fibres
                                    (⇑(ConcreteCategory.hom (FC :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type),
                                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type)))
                                          (CC :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                          π') :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (pullback π (y' ▷ ℕ∪{∞}))) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (LightProfinite.of
                                              (↑(S'
                                                    (⇑(ConcreteCategory.hom π) :
                                                      (a :
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            T) →
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          (S ⊗ ℕ∪{∞}))) :
                                                Type) ⊗
                                            ℕ∪{∞}))
                                    σ'),
                            continuous_toFun := sorry :
                            C((↑(fibres
                                    (⇑(ConcreteCategory.hom (FC :=
                                          fun
                                            (x1 x2 :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type),
                                            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type))) :
                                              Type)))
                                          (CC :=
                                          fun
                                            (X :
                                              CompHausLike fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type))) :
                                            Type))
                                          π') :
                                      (a :
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (pullback π (y' ▷ ℕ∪{∞}))) →
                                        (fun
                                              (X :
                                                CompHausLike fun (X : TopCat) ↦
                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                    SecondCountableTopology (↑X : Type)) ↦
                                            (↑X.toTop : Type))
                                          (LightProfinite.of
                                              (↑(S'
                                                    (⇑(ConcreteCategory.hom π) :
                                                      (a :
                                                          (fun
                                                                (X :
                                                                  CompHausLike fun (X : TopCat) ↦
                                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                                      SecondCountableTopology (↑X : Type)) ↦
                                                              (↑X.toTop : Type))
                                                            T) →
                                                        (fun
                                                              (X :
                                                                CompHausLike fun (X : TopCat) ↦
                                                                  TotallyDisconnectedSpace (↑X : Type) ∧
                                                                    SecondCountableTopology (↑X : Type)) ↦
                                                            (↑X.toTop : Type))
                                                          (S ⊗ ℕ∪{∞}))) :
                                                Type) ⊗
                                            ℕ∪{∞}))
                                    σ') :
                                Type),
                              (↑(pullback (P := fun (X : TopCat.{0}) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                                      (y' ▷ ℕ∪{∞})).1 :
                                Type)) } :
                      InducedCategory.Hom (D := TopCat) (F :=
                        toTop (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)))
                        (LightProfinite.of
                          (↑(fibres
                                (⇑(ConcreteCategory.hom (FC :=
                                      fun
                                        (x1 x2 :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type),
                                        (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type))) :
                                          Type)))
                                      (CC :=
                                      fun
                                        (X :
                                          CompHausLike fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type)) ↦
                                      (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                            TotallyDisconnectedSpace (↑X : Type) ∧
                                              SecondCountableTopology (↑X : Type))) :
                                        Type))
                                      π') :
                                  (a :
                                      (fun
                                            (X :
                                              CompHausLike fun (X : TopCat) ↦
                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                  SecondCountableTopology (↑X : Type)) ↦
                                          (↑X.toTop : Type))
                                        (pullback π (y' ▷ ℕ∪{∞}))) →
                                    (fun
                                          (X :
                                            CompHausLike fun (X : TopCat) ↦
                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                SecondCountableTopology (↑X : Type)) ↦
                                        (↑X.toTop : Type))
                                      (LightProfinite.of
                                          (↑(S'
                                                (⇑(ConcreteCategory.hom π) :
                                                  (a :
                                                      (fun
                                                            (X :
                                                              CompHausLike fun (X : TopCat) ↦
                                                                TotallyDisconnectedSpace (↑X : Type) ∧
                                                                  SecondCountableTopology (↑X : Type)) ↦
                                                          (↑X.toTop : Type))
                                                        T) →
                                                    (fun
                                                          (X :
                                                            CompHausLike fun (X : TopCat) ↦
                                                              TotallyDisconnectedSpace (↑X : Type) ∧
                                                                SecondCountableTopology (↑X : Type)) ↦
                                                        (↑X.toTop : Type))
                                                      (S ⊗ ℕ∪{∞}))) :
                                            Type) ⊗
                                        ℕ∪{∞}))
                                σ') :
                            Type))
                        (pullback (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π
                          (y' ▷ ℕ∪{∞})) } ≫
                    π')).toTop
            (P := fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)))
  (cover
    ({
        hom :=
          TopCat.ofHom
            {
              toFun :=
                Subtype.val (p :=
                  fun
                    (x :
                      (fun
                            (X :
                              CompHausLike fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                            Type))
                        (pullback (P := fun (X : TopCat.{0}) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) π (y' ▷ ℕ∪{∞}))) ↦
                  x ∈
                    fibres
                      (⇑(ConcreteCategory.hom (FC :=
                            fun
                              (x1 x2 :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type),
                              (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                                Type)))
                            (CC :=
                            fun
                              (X :
                                CompHausLike fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                              Type))
                            π') :
                        (a :
                            (fun
                                  (X :
                                    CompHausLike fun (X : TopCat) ↦
                                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                                (↑X.toTop : Type))
                              (pullback π (y' ▷ ℕ∪{∞}))) →
                          (fun
                                (X :
                                  CompHausLike fun (X : TopCat) ↦
                                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                              (↑X.toTop : Type))
                            (LightProfinite.of
                                (↑(S'
                                      (⇑(ConcreteCategory.hom π) :
                                        (a :
                                            (fun
                                                  (X :
                                                    CompHausLike fun (X : TopCat) ↦
                                                      TotallyDisconnectedSpace (↑X : Type) ∧
                                                        SecondCountableTopology (↑X : Type)) ↦
                                                (↑X.toTop : Type))
                                              T) →
                                          (fun
                                                (X :
                                                  CompHausLike fun (X : TopCat) ↦
                                                    TotallyDisconnectedSpace (↑X : Type) ∧
                                                      SecondCountableTopology (↑X : Type)) ↦
                                              (↑X.toTop : Type))
                                            (S ⊗ ℕ∪{∞}))) :
                                  Type) ⊗
                              ℕ∪{∞}))
                      σ'),
              continuous_toFun := sorry } } ≫
      π'))
Tactic: refine ⟨LightProfinite.of (S' π), LightProfinite.of (fibres π' σ'), y',
    ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ π',
    ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩