Definition. Covering spaces in HoTT [ag-000L]

A covering space of a type (space) $A$ is a family of sets indexed by $A$ .

{-# OPTIONS --safe --without-K #-}
module ag-000L where

open import MLTT.Spartan hiding (fiber)
open import UF.Sets

record covering (A : 𝓤 ̇ ) : 𝓤 ⁺  ̇ where
  constructor cov[_,_]
  field
    fiber : A → 𝓤 ̇
    fiber-is-set : ∀ (a : A) → is-set (fiber a)