Wide function classes

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-10.
Last modified on 2023-08-23.

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 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.

Definition

is-wide-function-class :
  {l1 l2 : Level} → function-class l1 l1 l2 → UU (lsuc l1 ⊔ l2)
is-wide-function-class c =
  ( has-equivalences-function-class c) ×
  ( is-closed-under-composition-function-class c)

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)

Properties

is-wide-function-class-Prop :
  {l1 l2 : Level} → function-class l1 l1 l2 → Prop (lsuc l1 ⊔ l2)
is-wide-function-class-Prop c =
  prod-Prop
    ( has-equivalences-function-class-Prop c)
    ( is-closed-under-composition-function-class-Prop c)

is-prop-is-wide-function-class :
  {l1 l2 : Level} (c : function-class l1 l1 l2) →
  is-prop (is-wide-function-class c)
is-prop-is-wide-function-class = is-prop-type-Prop ∘ is-wide-function-class-Prop

Recent changes