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
- 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-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-10. Fredrik Bakke. Define orthogonal factorization systems (#482).