Similarity-preserving maps on cumulative large sets

Content created by Louis Wasserman.

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

module foundation.similarity-preserving-maps-cumulative-large-sets where
Imports 
open import foundation.cumulative-large-sets
open import foundation.identity-types
open import foundation.similarity-preserving-maps-large-similarity-relations
open import foundation.universe-levels

Idea

Given cumulative large sets on X and Y, a map f : X → Y preserves similarity if whenever x₁ is similar to x₂ , f x₁ is similar to f x₂.

Definition

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

  preserves-sim-map-Cumulative-Large-Set :
    ( {l : Level} →
      type-Cumulative-Large-Set SX l →
      type-Cumulative-Large-Set SY l) → UUω
  preserves-sim-map-Cumulative-Large-Set f =
    preserves-sim-map-Large-Similarity-Relation
      ( large-similarity-relation-Cumulative-Large-Set SX)
      ( large-similarity-relation-Cumulative-Large-Set SY)
      ( f)

  sim-preserving-map-Cumulative-Large-Set : UUω
  sim-preserving-map-Cumulative-Large-Set =
    sim-preserving-map-Large-Similarity-Relation
      ( large-similarity-relation-Cumulative-Large-Set SX)
      ( large-similarity-relation-Cumulative-Large-Set SY)

  map-sim-preserving-map-Cumulative-Large-Set :
    sim-preserving-map-Cumulative-Large-Set →
    {l : Level} →
    type-Cumulative-Large-Set SX l → type-Cumulative-Large-Set SY l
  map-sim-preserving-map-Cumulative-Large-Set =
    map-sim-preserving-map-Large-Similarity-Relation

  preserves-sim-map-sim-preserving-map-Cumulative-Large-Set :
    (f : sim-preserving-map-Cumulative-Large-Set) →
    preserves-sim-map-Cumulative-Large-Set
      ( map-sim-preserving-map-Cumulative-Large-Set f)
  preserves-sim-map-sim-preserving-map-Cumulative-Large-Set =
    preserves-sim-map-sim-preserving-map-Large-Similarity-Relation

Similarity-preserving endomaps

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

  preserves-sim-endomap-Cumulative-Large-Set :
    ( {l : Level} →
      type-Cumulative-Large-Set SX l →
      type-Cumulative-Large-Set SX l) →
    UUω
  preserves-sim-endomap-Cumulative-Large-Set =
    preserves-sim-map-Cumulative-Large-Set SX SX

  sim-preserving-endomap-Cumulative-Large-Set : UUω
  sim-preserving-endomap-Cumulative-Large-Set =
    sim-preserving-map-Cumulative-Large-Set SX SX

  map-sim-preserving-endomap-Cumulative-Large-Set :
    sim-preserving-endomap-Cumulative-Large-Set →
    {l : Level} →
    type-Cumulative-Large-Set SX l → type-Cumulative-Large-Set SX l
  map-sim-preserving-endomap-Cumulative-Large-Set =
    map-sim-preserving-map-Large-Similarity-Relation

  preserves-sim-map-sim-preserving-endomap-Cumulative-Large-Set :
    (f : sim-preserving-endomap-Cumulative-Large-Set) →
    preserves-sim-endomap-Cumulative-Large-Set
      ( map-sim-preserving-endomap-Cumulative-Large-Set f)
  preserves-sim-map-sim-preserving-endomap-Cumulative-Large-Set =
    preserves-sim-map-sim-preserving-map-Large-Similarity-Relation

Properties

Similarity-preserving maps commute with raising universe levels

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

  abstract
    commute-map-raise-preserves-sim-map-Cumulative-Large-Set :
      ( f :
        {l : Level} →
        type-Cumulative-Large-Set SX l →
        type-Cumulative-Large-Set SY l) →
      preserves-sim-map-Cumulative-Large-Set SX SY f →
      {l1 : Level} (l2 : Level) (x : type-Cumulative-Large-Set SX l1) →
      f (raise-Cumulative-Large-Set SX l2 x) ＝
      raise-Cumulative-Large-Set SY l2 (f x)
    commute-map-raise-preserves-sim-map-Cumulative-Large-Set
      f preserves-sim-f {l1} l2 x =
      eq-sim-Cumulative-Large-Set SY _ _
        ( transitive-sim-Cumulative-Large-Set SY _ _ _
          ( sim-raise-Cumulative-Large-Set SY l2 (f x))
          ( preserves-sim-f _ _ (sim-raise-Cumulative-Large-Set' SX l2 x)))

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

  abstract
    commute-map-raise-sim-preserving-map-Cumulative-Large-Set :
      (f : sim-preserving-map-Cumulative-Large-Set SX SY)
      {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set SX l0) →
      map-sim-preserving-map-Cumulative-Large-Set SX SY
        ( f)
        ( raise-Cumulative-Large-Set SX l x) ＝
      raise-Cumulative-Large-Set SY
        ( l)
        ( map-sim-preserving-map-Cumulative-Large-Set SX SY f x)
    commute-map-raise-sim-preserving-map-Cumulative-Large-Set f =
      commute-map-raise-preserves-sim-map-Cumulative-Large-Set SX SY
        ( map-sim-preserving-map-Cumulative-Large-Set SX SY f)
        ( preserves-sim-map-sim-preserving-map-Cumulative-Large-Set SX SY f)

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

  abstract
    commute-map-raise-sim-preserving-endomap-Cumulative-Large-Set :
      (f : sim-preserving-endomap-Cumulative-Large-Set SX)
      {l0 : Level} (l : Level) (x : type-Cumulative-Large-Set SX l0) →
      map-sim-preserving-endomap-Cumulative-Large-Set SX
        ( f)
        ( raise-Cumulative-Large-Set SX l x) ＝
      raise-Cumulative-Large-Set SX
        ( l)
        ( map-sim-preserving-endomap-Cumulative-Large-Set SX f x)
    commute-map-raise-sim-preserving-endomap-Cumulative-Large-Set =
      commute-map-raise-sim-preserving-map-Cumulative-Large-Set SX SX

See also

Recent changes