\import Category
\import Category.Meta
\import Paths.Meta
\import Topology.TopSpace

\instance TopCat : Cat TopSpace
  | Hom => ContMap
  | id X => ContMap.id
  | o => ContMap.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {S1} {S2} h1 h2 => exts (\lam U => ext (func-cont {h2} {U}, func-cont {h1} {U})))