The category of connected set bundles over the circle

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.
Last modified on 2023-11-27.

module synthetic-homotopy-theory.category-of-connected-set-bundles-circle where
Imports 
open import category-theory.full-large-subcategories
open import category-theory.large-categories

open import foundation.category-of-families-of-sets
open import foundation.universe-levels

open import synthetic-homotopy-theory.circle
open import synthetic-homotopy-theory.connected-set-bundles-circle

Idea

The connected set bundles over the circle form a large category. This large category is the categorification of the poset of the natural numbers ordered by divisibility.

Definitions

The category of connected set bundles over the circle

connected-set-bundle-𝕊¹-Large-Category : Large-Category (lsuc) (_⊔_)
connected-set-bundle-𝕊¹-Large-Category =
  large-category-Full-Large-Subcategory
    ( Family-Of-Sets-Large-Category 𝕊¹)
    ( is-connected-prop-set-bundle-𝕊¹)

Recent changes