Smallness relative to large similarity relations

Content created by Louis Wasserman.

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

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

Idea

Given a large similarity relation R on a family of types X stratified by universe levels, a value x : X l0 is small relative to a universe level l if it is similar to a value in X l.

Definition

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  {X : (l : Level) → UU (α l)}
  (R : Large-Similarity-Relation β X)
  where

  is-small-Large-Similarity-Relation :
    {l0 : Level} (l : Level) → X l0 → UU (α l ⊔ β l0 l)
  is-small-Large-Similarity-Relation l x =
    Σ (X l) (sim-Large-Similarity-Relation R x)

Properties

Being small relative to a universe level is a proposition

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  {X : (l : Level) → UU (α l)}
  (R : Large-Similarity-Relation β X)
  {l0 : Level}
  (l : Level)
  (x : X l0)
  where

  abstract
    all-elements-equal-is-small-Large-Similarity-Relation :
      all-elements-equal (is-small-Large-Similarity-Relation R l x)
    all-elements-equal-is-small-Large-Similarity-Relation (y , Rxy) (z , Rxz) =
      eq-type-subtype
        ( sim-prop-Large-Similarity-Relation R x)
        ( eq-sim-Large-Similarity-Relation R y z
          ( transitive-sim-Large-Similarity-Relation R y x z
            ( Rxz)
            ( symmetric-sim-Large-Similarity-Relation R x y Rxy)))

    is-prop-is-small-Large-Similarity-Relation :
      is-prop (is-small-Large-Similarity-Relation R l x)
    is-prop-is-small-Large-Similarity-Relation =
      is-prop-all-elements-equal
        ( all-elements-equal-is-small-Large-Similarity-Relation)

  is-small-prop-Large-Similarity-Relation : Prop (α l ⊔ β l0 l)
  is-small-prop-Large-Similarity-Relation =
    ( is-small-Large-Similarity-Relation R l x ,
      is-prop-is-small-Large-Similarity-Relation)

Properties

A value is small relative to its own universe level

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  {X : (l : Level) → UU (α l)}
  (R : Large-Similarity-Relation β X)
  where

  is-small-self-Large-Similarity-Relation :
    {l : Level} (x : X l) →
    is-small-Large-Similarity-Relation R l x
  is-small-self-Large-Similarity-Relation x =
    ( x , refl-sim-Large-Similarity-Relation R x)

See also

Recent changes