Factorization operations
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-03-10.
Last modified on 2023-06-29.
module orthogonal-factorization-systems.factorization-operations where
Imports
open import foundation.universe-levels open import orthogonal-factorization-systems.factorizations-of-maps
Idea
A factorization operation on a function type A → B
is a choice of
factorization for
every map f
in A → B
.
∙
^ \
/ \
/ v
A -----> B
f
Definition
Factorization operations
module _ {l1 l2 : Level} (A : UU l1) (B : UU l2) where factorization-operation : (l3 : Level) → UU (l1 ⊔ l2 ⊔ lsuc l3) factorization-operation l3 = (f : A → B) → factorization f l3
Recent changes
- 2023-06-29. Fredrik Bakke. Fix hyperlinks (#677).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 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).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).