Smallness in cumulative large sets

Content created by Louis Wasserman.

Created on 2026-02-20.
Last modified on 2026-02-20.

module foundation.smallness-cumulative-large-sets where
Imports 
open import foundation.cumulative-large-sets
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.smallness-large-similarity-relations
open import foundation.universe-levels

Idea

Given a cumulative large set X, a value x : X l0 is small relative to a universe level l if it is similar to a value of X l.

Definition

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  (X : Cumulative-Large-Set α β)
  where

  is-small-prop-Cumulative-Large-Set :
    {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set X l0) →
    Prop (α l ⊔ β l0 l)
  is-small-prop-Cumulative-Large-Set =
    is-small-prop-Large-Similarity-Relation
      ( large-similarity-relation-Cumulative-Large-Set X)

  is-small-Cumulative-Large-Set :
    {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set X l0) →
    UU (α l ⊔ β l0 l)
  is-small-Cumulative-Large-Set l x =
    type-Prop (is-small-prop-Cumulative-Large-Set l x)

  is-prop-is-small-Cumulative-Large-Set :
    {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set X l0) →
    is-prop (is-small-Cumulative-Large-Set l x)
  is-prop-is-small-Cumulative-Large-Set =
    is-prop-is-small-Large-Similarity-Relation
      ( large-similarity-relation-Cumulative-Large-Set X)

Properties

An element is small relative to its own universe level

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  (X : Cumulative-Large-Set α β)
  where

  is-small-self-Cumulative-Large-Set :
    {l : Level} (x : type-Cumulative-Large-Set X l) →
    is-small-Cumulative-Large-Set X l x
  is-small-self-Cumulative-Large-Set x =
    ( x , refl-sim-Cumulative-Large-Set X x)

An element is small relative to any greater universe level

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  (X : Cumulative-Large-Set α β)
  where

  is-small-lub-level-Cumulative-Large-Set :
    {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set X l0) →
    is-small-Cumulative-Large-Set X (l0 ⊔ l) x
  is-small-lub-level-Cumulative-Large-Set l x =
    ( raise-Cumulative-Large-Set X l x ,
      sim-raise-Cumulative-Large-Set X l x)

Given x : X l0, x raised to another universe level is l0-small

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  (X : Cumulative-Large-Set α β)
  where

  is-small-raise-Cumulative-Large-Set :
    {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set X l0) →
    is-small-Cumulative-Large-Set X l0 (raise-Cumulative-Large-Set X l x)
  is-small-raise-Cumulative-Large-Set l x =
    ( x ,
      sim-raise-Cumulative-Large-Set' X l x)

Recent changes