Sequentially compact types

Content created by Fredrik Bakke and Vojtěch Štěpančík.

Created on 2023-11-27.
Last modified on 2024-03-12.

module synthetic-homotopy-theory.sequentially-compact-types where
Imports 
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.

Recent changes