Wide global function classes

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-11-24.

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

open import orthogonal-factorization-systems.function-classes
open import orthogonal-factorization-systems.global-function-classes

Idea

We say a global 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

record wide-global-function-class (β : Level → Level → Level) : UUω where
  field

    global-function-class-wide-global-function-class :
      global-function-class β

    has-equivalences-wide-global-function-class :
      has-equivalences-global-function-class
        global-function-class-wide-global-function-class

    is-closed-under-composition-wide-global-function-class :
      is-closed-under-composition-global-function-class
        global-function-class-wide-global-function-class

open wide-global-function-class public

function-class-wide-global-function-class :
  {β : Level → Level → Level} (P : wide-global-function-class β) →
  {l1 l2 : Level} → function-class l1 l2 (β l1 l2)
function-class-wide-global-function-class P =
  function-class-global-function-class
    ( global-function-class-wide-global-function-class P)

type-wide-global-function-class :
  {β : Level → Level → Level} (P : wide-global-function-class β)
  {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (β l1 l2 ⊔ l1 ⊔ l2)
type-wide-global-function-class P =
  type-function-class (function-class-wide-global-function-class P)

module _
  {β : Level → Level → Level} (P : wide-global-function-class β)
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-in-wide-global-function-class : (A → B) → UU (β l1 l2)
  is-in-wide-global-function-class =
    is-in-function-class (function-class-wide-global-function-class P)

  is-prop-is-in-wide-global-function-class :
    (f : A → B) → is-prop (is-in-wide-global-function-class f)
  is-prop-is-in-wide-global-function-class =
    is-prop-is-in-function-class (function-class-wide-global-function-class P)

  inclusion-wide-global-function-class :
    type-wide-global-function-class P A B → A → B
  inclusion-wide-global-function-class =
    inclusion-function-class (function-class-wide-global-function-class P)

  is-emb-inclusion-wide-global-function-class :
    is-emb inclusion-wide-global-function-class
  is-emb-inclusion-wide-global-function-class =
    is-emb-inclusion-function-class
      ( function-class-wide-global-function-class P)

  emb-wide-global-function-class :
    type-wide-global-function-class P A B ↪ (A → B)
  emb-wide-global-function-class =
    emb-function-class (function-class-wide-global-function-class P)

Recent changes