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

The category of connected set bundles over the circle

module synthetic-homotopy-theory.category-of-connected-set-bundles-circle where

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-𝕊¹)