A covering space of a type (space) is a family of sets indexed by .
{-# 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)