∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] (A : C)
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (if h : p₀ ∈ Opposite.unop U then CategoryTheory.eqToHom ⋯
    else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (if p₀ ∈ Opposite.unop U then A else ⊤_ C)) =
    CategoryTheory.CategoryStruct.id (if p₀ ∈ Opposite.unop U then A else ⊤_ C)