# Global function classes

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-24.

module orthogonal-factorization-systems.global-function-classes where

Imports
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-types
open import foundation.propositions
open import foundation.pullbacks
open import foundation.subtypes
open import foundation.universe-levels

open import orthogonal-factorization-systems.function-classes


## Idea

A global function class is a global subtype of function types that is closed under composition with equivalences.

Note that composition with homogenous equivalences follows from univalence, so this condition should hold for the correct universe polymorphic definition.

## Definitions

### The predicate on families of function classes of being closed under composition with equivalences

module _
{β : Level → Level → Level}
(P : {l1 l2 : Level} {A : UU l1} {B : UU l2} → subtype (β l1 l2) (A → B))
where

is-closed-under-equiv-precomp-function-classes :
(l1 l2 l3 : Level) → UU (β l1 l2 ⊔ β l3 l2 ⊔ lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
is-closed-under-equiv-precomp-function-classes l1 l2 l3 =
{A : UU l1} {B : UU l2} {C : UU l3} (f : A → B) → is-in-subtype P f →
(e : C ≃ A) → is-in-subtype P (f ∘ map-equiv e)

is-closed-under-equiv-postcomp-function-classes :
(l1 l2 l3 : Level) → UU (β l1 l2 ⊔ β l1 l3 ⊔ lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
is-closed-under-equiv-postcomp-function-classes l1 l2 l3 =
{A : UU l1} {B : UU l2} {C : UU l3} (f : A → B) → is-in-subtype P f →
(e : B ≃ C) → is-in-subtype P (map-equiv e ∘ f)


### The large type of global function classes

record global-function-class (β : Level → Level → Level) : UUω where
field
function-class-global-function-class :
{l1 l2 : Level} → function-class l1 l2 (β l1 l2)

is-closed-under-equiv-precomp-global-function-class :
{l1 l2 l3 : Level} →
is-closed-under-equiv-precomp-function-classes
( function-class-global-function-class)
l1 l2 l3

is-closed-under-equiv-postcomp-global-function-class :
{l1 l2 l3 : Level} →
is-closed-under-equiv-postcomp-function-classes
( function-class-global-function-class)
l1 l2 l3

open global-function-class public

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

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

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

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

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

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

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


### Global function classes containing identities

module _
{β : Level → Level → Level} (P : global-function-class β)
where

has-identity-maps-global-function-class-Level :
(l : Level) → UU (β l l ⊔ lsuc l)
has-identity-maps-global-function-class-Level l =
(A : UU l) → is-in-global-function-class P (id {A = A})

has-identity-maps-global-function-class : UUω
has-identity-maps-global-function-class =
{l : Level} → has-identity-maps-global-function-class-Level l


### Global function classes containing equivalences

module _
{β : Level → Level → Level} (P : global-function-class β)
where

has-equivalences-global-function-class-Level :
(l1 l2 : Level) → UU (β l1 l2 ⊔ lsuc l1 ⊔ lsuc l2)
has-equivalences-global-function-class-Level l1 l2 =
{A : UU l1} {B : UU l2} (f : A → B) →
is-equiv f → is-in-global-function-class P f

has-equivalences-global-function-class : UUω
has-equivalences-global-function-class =
{l1 l2 : Level} → has-equivalences-global-function-class-Level l1 l2


Note: The previous two conditions are equivalent by the closure property of global function classes.

### Composition closed function classes

We say a function class is composition closed if it is closed under taking composites.

module _
{β : Level → Level → Level} (P : global-function-class β)
where

is-closed-under-composition-global-function-class-Level :
(l1 l2 l3 : Level) →
UU (β l1 l2 ⊔ β l1 l3 ⊔ β l2 l3 ⊔ lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
is-closed-under-composition-global-function-class-Level l1 l2 l3 =
{A : UU l1} {B : UU l2} {C : UU l3} {g : B → C} {f : A → B} →
is-in-global-function-class P g →
is-in-global-function-class P f →
is-in-global-function-class P (g ∘ f)

is-closed-under-composition-global-function-class : UUω
is-closed-under-composition-global-function-class =
{l1 l2 l3 : Level} →
is-closed-under-composition-global-function-class-Level l1 l2 l3


## Pullback-stable global function classes

A global function class is said to be pullback-stable if given a function in it, its pullback along any map is also in the global function class.

module _
{β : Level → Level → Level} (P : global-function-class β)
where

is-pullback-stable-global-function-class-Level :
(l1 l2 l3 l4 : Level) →
UU (β l1 l3 ⊔ β l4 l2 ⊔ lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3 ⊔ lsuc l4)
is-pullback-stable-global-function-class-Level l1 l2 l3 l4 =
{A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (f : A → C) (g : B → C)
(c : cone f g X) (p : is-pullback f g c) →
is-in-global-function-class P f →
is-in-global-function-class P (horizontal-map-cone f g c)

is-pullback-stable-global-function-class : UUω
is-pullback-stable-global-function-class =
{l1 l2 l3 l4 : Level} →
is-pullback-stable-global-function-class-Level l1 l2 l3 l4


## Properties

### Having identities is equivalent to having equivalences

This follows from either of the closure properties of global function classes.

module _
{β : Level → Level → Level} (P : global-function-class β)
where

has-equivalences-has-identity-maps-global-function-class :
has-identity-maps-global-function-class P →
has-equivalences-global-function-class P
has-equivalences-has-identity-maps-global-function-class
has-id-P {B = B} f f' =
is-closed-under-equiv-precomp-global-function-class
P id (has-id-P B) (f , f')

has-equivalences-has-identity-maps-global-function-class' :
has-identity-maps-global-function-class P →
has-equivalences-global-function-class P
has-equivalences-has-identity-maps-global-function-class'
has-id-P {A = A} f f' =
is-closed-under-equiv-postcomp-global-function-class
P id (has-id-P A) (f , f')

has-identity-maps-has-equivalences-global-function-class :
has-equivalences-global-function-class P →
has-identity-maps-global-function-class P
has-identity-maps-has-equivalences-global-function-class has-equiv-P A =
has-equiv-P id is-equiv-id