I do not understand the proof of Variant 4.2.3.16 of *Higher Topos Theory* by Jacob Lurie, and I need help.




---


Variant 4.2.3.16 asserts the following:



> 
> ($\diamond$) Let $K$ be a finite simplicial set. There is a cofinal map $N(A)\to K$, where $A$ is a finite poset.
> 
> 
> 


The proof proceeds as follows:


(**1**). Consider the following property for a simplicial set $K$:


($\ast$) Every nondegenerate simplex $\Delta^n\to K$ is a monomorphism.


If K satisfies ($\ast$), then $K$ satisfies the conclusion of ($\diamond$).


(**2**). We show that, for each finite simplicial set $K$, there is a cofinal map $\widetilde{K}\to K$, where $\widetilde{K}$ is finite and satisfies ($\ast$).




---


I am fine with step (1). But I don't understand the proof of (2).


Let me explain Lurie's proof of (2). He argues that we can prove (2) by induction on the number of nondegenerate simplices of $K$. According to him, this is because if $K$ can be written as $K=K\_0\amalg \_{\partial\Delta^n} \Delta^n$, where $K\_0$ satisfies ($\ast$), then $K$ also satisfies ($\ast$). To prove this, he choose a cofinal map $\widetilde{K\_0}\to K\_0$, where $\widetilde{K}\_0$ is a finite simplicial set satisfying ($\ast$), and claims that the map $$\widetilde{K}=(\widetilde{K}\_0\times \Delta^n)\amalg \_{\partial \Delta^n} \Delta^n\to K$$
witnesses property ($\ast$).


The problem is, **I do not understand what the map $\partial \Delta^n\to \widetilde{K}\_0$ used in the definition of $\widetilde{K}$ is.** Can someone explain what this map is? (Or does anyone know how to prove (2) or ($\diamond$) in different ways?)


Thanks in advance.



Cofinal maps from posets (HTT, 4.2.3.16)
[Rephrasing my comment as an answer]


While I cannot speak for the actual proof, two points are worth noting. First, a similar construction appears in Kerodon (<https://kerodon.net/tag/02QA>) but there (1) $\widetilde{K} \to K$ is required to be a trivial fibration but (2) it doesn't restrict correctly to when $K$ is finite.


The second point is that Kerodon also includes a stronger proof of this same fact (<https://kerodon.net/tag/02MU>). The construction is quite different but should suffice as a replacement.


