Wide function classes

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-10.
Last modified on 2024-02-06.

module orthogonal-factorization-systems.wide-function-classes where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.propositions
open import foundation.universe-levels

open import orthogonal-factorization-systems.function-classes

Idea

We say a (small) function class is wide if it contains all equivalences and is composition closed. This means it is morally a wide sub-∞-category of the ∞-category of types at a fixed universe level.

Definition

The predicate on small function classes of being wide

module _
  {l1 l2 : Level} (P : function-class l1 l1 l2)
  where

  is-wide-function-class : UU (lsuc l1 ⊔ l2)
  is-wide-function-class =
    ( has-equivalences-function-class P) ×
    ( is-closed-under-composition-function-class P)

  is-wide-function-class-Prop : Prop (lsuc l1 ⊔ l2)
  is-wide-function-class-Prop =
    product-Prop
      ( has-equivalences-function-class-Prop P)
      ( is-closed-under-composition-function-class-Prop P)

  is-prop-is-wide-function-class : is-prop is-wide-function-class
  is-prop-is-wide-function-class = is-prop-type-Prop is-wide-function-class-Prop

  has-equivalences-is-wide-function-class :
    is-wide-function-class → has-equivalences-function-class P
  has-equivalences-is-wide-function-class = pr1

  is-closed-under-composition-is-wide-function-class :
    is-wide-function-class → is-closed-under-composition-function-class P
  is-closed-under-composition-is-wide-function-class = pr2

The type of small wide function classes

wide-function-class : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
wide-function-class l1 l2 =
  Σ (function-class l1 l1 l2) (is-wide-function-class)

module _
  {l1 l2 : Level} (P : wide-function-class l1 l2)
  where

  function-class-wide-function-class : function-class l1 l1 l2
  function-class-wide-function-class = pr1 P

  is-wide-wide-function-class :
    is-wide-function-class function-class-wide-function-class
  is-wide-wide-function-class = pr2 P

  has-equivalences-wide-function-class :
    has-equivalences-function-class function-class-wide-function-class
  has-equivalences-wide-function-class =
    has-equivalences-is-wide-function-class
      ( function-class-wide-function-class)
      ( is-wide-wide-function-class)

  is-closed-under-composition-wide-function-class :
    is-closed-under-composition-function-class
      ( function-class-wide-function-class)
  is-closed-under-composition-wide-function-class =
    is-closed-under-composition-is-wide-function-class
      ( function-class-wide-function-class)
      ( is-wide-wide-function-class)

Recent changes