# Locally small types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.

Created on 2022-02-17.

module foundation.locally-small-types where

Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.inhabited-subtypes
open import foundation.subuniverses
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.small-types
open import foundation-core.subtypes
open import foundation-core.transport-along-identifications
open import foundation-core.truncated-types
open import foundation-core.truncation-levels


## Idea

A type is said to be locally small if its identity types are small.

## Definition

is-locally-small :
(l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
is-locally-small l A = (x y : A) → is-small l (x ＝ y)


### The type of locally small types

Locally-Small-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Locally-Small-Type l1 l2 = Σ (UU l2) (is-locally-small l1)

module _
{l1 l2 : Level} (A : Locally-Small-Type l1 l2)
where

type-Locally-Small-Type : UU l2
type-Locally-Small-Type = pr1 A

is-locally-small-type-Locally-Small-Type :
is-locally-small l1 type-Locally-Small-Type
is-locally-small-type-Locally-Small-Type = pr2 A


## Properties

### Being locally small is a property

is-prop-is-locally-small :
(l : Level) {l1 : Level} (A : UU l1) → is-prop (is-locally-small l A)
is-prop-is-locally-small l A =
is-prop-Π (λ x → is-prop-Π (λ y → is-prop-is-small l (x ＝ y)))

is-locally-small-Prop :
(l : Level) {l1 : Level} (A : UU l1) → Prop (lsuc l ⊔ l1)
pr1 (is-locally-small-Prop l A) = is-locally-small l A
pr2 (is-locally-small-Prop l A) = is-prop-is-locally-small l A


### Any type in UU l is l-locally small

is-locally-small' : {l : Level} {A : UU l} → is-locally-small l A
is-locally-small' x y = is-small'


### Any small type is locally small

is-locally-small-is-small :
{l l1 : Level} {A : UU l1} → is-small l A → is-locally-small l A
pr1 (is-locally-small-is-small (X , e) x y) =
map-equiv e x ＝ map-equiv e y
pr2 (is-locally-small-is-small (X , e) x y) = equiv-ap e x y


### Any proposition is locally small

is-locally-small-is-prop :
(l : Level) {l1 : Level} {A : UU l1} → is-prop A → is-locally-small l A
is-locally-small-is-prop l H x y = is-small-is-contr l (H x y)


### Any univalent universe is locally small

is-locally-small-UU :
{l : Level} → is-locally-small l (UU l)
pr1 (is-locally-small-UU X Y) = X ≃ Y
pr2 (is-locally-small-UU X Y) = equiv-univalence


### Any Σ-type of locally small types is locally small

is-locally-small-Σ :
{l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} →
is-locally-small l3 A → ((x : A) → is-locally-small l4 (B x)) →
is-locally-small (l3 ⊔ l4) (Σ A B)
is-locally-small-Σ {B = B} H K x y =
is-small-equiv
( Eq-Σ x y)
( equiv-pair-eq-Σ x y)
( is-small-Σ
( H (pr1 x) (pr1 y))
( λ p → K (pr1 y) (tr B p (pr2 x)) (pr2 y)))

Σ-Locally-Small-Type :
{l1 l2 l3 l4 : Level} (A : Locally-Small-Type l1 l2) →
(type-Locally-Small-Type A → Locally-Small-Type l3 l4) →
Locally-Small-Type (l1 ⊔ l3) (l2 ⊔ l4)
pr1 (Σ-Locally-Small-Type A B) =
Σ (type-Locally-Small-Type A) (type-Locally-Small-Type ∘ B)
pr2 (Σ-Locally-Small-Type A B) =
is-locally-small-Σ
( is-locally-small-type-Locally-Small-Type A)
( is-locally-small-type-Locally-Small-Type ∘ B)


### The underlying type of a subtype of a locally small type is locally small

is-locally-small-type-subtype :
{l1 l2 l3 : Level} {A : UU l1} (P : subtype l2 A) →
is-locally-small l3 A → is-locally-small l3 (type-subtype P)
is-locally-small-type-subtype {l3 = l3} P H =
is-locally-small-Σ H
( λ a → is-locally-small-is-prop l3 (is-prop-is-in-subtype P a))

type-subtype-Locally-Small-Type :
{l1 l2 l3 : Level} (A : Locally-Small-Type l1 l2) →
subtype l3 (type-Locally-Small-Type A) → Locally-Small-Type l1 (l2 ⊔ l3)
pr1 (type-subtype-Locally-Small-Type A P) = type-subtype P
pr2 (type-subtype-Locally-Small-Type A P) =
is-locally-small-type-subtype P (is-locally-small-type-Locally-Small-Type A)


### Any product of locally small types indexed by a small type is small

is-locally-small-Π :
{l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} →
is-small l3 A → ((x : A) → is-locally-small l4 (B x)) →
is-locally-small (l3 ⊔ l4) ((x : A) → B x)
is-locally-small-Π H K f g =
is-small-equiv
( f ~ g)
( equiv-funext)
( is-small-Π H (λ x → K x (f x) (g x)))

Π-Locally-Small-Type :
{l1 l2 l3 l4 : Level} (A : Small-Type l1 l2) →
(type-Small-Type A → Locally-Small-Type l3 l4) →
Locally-Small-Type (l1 ⊔ l3) (l2 ⊔ l4)
pr1 (Π-Locally-Small-Type A B) =
(a : type-Small-Type A) → type-Locally-Small-Type (B a)
pr2 (Π-Locally-Small-Type A B) =
is-locally-small-Π
( is-small-type-Small-Type A)
( is-locally-small-type-Locally-Small-Type ∘ B)


### The type of types in any given subuniverse is locally small

is-locally-small-type-subuniverse :
{l1 l2 : Level} (P : subuniverse l1 l2) →
is-locally-small l1 (type-subuniverse P)
is-locally-small-type-subuniverse P =
is-locally-small-type-subtype P is-locally-small-UU


### The type of locally small types is locally small

is-locally-small-Locally-Small-Type :
{l1 l2 : Level} → is-locally-small l2 (Locally-Small-Type l1 l2)
is-locally-small-Locally-Small-Type {l1} =
is-locally-small-type-subuniverse (is-locally-small-Prop l1)


### The type of truncated types is locally small

is-locally-small-Truncated-Type :
{l : Level} (k : 𝕋) → is-locally-small l (Truncated-Type l k)
is-locally-small-Truncated-Type k =
is-locally-small-type-subuniverse (is-trunc-Prop k)


### The type of propositions is locally small

is-locally-small-type-Prop :
{l : Level} → is-locally-small l (Prop l)
is-locally-small-type-Prop = is-locally-small-Truncated-Type neg-one-𝕋


### The type of subtypes of a small type is locally small

is-locally-small-subtype :
{l1 l2 l3 : Level} {A : UU l1} →
is-small l2 A → is-locally-small (l2 ⊔ l3) (subtype l3 A)
is-locally-small-subtype H =
is-locally-small-Π H (λ _ → is-locally-small-type-Prop)


### The type of inhabited subtypes of a small type is locally small

is-locally-small-inhabited-subtype :
{l1 l2 l3 : Level} {A : UU l1} →
is-small l2 A → is-locally-small (l2 ⊔ l3) (inhabited-subtype l3 A)
is-locally-small-inhabited-subtype H =
is-locally-small-type-subtype
( is-inhabited-subtype-Prop)
( is-locally-small-subtype H)