Locally small modal-operators

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-28.
Last modified on 2023-09-15.

module orthogonal-factorization-systems.locally-small-modal-operators where
open import foundation.dependent-pair-types
open import foundation.locally-small-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators


A modal operator is locally small if it maps small types to locally small types.


Locally small modal operators

is-locally-small-operator-modality :
  {l1 l2 : Level} (l3 : Level) ( : operator-modality l1 l2) 
  UU (lsuc l1  l2  lsuc l3)
is-locally-small-operator-modality {l1} l3  =
  (X : UU l1)  is-locally-small l3 ( X)

locally-small-operator-modality :
  (l1 l2 l3 : Level)  UU (lsuc l1  lsuc l2  lsuc l3)
locally-small-operator-modality l1 l2 l3 =
  Σ ( operator-modality l1 l2)
    ( is-locally-small-operator-modality l3)

operator-modality-locally-small-operator-modality :
  {l1 l2 l3 : Level} 
  locally-small-operator-modality l1 l2 l3  operator-modality l1 l2
operator-modality-locally-small-operator-modality = pr1

is-locally-small-locally-small-operator-modality :
  {l1 l2 l3 : Level} ( : locally-small-operator-modality l1 l2 l3) 
  is-locally-small-operator-modality l3
    ( operator-modality-locally-small-operator-modality )
is-locally-small-locally-small-operator-modality = pr2

Recent changes