Difficulty using the (co)limit formulae to construct the $n$-(co)skeleton left and right Kan extensions for truncated simplicial objects Tl;Dr - I’m struggling to show that the $n$-skeleton is a Kan extension, from the basic limit formula (this should be possible, as it was “left to the reader” in my book). I’m also struggling to even understand what the $n$-skeleton’s definition is: initially I thought “degenerate” meant: “empty” or “singleton”, but I’ve done some more googling since I wrote this post and that doesn’t seem to be the case. Unfortunately I can’t anywhere find an explicit definition of “degenerate” simplex or of $n$-skeleton.
$\newcommand{\C}{\mathsf{C}}\newcommand{\D}{\mathsf{D}}\newcommand{\E}{\mathsf{E}}\newcommand{\lan}{\operatorname{Lan}}\newcommand{\ran}{\operatorname{Ran}}\newcommand{\set}{\mathsf{Set}}\newcommand{\op}{\mathsf{op}}\newcommand{\sk}{\operatorname{sk}}\newcommand{\tr}{\operatorname{tr}}\newcommand{\cosk}{\operatorname{cosk}}$To find the left and right Kan extensions of a functor, we can use the (co)limit formulae:

Given functors $F:\C\to\E$ and $K:\C\to\D$, suppose that for every $d\in\D$ the following colimit exists: $$\operatorname{colim}\left((K\big\downarrow d)\overset{\Pi}{\longrightarrow}\C\overset{F}{\longrightarrow}\E\right)$$Where $(K\big\downarrow d)$ is the slice category, then $\lan_K(F)$ exists and is, up to isomorphism, the functor defined by the above colimit, viewing it as a functor $\D\to\E$.
If for every $d\in\D$ the following limit exists: $$\lim\left((d\big\downarrow K)\overset{\Pi}{\longrightarrow}\C\overset{F}{\longrightarrow}\E\right)$$Then $\ran_K(F)$ exists and is, up to isomorphism, the functor defined by the above limit, viewed as a functor $\D\to\E$.

