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

open import category-theory.precategories
open import category-theory.slice-precategories

open import foundation.universe-levels

open import iterative.set.category

module iterative.set.category.slices where

-- Slice categories of V⁰
V⁰/ : {i : Level} → obj-Precategory (V⁰-Precategory i) → Precategory (lsuc i) i
V⁰/ {i} a = Slice-Precategory (V⁰-Precategory i) a