Home

前層

module category-theory.presheaf where
Imports 
open import foundations.universe
open import foundations.function-extensionality
open import category-theory.category
open import category-theory.functor
open import category-theory.category-of-sets

private variable o h : Level

module _ ℓ (e : FunExtLevel ℓ ℓ) where
  Presheaf : Category o h →  Type (o ⊔ h ⊔ lsuc ℓ)
  Presheaf 𝒞 = Functor 𝒞 (Sets ℓ e)