module foundations.fiber where
open import foundations.universe open import foundations.identity-type open import foundations.sigma-type
private variable
ℓ ℓ′ : Level
Fiber : ∀ {A : Type ℓ} {B : Type ℓ′}
→ (A → B) → B → Type (ℓ ⊔ ℓ′)
Fiber {A = A} f y = Σ[ x ∈ A ] (f x ＝ y)