{P : Sort u} →
  {α : Type u_1} →
    {β : Type u_2} →
      {inst : TopologicalSpace α} →
        {F : Ctop.Realizer α} →
          {f : β → Set α} →
            {t : LocallyFinite.Realizer F f} →
              {α' : Type u_1} →
                {β' : Type u_2} →
                  {inst' : TopologicalSpace α'} →
                    {F' : Ctop.Realizer α'} →
                      {f' : β' → Set α'} →
                        {t' : LocallyFinite.Realizer F' f'} →
                          α = α' →
                            β = β' →
                              inst ≍ inst' → F ≍ F' → f ≍ f' → t ≍ t' → LocallyFinite.Realizer.noConfusionType P t t'