Factorization operations into function classes
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-05-09.
Last modified on 2023-06-29.
module orthogonal-factorization-systems.factorization-operations-function-classes where
Imports
open import foundation.contractible-types open import foundation.function-types open import foundation.inhabited-types open import foundation.propositions open import foundation.universe-levels open import orthogonal-factorization-systems.factorizations-of-maps open import orthogonal-factorization-systems.function-classes
Idea
A factorization operation into function classes L
and R
is a
factorization operation
such that the left map (in diagrammatic order) of every
factorization is
in L
, and the right map is in R
.
∙
^ \
L ∋ / \ ∈ R
/ v
A -----> B
Definition
module _ {l1 l2 lF lL lR : Level} (L : function-class l1 lF lL) (R : function-class lF l2 lR) (A : UU l1) (B : UU l2) where factorization-operation-function-class : UU (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR) factorization-operation-function-class = (f : A → B) → factorization-function-class L R f mere-factorization-property-function-class : UU (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR) mere-factorization-property-function-class = (f : A → B) → is-inhabited (factorization-function-class L R f) unique-factorization-operation-function-class : UU (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR) unique-factorization-operation-function-class = (f : A → B) → is-contr (factorization-function-class L R f)
Properties
A mere function class factorization property is a property
module _ {l1 l2 lF lL lR : Level} (L : function-class l1 lF lL) (R : function-class lF l2 lR) {A : UU l1} {B : UU l2} where mere-factorization-property-function-class-Prop : Prop (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR) mere-factorization-property-function-class-Prop = Π-Prop (A → B) (is-inhabited-Prop ∘ factorization-function-class L R) is-prop-mere-factorization-property-function-class : is-prop (mere-factorization-property-function-class L R A B) is-prop-mere-factorization-property-function-class = is-prop-type-Prop mere-factorization-property-function-class-Prop
Having a unique function class factorization operation is a property
module _ {l1 l2 lF lL lR : Level} (L : function-class l1 lF lL) (R : function-class lF l2 lR) {A : UU l1} {B : UU l2} where unique-factorization-operation-function-class-Prop : Prop (l1 ⊔ l2 ⊔ lsuc lF ⊔ lL ⊔ lR) unique-factorization-operation-function-class-Prop = Π-Prop (A → B) (is-contr-Prop ∘ factorization-function-class L R) is-prop-unique-factorization-operation-function-class : is-prop (unique-factorization-operation-function-class L R A B) is-prop-unique-factorization-operation-function-class = is-prop-type-Prop unique-factorization-operation-function-class-Prop
Recent changes
- 2023-06-29. Fredrik Bakke. Fix hyperlinks (#677).
- 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-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-05-09. Fredrik Bakke and Egbert Rijke. Some half-finished additions to modalities (#606).