The category of families of sets

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-28.
Last modified on 2023-11-01.

module foundation.category-of-families-of-sets where
Imports 
open import category-theory.categories
open import category-theory.large-categories
open import category-theory.large-function-categories
open import category-theory.large-function-precategories
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.category-of-sets
open import foundation.universe-levels

Idea

The large category of families of sets over a type A is the large function category A → Set.

Definition

The large precategory of families of sets over a type

Family-Of-Sets-Large-Precategory :
  {l : Level} → UU l →
  Large-Precategory (λ l1 → l ⊔ lsuc l1) (λ l1 l2 → l ⊔ l1 ⊔ l2)
Family-Of-Sets-Large-Precategory A =
  Large-Function-Precategory A Set-Large-Precategory

The small precategory of families of sets over a type

Family-Of-Sets-Precategory :
  {l1 : Level} (l2 : Level) → UU l1 → Precategory (l1 ⊔ lsuc l2) (l1 ⊔ l2)
Family-Of-Sets-Precategory l2 A =
  precategory-Large-Precategory (Family-Of-Sets-Large-Precategory A) l2

The large category of families of sets over a type

module _
  {l : Level} (A : UU l)
  where

  Family-Of-Sets-Large-Category :
    Large-Category (λ l1 → l ⊔ lsuc l1) (λ l1 l2 → l ⊔ l1 ⊔ l2)
  Family-Of-Sets-Large-Category =
    Large-Function-Category A Set-Large-Category

  is-large-category-Family-Of-Sets-Large-Category :
    is-large-category-Large-Precategory (Family-Of-Sets-Large-Precategory A)
  is-large-category-Family-Of-Sets-Large-Category =
    is-large-category-Large-Category Family-Of-Sets-Large-Category

The small category of families of sets over a type

module _
  {l1 : Level} (l2 : Level) (A : UU l1)
  where

  Family-Of-Sets-Category : Category (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  Family-Of-Sets-Category =
    category-Large-Category (Family-Of-Sets-Large-Category A) l2

  is-category-Family-Of-Sets-Category :
    is-category-Precategory (Family-Of-Sets-Precategory l2 A)
  is-category-Family-Of-Sets-Category =
    is-category-Category Family-Of-Sets-Category

Recent changes