{-# OPTIONS --without-K --rewriting #-}

open import category-theory.functors-precategories
open import category-theory.precategories

open import foundation.category-of-sets
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import iterative.set

module iterative.set.category where

V⁰-Precategory : ∀ i → Precategory (lsuc i) i
pr1 (V⁰-Precategory i) = V⁰ i
pr1 (pr2 (V⁰-Precategory i)) x y = hom-set-Set (El⁰-Set i x) (El⁰-Set i y)
pr1 (pr1 (pr2 (pr2 (V⁰-Precategory i)))) g f = g ∘ f
pr2 (pr1 (pr2 (pr2 (V⁰-Precategory i)))) h g f = (refl , refl)
pr1 (pr2 (pr2 (pr2 (V⁰-Precategory i)))) x = id
pr1 (pr2 (pr2 (pr2 (pr2 (V⁰-Precategory i))))) f = refl
pr2 (pr2 (pr2 (pr2 (pr2 (V⁰-Precategory i))))) f = refl

-- Functor from V⁰-Precategory to Set-Precategory
functor-V⁰-Set : ∀ i → functor-Precategory (V⁰-Precategory i) (Set-Precategory i)
pr1 (functor-V⁰-Set i) = El⁰-Set i
pr1 (pr2 (functor-V⁰-Set i)) = id
pr1 (pr2 (pr2 (functor-V⁰-Set i))) g f = refl
pr2 (pr2 (pr2 (functor-V⁰-Set i))) x = refl