# Locally small modal-operators

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-28.

module orthogonal-factorization-systems.locally-small-modal-operators where

Imports
open import foundation.dependent-pair-types
open import foundation.locally-small-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators


## Idea

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

## Definitions

### 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