# The category of families of sets

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-28.

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