Remark 6.138. There is a pullback square For \(\An\), every lax functor occurring here is automatically strict.
