# Σ-closed subuniverses

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-28.

module foundation.sigma-closed-subuniverses where

Imports
open import foundation.dependent-pair-types
open import foundation.subuniverses
open import foundation.universe-levels

open import foundation-core.function-types


## Idea

A subuniverse P is Σ-closed if it is closed under the formation of Σ-types. Meaning P is Σ-closed if Σ A B is in P whenever B is a family of types in P over a type A in P.

## Definition

We state a general form involving three universes, and a more traditional form using a single universe

is-closed-under-Σ-subuniverses :
{l1 l2 lP lQ lR : Level}
(P : subuniverse l1 lP)
(Q : subuniverse l2 lQ)
(R : subuniverse (l1 ⊔ l2) lR) →
UU (lsuc l1 ⊔ lsuc l2 ⊔ lP ⊔ lQ ⊔ lR)
is-closed-under-Σ-subuniverses P Q R =
(X : type-subuniverse P)
(Y : inclusion-subuniverse P X → type-subuniverse Q) →
is-in-subuniverse R
( Σ (inclusion-subuniverse P X) (inclusion-subuniverse Q ∘ Y))

is-closed-under-Σ-subuniverse :
{l lP : Level} → subuniverse l lP → UU (lsuc l ⊔ lP)
is-closed-under-Σ-subuniverse P = is-closed-under-Σ-subuniverses P P P

closed-under-Σ-subuniverse :
(l lP : Level) → UU (lsuc l ⊔ lsuc lP)
closed-under-Σ-subuniverse l lP =
Σ (subuniverse l lP) (is-closed-under-Σ-subuniverse)