\import Category
\import Category.Meta
\import Logic
\import Paths
\import Topology.CoverSpace

\instance PrecoverSpaceCat : Cat PrecoverSpace
  | Hom => PrecoverMap
  | id X => PrecoverMap.id
  | o => PrecoverMap.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam c d => PrecoverSpace.PrecoverSpace-ext \lam {C} =>
      (\lam Cc => cauchy-subset (func-cover {d} Cc) \lam (inP (V,CV,p)) => transportInv C p CV,
       \lam Cc => cauchy-subset (func-cover {c} Cc) \lam (inP (V,CV,p)) => transportInv C p CV)

\instance CoverSpaceCat : Cat CoverSpace
  | Hom => PrecoverMap
  | id X => PrecoverMap.id
  | o => PrecoverMap.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam c d => CoverSpace.CoverSpace-ext \lam {C} =>
      (\lam Cc => cauchy-subset (func-cover {d} Cc) \lam (inP (V,CV,p)) => transportInv C p CV,
       \lam Cc => cauchy-subset (func-cover {c} Cc) \lam (inP (V,CV,p)) => transportInv C p CV)