Locally small types

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

Created on 2022-02-17.
Last modified on 2024-03-12.

module foundation.locally-small-types where
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


A type is said to be locally small with respect to a universe UU l if its identity types are small with respect to that universe.


Locally small types

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)

module _
  {l l1 : Level} {A : UU l1} (H : is-locally-small l A) (x y : A)

  type-is-locally-small : UU l
  type-is-locally-small = pr1 (H x y)

  equiv-is-locally-small : (x  y)  type-is-locally-small
  equiv-is-locally-small = pr2 (H x y)

  inv-equiv-is-locally-small : type-is-locally-small  (x  y)
  inv-equiv-is-locally-small = inv-equiv equiv-is-locally-small

  map-equiv-is-locally-small : (x  y)  type-is-locally-small
  map-equiv-is-locally-small = map-equiv equiv-is-locally-small

  map-inv-equiv-is-locally-small : type-is-locally-small  (x  y)
  map-inv-equiv-is-locally-small = map-inv-equiv equiv-is-locally-small

The subuniverse of UU l1-locally small types in UU l2

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)

  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

  small-identity-type-Locally-Small-Type :
    (x y : type-Locally-Small-Type)  UU l1
  small-identity-type-Locally-Small-Type =
    type-is-locally-small is-locally-small-type-Locally-Small-Type

  equiv-is-locally-small-type-Locally-Small-Type :
    (x y : type-Locally-Small-Type) 
    (x  y)  small-identity-type-Locally-Small-Type x y
  equiv-is-locally-small-type-Locally-Small-Type =
    equiv-is-locally-small is-locally-small-type-Locally-Small-Type


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 =
    ( 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-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 =
    ( 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-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-inhabited-subtype-Prop)
    ( is-locally-small-subtype H)

See also


Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R Grayson. Symmetry. 06 2023. URL: https://unimath.github.io/SymmetryBook/book.pdf.
Egbert Rijke. The join construction. 01 2017. arXiv:1701.07538.

Recent changes