This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Sequentially compact types

module synthetic-homotopy-theory.sequentially-compact-types where

open import foundation.propositions
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams
open import synthetic-homotopy-theory.universal-property-sequential-colimits

Idea

A sequentially compact type is a type X such that exponentiating by X commutes with sequential colimits

  colimₙ (X → Aₙ) ≃ (X → colimₙ Aₙ)

for every cotower Aₙ.

Definitions

The predicate of being a sequentially compact type

module _
  {l1 : Level} (X : UU l1)
  where

  is-sequentially-compact : UUω
  is-sequentially-compact =
    {l2 l3 : Level} (A : sequential-diagram l2) {A∞ : UU l3}
    (c : cocone-sequential-diagram A A∞) →
    universal-property-sequential-colimit c →
    universal-property-sequential-colimit
      ( cocone-postcomp-sequential-diagram X A c)

References

[Rij19]

Egbert Rijke. Classifying Types. PhD thesis, Carnegie Mellon University, 06 2019. arXiv:1906.09435.