Fixing a $K$, if the Kan extensions exist for every $F\in\E^\C$, then there are adjunctions: $$\ran_K\vdash K^\ast\vdash\lan_K$$Where $K^\ast:\E^\D\to\E^\C$ is the functor of precomposition.
Now, "we" know that with $\D=\Delta$ the simplicial category (including zero), $\C=\Delta_{\le n}$ the full subcategory of $\Delta$ on the objects $[0],[1],\cdots,[n]$, and $\E$ any complete and cocomplete category, $K:\Delta_{\le n}\hookrightarrow\Delta$ the inclusion functor, then the left/right Kan extensions correspond to the $\sk_n\vdash\cosk_n$ adjunction, given by $\sk_n=\lan_{\tr_n},\,\cosk_n=\ran_{\tr_n}$; these abbreviations refer to the $n$-skeleton, $n$-truncation and $n$-coskeleton.
I would like to verify this in detail using the (co)limit formulae. It's worth noting that I know essentially nothing about simplices; I have no experience working with them, or with doing any homotopy / homology theory with them, yet (I very much intend to at some point) but I would like to understand this as a primer. In fact, my motivation for my recent interest in more advanced category theory comes from wanting to 'do' algebraic topology. So I've never come across the $n$-(co)skeleton functors before.
According to nLab, the $n$-skeleton of a truncated simplicial object $S_n$ in $\E$ shall be the simplicial object $S$, defined on $k\le n$ to be $S_n(k)$, and on $k>n$ to be "a degenerate simplex". I can only assume this means $S(k)$ is the singleton set (or more generally, the terminal object) for $k>n$. I want to verify this by inspection of the following diagram: (please excuse the Paint, I don't know how to do fancier diagrams in LaTex)

Where $m\in\Bbb N_0$ is arbitrary, $S$ stands for $\lan_{\tr_n}(S_n)$, and $0\le k,k'\le n$. The $\{f:k'\to k\}$ refer to arrows in $\Delta(k',k)$ i.e. nondecreasing functions $\{0,\cdots,k'\}\to\{0,\cdots,k\}$, but note that $S_n$ acts contravariantly. The top and bottom portions of the diagram are to be interpreted with $f,g,g',k,k'$ all varying, to uniquely induce the source-target arrows. This, if I'm not mistaken, is the correct construction from the colimit formula. $i,j$ refer to inclusions, and $g=f\circ g'$. $\pi$ is the coequaliser arrow.
We want to show that $S(m)=S_n(m)$ when $m\le n$ and $S(m)=\ast$ (the terminal object) when $m>n$.
Subquestion: Is that obvious from the above diagram / definition? Riehl took care of a similar example, simply stating the value of $S(m)$ "by inspection". I had to verify this object was indeed a coequaliser, and what the appropriate coequalising arrow should be, and it wasn't at all obvious to me... I must be missing some intuition.
Moving on, I'll now try to verify this is a suitable coequaliser object. I imagine it's easiest to begin with the case $m>n$. As $S(m)$ is allegedly $\ast$, $\pi$ is just the unique arrow and the claim is that every arrow $\varphi:\bigsqcup_{\{g':m\to k'\}}S_n(k')\to X$, with $\varphi\circ s=\varphi\circ t$, factors uniquely through $\ast$. Here, $s,t$ abbreviate the source/target arrows as depicted.
Plugging in inclusions $i_{(fg',g')}$ to the right of $\varphi s=\varphi t$, for arbitrary $f,g'$, shows: $$\varphi\circ j_{fg'}=\varphi\circ j_{g'}\circ S_n(f)$$If it were the case that $\varphi=\alpha\circ\pi$ for some $\alpha:\ast\to X$, then that'd imply: $$\alpha\circ(!:S_n(k)\to\ast)=\alpha\circ(!:S_n(k)\to\ast)$$By uniqueness, which is an entirely trivial condition. $\alpha$ could indeed be any arrow, picking out any 'point', so I suppose it must be shown that $\varphi$ is somehow "just a constant map". I really don't know if this can be more categorically abstracted, so I'll just worry about $\E=\set$ now. I want to show that $\varphi\circ s=\varphi\circ t$ implies necessarily that $\varphi$ is the constant map to some element $\alpha\in X$.
We know from how coequalisers are built in $\set$ that this is equivalent to:

The smallest equivalence relation on the set $\bigsqcup_{\{g':m\to k'\}}S_n(k')$ containing $S_n(k)\ni x_{g_1}\sim x_{g_2}\in S_n(k')$ whenever $\exists y_f\in\bigsqcup_{\{f:k'\to k\}}S_n(k)$, $S_n(f)(y_f)=x_{g_2}$ and $y_f=x_{g_1}$, and $fg_1=g_2$, is the equivalence relation $a\sim b$ for all $a,b$.

More nicely, we want to show $x_g\sim x_{g'}$ whenever $g'=fg$, $x_{g'}=S_n(f)(x_g)$ for some $f$, implies all elements are equivalent.
Lemma: Under the smallest equivalence relation $\sim$ containing the above condition, every element of $(S_n(k'))_{g'}$ is equivalent to some element of $(S_n(k))_g$, for any $g',g$.
Proof:

Take $g':m\to k'$ and $g:m\to k$. We want to find a nondecreasing function $f:k\to k'$ such that $fg=g'$, because then every element of $(S_n(k'))_{g'}$ shall be identified with its image in $S_n(f)(S_n(k'))\subseteq S_n(k)$. We can define $f$ on the image $g([m])$ as $g(i)\mapsto g'(i)$. So far, this partial function $f$ is nondecreasing because $g(i)\le g(j)$ iff. $i\le j$ iff. $g'(i)\le g'(j)$. There are potentially many choices of $f$ to complete it to a nondecreasing function $[k]\to[k']$, but perhaps the simplest is $f(i):=f\left(\max\{i'\in g([m]):i'\le i\}\right)$. Then $f$ has the desired properties.

Ok. So in the disjoint union, we can always identify elements of one component with elements of another. It suffices to show the hopefully easier result that for any nondecreasing $g:m\to k$ and any two $x,y\in S_n(k)$, there is a nondecreasing $f:k\to k$ with $fg=g$ and $S_n(f)(x)=y$. This is not, perhaps, strictly necessary to show, as it may be that $x\sim y$ through a longer chain of equivalences, but I can't think of any further simplification to make. I know that for any choice of $f$ that is surjective, $S_n(f)$ will also be surjective - because $f$ will have some inverse arrow $f^{-1}$ and functors preserve left/right inverses. So I know that $S_n(f)(x')=y$ for some $x'$. What's bugging me is that I don't think there's any way to guarantee $S_n(f)(x)=y$ for some fixed, distinguished $x$. Now $f$ can obviously be chosen as the identity function, but if $g([k])$ is a proper subset of $[k]$ then that isn't necessary.
The very arbitrary nature of $S_n$ makes me feel like I have nothing left to go on. I really can't see how to demonstrate $x\sim y$. In particular, this won't be true if $m\le n$. However the problem, as I've stated it now, doesn't seem to depend on the fact $m>n$ in any obvious way.
I'd appreciate any hints on this, it seems quite mysterious.
 A: I have resolved my confusion. I post this answer for my later reference - to take paper notes - and for the aid of anyone else with a similar confusion. Unfortunately, I've just discovered that the final two sections of this answer (showing compatibility with two alternative definitions of skeleton and coskeleton) are incorrect. They can be handled with my answer here.
$\newcommand{\lan}{\operatorname{Lan}}\newcommand{\ran}{\operatorname{Ran}}\newcommand{\set}{\mathsf{Set}}\newcommand{\op}{\mathsf{op}}\newcommand{\sk}{\operatorname{sk}}\newcommand{\tr}{\operatorname{tr}}\newcommand{\cosk}{\operatorname{cosk}}\newcommand{\nat}{\mathsf{Nat}}$I will use the following slightly cleaner diagram for elaboration.

It really is just 'formal', as Zhen commented. First of all, $S:\Delta_{\le n}^\op\to\set$ is some functor (what do we call these, $n$-simplicial sets?) and $S'=\lan_n(S)$, a true simplicial set / object. The coequaliser definitely exists, so we don't actually need to worry about calculating it in general!
When $m\le n$, we can say $S'_m\cong S_m$:

Let $\pi$ be defined by $\pi\circ\iota_{g:m\to k}:=S_g:S_k\to S_m$. If $g=fh$ for $g,f,h$ all arrows in $\Delta_{\le n}$, then $\pi\circ\iota_g=\pi\circ\iota_h\circ S_f$ holds by the contravariant functoriality of $S$, so $\pi$ agrees with the source/target arrows. $\pi$ is a coequaliser:
If $q:\bigsqcup_{t:m\to k}S_k\to X$ is any other arrow that agrees with source/target, then $q=\alpha\pi$ for some $\alpha:S_m\to X$ would imply that $q\circ\iota_{1:m\to m}=\alpha$, so $\alpha$ exists uniquely if it exists at all. But if we define $\alpha:=q\circ\iota_{1:m\to m}$, then for any $g:m\to r$ ($r\le n$): $$\alpha\pi\circ\iota_g=q\circ\iota_{1:m\to m}\circ S_g=q\circ\iota_{g\circ 1:m\to r}=q\circ\iota_g$$As $q$ agrees with source/target. By the universal property of the coproduct, it must be that $q=\alpha\pi$. Therefore, $(\pi,S_m)$ is a valid coequaliser.

I was worried about explicitly calculating the coequaliser, but I don't need to. The coequaliser just supplies us with some objects we can freely attach to $S$ to have a full simplicial object $S'$, in a 'nice' way. We can begin the formal extension process by defining $S'_m:=S_m$ when $m\le n$ (valid, as shown) and $S'_f:=S_f$ whenever $f$ is an arrow in $\Delta_{\le n}^\op$. We can also define, for $k\le n$ and any $m$, $t\in\Delta(m,k)$ whatsoever, the arrow $S'_t:=\pi\circ\iota_t:S_k=S'_k\to S'_m$. Then the condition on $\pi$ reads: $$S'_g=S'_h\circ S_f=S'_h\circ S'_f$$Whenever $g=fh$ as in the diagram. It is clear that $S'$ acts functorially (contravariant) among such arrows. However we need this action to be functorial among all possible arrows in $\Delta_{\le n}$.
The Kan extension process produces, for a generic $x:m\to m'$ in $\Delta$, an arrow $\lan_n(S)(x):S'_{m'}\to S'_m$ as uniquely specified by the condition $\lan_n(S)(x)\circ\pi\circ\iota_h=\pi\circ\iota_{hx}$ for all $h:m'\to k$ with $k\le n$. That reads: $$\lan_n(S)(x)\circ S'_h=S'_{hx}$$So we see that, if $m'\le n$, $\lan_n(S)(x)=S'_x$ is forced by uniqueness. So there is no ambiguity in declaring $S'_x:=\lan_n(S)(x)$ for generic arrows $x$, and now we get full functoriality (by uniqueness and by the condition on $\lan_n(S)(\cdot)$).
So $S'$ is a full simplicial object (we only need a cocomplete category) and it agrees with $S$ on indices $m\le n$. The whole 'degenerate' business was opaque to me. But, with this definition of $S'$ on arrows, by very definition is (in the case of $\set$) every "simplex" of $S'_m$, for $m>n$, in the image of $S'_t$ on $k$-simplices, for $k\le n$ and $t:m\to k$ (coequalisers surject in $\set$). It can be shown that this is a sufficient condition (regardless of $t$) for the $(m>n)$-simplices to all be degenerate. The degeneracy operators are those supplied by the coequaliser.
When $S$ is the truncation of a full simplicial set $S$, $S'$ shall be $\sk_n(S)$:

This was already shown on $m\le n$. If $m>n$, then define $\pi$ uniquely by $\pi\circ\iota_t:=S_t:S_k\to S_m$. Since $S$ is functorial, the $\pi$ thus defined shall agree with source/target. Let $q:\bigsqcup_{t:m\to k}S_k\to X$ be any other arrow agreeing with source / target. The elements of $\sk_n(S_m)$ are precisely all $\sigma\in S_m$ that are of the form $S_t(\tau)$ for some $\tau\in S_k,\,t:m\to k$ and $k\le n$. If $q=\gamma\pi$ for some function $\gamma$, it must be that: $$q\circ\iota_t(\tau)=\gamma\circ S_t(\tau)=\gamma(\sigma)$$So the value of $\gamma$ on every element is forced.
But in fact, we may take $k=n$ and $t$ some surjection $m\to n$. For if such $t$ exists, we may find a surjection $t':m\to n$ and $t'':n\to k$ with $t''\circ t'=t$. Then, $S_{t'}\circ S_{t''}=S_t$, so there must be some $\tau'\in S_n$ that $S_{t'}(\tau')=\sigma$. Now fix some choice of surjective $\alpha:m\to n$ and $\tau\in S_n$, and define a function $\gamma:\sk_n(S_m)\to X$ by $\gamma(\sigma):=q\circ\iota_{\alpha}(\tau)$. We need to check this is well-defined.
Should $t:m\to k$, $\omega\in S_k$ be any pair with $k\le n$ and $S_t(\omega)=\sigma$, then, as before, we know $S_\alpha\circ S_\beta=S_t$ for some $\beta:n\to k$, so: $$\sigma=S_t(\omega)=S_\alpha(S_\beta(\omega))=S_\alpha(\tau)$$But $S_\alpha$ is injective because $\alpha$ is (split) surjective; thus, $\tau=S_\beta(\omega)$, and: $$g\circ\iota_t(\omega)=g\circ\iota_{\beta\alpha}(\omega)=g\circ\iota_{\alpha}(S_\beta(\omega))=g\circ\iota_{\alpha}(\tau)=\gamma(\sigma)$$Proving well-definedness and agreement with $q$.


Now for the co-skeleton. Take some $X:\Delta_{\le n}^\op\to\set$ and call its right Kan extension along $\Delta_{\le n}^\op\hookrightarrow\Delta_n^\op$ the simplicial set $X'$. The limit formula gives us: $$X'_m\cong\left\{(x_t)\in\prod_{t:s\to m,\,s\le n}X_s:X(f)x_{g:k\to m}=x_{gf:r\to m},\,\forall f\in\Delta_{\le n}(r,k)\right\}$$
This is identical to: $$X'_m\cong\nat(\tr_n\Delta^m,\tr_n X')$$Via the identification $x_t\sim\varphi(t)$. By the Yoneda lemma, $X'_m=X_m$ for indices $m\le n$. nLab takes the definition of "$n$-coskeletal" to be when that isomorphism holds, essentially. nLab also claims that, if $X$ is the truncation of a full simplicial set $X$, then: $$\cosk_n(X_m)=\nat(\sk_n\Delta^m,X)$$The standard $m$-simplicial set $\Delta^m$ is $m$-dimensional, so this formula holds trivially when $m\le n$ (by the Yoneda lemma). Why should it hold for $m>n$?

$\sk_n(\Delta^m)$ is the simplicial set with $\nu$-simplices the set of all $f:\nu\to m$ that factor through an arrow $f':k\to m$ where $k\le n$. We want to identify natural transformations $\varphi:\sk_n(\Delta^m)\implies X$ with natural transformations $\psi:\tr_n(\Delta^m)\implies\tr_n X$. Now, $\tr_n\sk_n(\Delta^m)=\tr_n\Delta^m$, so $\varphi$ can be mapped to $\psi=\tr_n\varphi$.
Let's take any $\psi:\tr_n\Delta^m\implies\tr_n X$. We need to show there is a unique way to extend $\psi$ to components $\psi_{\nu}:\sk_n(\Delta^m_\nu)\to X_\nu$ ($\nu>n$) that assemble into a natural transformation. Given any $f:\nu\to m$ in the $n$-skeleton, break down $f=gh$ where $g:k\to m$ has $k\le n$. If $\psi$ lifts to a natural transformation, then: $$\psi_\nu(f)=\psi_\nu\circ h_\ast(g)=X(h)\circ\psi_k(g)$$But the component $\psi_k$ is already given, so this extension is certainly unique. We just need  to know that $\psi_\nu$ can be defined in this way unambiguously, that is, that $X(h)\circ\psi_k(g)=X(h')\circ\psi_{k'}(g')$ for any pairs $k,k'\le n$ with $gh=f=g'h'$.
We can write $f=g'h'$ in the canonical way, where $h':\nu\to k'$ is a surjection and $g':k'\to m$ is an injection. Given another: $$f=\nu\overset{h}{\longrightarrow}k\overset{g}{\longrightarrow}m$$With $k\le n$, it is true that $g=g'\circ\ell$ for some $\ell:k\to k'$. Because $\psi$ is natural: $$X(h)\circ\psi_k(g)=X(h)\circ\psi_k(g'\ell)=X(h)X(\ell)\circ\psi_{k'}(g')$$
But $f=gh=g'\ell h=g'h'$, so by injection it is true that $\ell h=h'$. So we can finish off: $$X(h)\circ\psi_k(g)=X(h)X(\ell)\circ\psi_{k'}(g)=X(h')\circ\psi_{k'}(g')$$
So the definition of $\psi$ on composites $f=gh$ as $X(h)\circ\psi_k(g)$ is well defined and lifts $\psi$ to a natural transformation - uniquely - from $\sk_n(\Delta^m)\implies X$.

