Function classes
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.
Created on 2023-03-10.
Last modified on 2023-09-11.
module orthogonal-factorization-systems.function-classes where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.identity-types open import foundation.propositions open import foundation.pullback-squares open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels
Idea
A function class is a subtype of the type of all functions in a given universe.
Definitions
function-class : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) function-class l1 l2 l3 = {A : UU l1} {B : UU l2} → (A → B) → Prop l3
Function classes containing identities or equivalences
has-identity-maps-function-class : {l1 l2 : Level} → function-class l1 l1 l2 → UU (lsuc l1 ⊔ l2) has-identity-maps-function-class {l1} {l2} c = (A : UU l1) → type-Prop (c (id {A = A})) identity-maps-function-class : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) identity-maps-function-class l1 l2 = Σ (function-class l1 l1 l2) (has-identity-maps-function-class) has-equivalences-function-class : {l1 l2 l3 : Level} → function-class l1 l2 l3 → UU (lsuc l1 ⊔ lsuc l2 ⊔ l3) has-equivalences-function-class {l1} {l2} c = (A : UU l1) (B : UU l2) (f : A → B) → is-equiv f → type-Prop (c f) equivalences-function-class : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) equivalences-function-class l1 l2 l3 = Σ (function-class l1 l2 l3) (has-equivalences-function-class)
Composition closed function classes
We say a function class is composition closed if it is closed under taking composites.
is-closed-under-composition-function-class : {l1 l2 : Level} → function-class l1 l1 l2 → UU (lsuc l1 ⊔ l2) is-closed-under-composition-function-class {l1} {l2} c = (A B C : UU l1) (f : A → B) (g : B → C) → type-Prop (c f) → type-Prop (c g) → type-Prop (c (g ∘ f)) composition-closed-function-class : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) composition-closed-function-class l1 l2 = Σ (function-class l1 l1 l2) (is-closed-under-composition-function-class)
Pullback-stable function classes
A function class is said to be pullback-stable if given a function in it, then its pullback along any map is also in the function class.
is-pullback-stable-function-class : {l1 l2 l3 : Level} (l : Level) → function-class l1 l2 l3 → UU (lsuc l1 ⊔ lsuc l2 ⊔ l3 ⊔ lsuc l) is-pullback-stable-function-class {l1} {l2} l F = (A : UU l1) (B C : UU l2) (f : A → C) (g : B → C) (c : Σ (UU l1) (pullback-cone l f g)) → type-Prop (F f) → type-Prop (F (horizontal-map-pullback-cone f g (pr2 c))) pullback-stable-function-class : (l1 l2 l3 l4 : Level) → UU (lsuc (l1 ⊔ l2 ⊔ l3 ⊔ l4)) pullback-stable-function-class l1 l2 l3 l4 = Σ (function-class l1 l2 l3) (is-pullback-stable-function-class l4)
Properties
Having identities is a property
has-identity-maps-function-class-Prop : {l1 l2 : Level} → function-class l1 l1 l2 → Prop (lsuc l1 ⊔ l2) has-identity-maps-function-class-Prop {l1} {l2} c = Π-Prop (UU l1) λ A → c (id {A = A}) is-prop-has-identity-maps-function-class : {l1 l2 : Level} (c : function-class l1 l1 l2) → is-prop (has-identity-maps-function-class c) is-prop-has-identity-maps-function-class = is-prop-type-Prop ∘ has-identity-maps-function-class-Prop
Having equivalences is a property
has-equivalences-function-class-Prop : {l1 l2 l3 : Level} → function-class l1 l2 l3 → Prop (lsuc l1 ⊔ lsuc l2 ⊔ l3) has-equivalences-function-class-Prop {l1} {l2} {l3} c = Π-Prop (UU l1) λ A → Π-Prop (UU l2) λ B → Π-Prop (A → B) ( λ f → function-Prop (is-equiv f) (c f)) is-prop-has-equivalences-function-class : {l1 l2 l3 : Level} (c : function-class l1 l2 l3) → is-prop (has-equivalences-function-class c) is-prop-has-equivalences-function-class = is-prop-type-Prop ∘ has-equivalences-function-class-Prop
Composition closedness is a property
is-prop-is-closed-under-composition-function-class : {l1 l2 : Level} (c : function-class l1 l1 l2) → is-prop (is-closed-under-composition-function-class c) is-prop-is-closed-under-composition-function-class c = is-prop-Π λ A → is-prop-Π λ B → is-prop-Π λ C → is-prop-Π λ f → is-prop-Π λ g → is-prop-function-type (is-prop-function-type ( is-prop-type-Prop (c (g ∘ f)))) is-closed-under-composition-function-class-Prop : {l1 l2 : Level} → function-class l1 l1 l2 → Prop (lsuc l1 ⊔ l2) pr1 (is-closed-under-composition-function-class-Prop c) = is-closed-under-composition-function-class c pr2 (is-closed-under-composition-function-class-Prop c) = is-prop-is-closed-under-composition-function-class c
Being pullback-stable is a property
is-prop-is-pullback-stable-function-class : {l1 l2 l3 : Level} (l : Level) (F : function-class l1 l2 l3) → is-prop (is-pullback-stable-function-class l F) is-prop-is-pullback-stable-function-class l F = is-prop-Π λ A → is-prop-Π λ B → is-prop-Π λ C → is-prop-Π λ f → is-prop-Π λ g → is-prop-Π λ c → is-prop-function-type ( is-prop-type-Prop (F (horizontal-map-pullback-cone f g (pr2 c)))) is-pullback-stable-function-class-Prop : {l1 l2 l3 : Level} (l : Level) (F : function-class l1 l2 l3) → Prop (lsuc l1 ⊔ lsuc l2 ⊔ l3 ⊔ lsuc l) pr1 (is-pullback-stable-function-class-Prop l F) = is-pullback-stable-function-class l F pr2 (is-pullback-stable-function-class-Prop l F) = is-prop-is-pullback-stable-function-class l F
Having equivalences is equivalent to having identity maps
This is a consequence of univalence.
module _ {l1 l2 : Level} (F : function-class l1 l1 l2) where has-identity-maps-has-equivalences-function-class : has-equivalences-function-class F → has-identity-maps-function-class F has-identity-maps-has-equivalences-function-class has-equivs-F A = has-equivs-F A A id is-equiv-id htpy-has-identity-maps-function-class : has-identity-maps-function-class F → {X Y : UU l1} → (p : X = Y) → type-Prop (F (map-eq p)) htpy-has-identity-maps-function-class has-ids-F {X} refl = has-ids-F X has-equivalence-has-identity-maps-function-class : has-identity-maps-function-class F → {X Y : UU l1} (e : X ≃ Y) → type-Prop (F (map-equiv e)) has-equivalence-has-identity-maps-function-class has-ids-F {X} {Y} e = tr ( type-Prop ∘ F) ( ap pr1 (is-section-eq-equiv e)) ( htpy-has-identity-maps-function-class has-ids-F (eq-equiv X Y e)) has-equivalences-has-identity-maps-function-class : has-identity-maps-function-class F → has-equivalences-function-class F has-equivalences-has-identity-maps-function-class has-ids-F A B f is-equiv-f = has-equivalence-has-identity-maps-function-class has-ids-F (f , is-equiv-f) is-equiv-has-identity-maps-has-equivalences-function-class : is-equiv has-identity-maps-has-equivalences-function-class is-equiv-has-identity-maps-has-equivalences-function-class = is-equiv-is-prop ( is-prop-has-equivalences-function-class F) ( is-prop-has-identity-maps-function-class F) ( has-equivalences-has-identity-maps-function-class) equiv-has-identity-maps-has-equivalences-function-class : has-equivalences-function-class F ≃ has-identity-maps-function-class F pr1 equiv-has-identity-maps-has-equivalences-function-class = has-identity-maps-has-equivalences-function-class pr2 equiv-has-identity-maps-has-equivalences-function-class = is-equiv-has-identity-maps-has-equivalences-function-class is-equiv-has-equivalences-has-identity-maps-function-class : is-equiv has-equivalences-has-identity-maps-function-class is-equiv-has-equivalences-has-identity-maps-function-class = is-equiv-is-prop ( is-prop-has-identity-maps-function-class F) ( is-prop-has-equivalences-function-class F) ( has-identity-maps-has-equivalences-function-class) equiv-has-equivalences-has-identity-maps-function-class : has-identity-maps-function-class F ≃ has-equivalences-function-class F pr1 equiv-has-equivalences-has-identity-maps-function-class = has-equivalences-has-identity-maps-function-class pr2 equiv-has-equivalences-has-identity-maps-function-class = is-equiv-has-equivalences-has-identity-maps-function-class
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-08-23. Fredrik Bakke. Pre-commit fixes and some miscellaneous changes (#705).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).