Let be an (∞,1)-category and and two morphisms in . Write for the under-over-(∞,1)-category.
We say that is left orthogonal to and that is right orthogonal to and write
if for every commuting diagram
in we have that is contractible.
Note that the notation subtly includes the given commuting diagram, since is only defined relative to a particular given morphism . Here we take that to be the common composite of the given commuting square, with and regarded as objects of via the resulting commuting triangles.
Let be an (∞,1)-category. An orthogonal factorization system on is a pair of classes of morphisms in that satisfy the following axioms.
Both classes are stable under retracts.
Every morphism in is left orthogonal to every morphism in ;
For every morphism in there exists a commuting triangle
with and .
This is (Lurie, prop. 126.96.36.199 (7), (8)).
Let be an orthogonal factorization system on an -category . Write for the full sub-(∞,1)-category of the arrow category on the morphisms in .
this is a reflective sub-(∞,1)-category
The adjunction units are of the form
(In words: the reflection into is given by the factorization in ).
This is (Lurie, lemma 188.8.131.52).
Section 5.2.8 of
Formalization in homotopy type theory is discussed in
- Egbert Rijke, Orthogonal factorization in HoTT, talk at IAS, January 24, 2013 (video)