cshsketches.tex

\documentclass[csh.tex]{subfiles}
\usepackage{amssymb, amsmath}
\usepackage[backend=bibtex,citestyle=authoryear-icomp]{biblatex}
\usepackage[all]{xy}
\usepackage{url}


\newcommand\pushout{\ar@{}[dr]|(.9)\ulcorner}
\newcommand\parr{\ar@<.5ex>[r]\ar@<-.5ex>[r]}
\begin{document}

\section{9/9/19}

https://mathoverflow.net/questions/331121/extending-kan-fibrations-without-using-minimal-fibrations

Szumilo's answer is not constructive enough, in that it still
makes all monic cofibrations. Shulman's solution relies on
\(\kappa\)-representability, which was to other obstacle to
overcome.

Added my draft as another answer. Let's see what happens.

\section{26/8/19}
LaTeX hurts my back.

I now have solved the problem. I think I want to add the
example of modest Kan complexes, and explain why/how the 
construction should work there, without claiming victory just 
yet.

\section{14/8/19}

The time has come for the puzzle of defining the ascend functor.

For $f\of X\to \Delta^n$ the $n$-dimensional simplices of $Af$ are freely glued 
in simplices between p-dimensional simplicies of $f$ and $q$-dimensional
simplicies of $f^{\delta^n_k}$, such that $p+q=n-1$. The whole $f^\delta$ part is
supposed to be located over $k$, at the start of the fibre. So how to break a
morphism in two parts for defining the action?

The morphism $f$ assigns some element $\xi$ of $|Delta^n|$ to each
$x\of \dom f$ and the other part has a dimension $d$. So we have this couple
$\tuplet{\xi,d}$. All that needed is a consist way to break up 
$\phi\of[a]\to [\dim(\xi)+y+1]$ into two morphisms $\phi_0\of[a_0]\to\dom[\xi]$
and $\phi_1\of[a_1]\to [y]$, to apply to the two constituent parts.

\begin{align*}
m_0 &= \max(\set{a\of[a]| \phi(a) \of \dom(\xi),\xi(\phi(a)) < k }\cup\set{-1})\\
m_1 &= \max(\set{a\of[a]| y < \phi(a), \xi(\phi(a) - y - 1) < k }\cup\set{-1})\\
a_0 &= a - m_1 + m_0\\% $m_1+1$ maps to $m_0+1$!
a_1 &= m_1 - m_0 - 1\\
\phi_0(i) \textrm{ for } i \leq m_0 &= \phi(i)\\
\phi_0(i) \textrm{ for } i > m_0 &= \phi(i + m_1 - m_0) - y - 1\\
\phi_1(i) &= \phi(i + m_0 + 1) - \phi(m_0 + 1)
\end{align*}
I don't believe I made any off by one errors here, but it is always hard to be
sure.

\paragraph{Conclusion}
I got the proof down. The rest, I believe is context.

\section{29/7/19}

I was working toward an argument that works for internal families of morphism
as long as their domains are small in an internalized sense. GHSS seems to be 
using decidable properties of cofibration to make the small object argument 
work. I doubt that this is necessary.

"A small object argument for incomplete toposes"

How about this: given $f\of X \to Y$, consider small morphisms $g\of W \to Y$
that factor through $f$. I.e. the category of small objects over $f$.

The one step factorization is these small morphisms is not sufficient,
the colimit must be taken over $n$-fold factorizations for all $n$. Now,
a morphism between small morphisms induces a morphism between these 
factorisations as long as the number of factorizations is greater for the target 
object. It is a bit underwhelming, but the result is the product category of 
the poset $(\nno, \leq)$ and the category of small morphisms over $f$.

That is almost too simple\dots. 

Take the colimit here. The hard part is the domain. There is an object of small 
morphisms over $f$.

Perhaps it is somehow easier the other way around. For small morphisms, the
transfinite factorisations supposedly just exists. 

No! 

I want to avoid making the codomain of the generic left morphisms small as well,
but without such an assumption, it is not clear that a colimit exists.

This could be a case of mixed concerns. On one hand, the construction is a
recursive colimit, which may not exist, on the other, 

\paragraph{Jump ahead}
Consider $f\of X\to Y$ again. There is a diagram of small fibrations over
$Y$ and that could be useful. Maybe there simply is a limit. There are structure
morphisms to work with. And morphism of small morphisms over $f$ can be judged
to be left morphisms due to the lifting properties.

\paragraph{Inspiration}
I feel up to nothing today. I have no faith I am doing any good, and I am not
having any fun working on this either. Instead, I am once again trying to
remember what my plan was, because despite all these notes, I don't know how to 
write this paper. 

I came up with a combinatorial proof for the descent of fibrations along 
cofibrations. That puzzle motivated me for the last 50 days. Do I do any good to
solve it?

The proof is supposed to show that the universe of types is fibrant. Five years
ago nobody seemed to be aware of a combinatorial approach that actually worked.
That is a reason to think that these facts aren't widely known.

"Fibrant universes--a combinatorial proof"

This was the manageable part. 

The good days were: 12/6-19/6. After those, I got distracted. Keep wiritng about
this.

\paragraph{Ascent functor}
After mucking about with encodings, I am not eager to start again, though the
difference should not matter all that much.

A small part of the pain come from the pervasive off by one error.
The real pain, however, is in defining the restriction maps.

Let's just start with $\alpha\of[a]\to[n]$. We want to use an initial segment
of $\alpha_k$ for glueing, so we can just indicate how many elements we want to
use, leading to $(\alpha,i)$ with 
$f(\alpha,i):[a - i] \to [a]$ and $g(\alpha,i):[i - 1]\to [a]$ as components.
I have no good names yet. We need a way to split morphisms up, however.
$f(\phi,\alpha, i)$ and $g(\phi,\alpha,i)$.

It is a convolution of sorts.

The sad thing is that the sets of simplices is simple, but the action is
incredibly hard to define.

Idea: $\alpha +_k b$ for adding $b$ elements to the start of the $k$-th fibre
This lets us do:
\[ \sum_{\alpha +k b \of |\Lambda^n_k|} X[\alpha]\times X^{\delta^n_k}[b]\]
So how is the action defined? 

Let's solve this puzzle later. At least I have an idea what to do now.

\section{15/7/19}
Nicola Gambino, Christian Sattler, Karol Szumiło and Simon Henry are working on
constructive simplicial homotopy. I assume their constructuction are correct,
because they are exactly the ones I was considering. See: 
https://arxiv.org/abs/1905.06281,
https://arxiv.org/abs/1907.05394.

So what is left?
\begin{itemize}
\item There seems to be no consideration of realizability categories.
\item None of the external view I was considering is present, which could mean 
my approach is a different way of looking at the same results, or simply
completely different.
\item Completeness of modest sets in the ex/lex completion of assemblies.
\end{itemize}

I have no answer for the coherence properties, but I can do more of the rest.
The main issue are:
\begin{itemize}
 \item Do ex/lex completions indeed preserve completeness?
 \item Are homotopy categories indeed equivalent and do they preserve 
 completeness?
\end{itemize}
These are questions about presheaves modulo weak equivalences.

I am unsure about whether the coherence issues pose a problem for the modest 
case.

\paragraph{Complete universes}
Rather than looking at maps with a lot of sepcific properties, we are interested
in morphisms $u\of U \to V$ of locally cartesian closed categories
where every exponential $u^I\of U^I\to V^I$ is a pullback of $u$.
Issues:
\begin{itemize}
\item Beck-Chevalley: what does it mean here? Does it hold up?
I think that asking that $u^I$ is a pullback sufficient, and that discretes of 
the effective topos simply won't do that.
\item Is it true that discretes aren't a complete universe then?
\item What does moving to a category of internal presheaves do?
\item What does localization on a cofibrantly generated model structure do?
\end{itemize}

\paragraph{Beck Chevalley}
The Beck Chevalley condition seems to require a little more just to formulate,
since we need $\Pi_f \of u^X \to u^Y$ for all $f\of X\to Y$.
Okay, so I know about the fibred product: 
$A^f = \set{\tuplet{y\of Y,X_y \to A}}$
This is sufficient. If $u^f$ is a pulback of $u$, then a map 
$\Pi_f\of u^X \to u^Y$ is transposed to that one. This also cements completeness
some more. What about Beck-Chevalley?

It would be hard to guarantee that the right adjoints commute on the nose,
but no more than isomorphism is required. It look like:
if $a$ is a pullback of $b$ with $c\of a\to b$, then $\chi_a\of u^a \to u$ is 
isomorphic to $\chi_b\circ u^c \of u^b\to u$. Yeah, the morphisms don't have to
commute on the nose, but they should have isomorphic fibres.
This sound pretty automatic, however. I.e. in an lccc, if fibred products are
pullbacks, then Beck-Chevalley holds.

I just realize what is nice about the exact completion: it creates a classifier
of discrete objects. The map is unique, so we no longer have to mess with things
holding only to isomorphism.

There are transpose Beck Chevalley condition. The notions of a large coporduct
of small object is confusing, but in case of modest sets, it makes sense due to
the modest reflection. Yeah, and we see it in the subobject poset as well.

It doesn't simplify anything to work this way.

\paragraph{Discretes}
So what is the problem with discrete objects in the effective topos? 
There is something about quotients along equivalence relations that aren't
$\neg\neg$-closed.

Actually, let's work things out. For modest sets in assemblies out complete
universe is given by the bundle of equivalence classes over the set of partial
equivalence relations over the natural numbers. Since each equivalence class is
a set of numbers, we have a set of realizers for each equivalence class.
This is the universe of modest sets.

It is complete in the above sense? The fibred products along arbitrary functors
are products again. 

\paragraph{differences between ex/lex and ex/reg: the epic factor}
The ex/lex completion is the homotopy category for the canonical cofibrantly 
generated model structure on locally contractible simplices. So what changes for
the ex/reg completion? Probabaly that products over inhabited families of
cofibrant generator suddenly count as well.

The ex/reg completion has extra equivalences between the locally contractible
spaces, with mere existence of paths replacing a specific choice. This weakening
is fatal for completeness in the recursive realizability context, which is good
at throwing a wrench into axiom of choice based arguments.

locally contratible--for lack of better words. $\geq 1$-connected perhaps.

\paragraph{Internal prescheaves}
The ex/lex completion and the simplicial homotopy catgeory combine two steps:
presheaves and cofibrantly generated model structures. So\dots don't presheaves
simply preserve complete universes?

The idea is simple enough: use fibrewise smallness. That should work.

Okay, there is an obvious quirk not to overlook: the homotopy
category allows large set of paths, but those aren't small objects anymore.
The modest reflection sort of solves this riddle: the classical epic part
is split, the rest is recorded in the small structure.

\paragraph{Combinations}
Ex/lex is simply connected simplicial sets with the standard model structure.
If we repeat the simplicial homotopy category construction up here, what do
we wind up with? Convariantly `bisimplicial' assemblies, with a cofibrantly
generated model structure. The result should be the same if we just look
at simplicial assemblies.

\paragraph{coming back up}
The intuition that modest simplicial sets could be a good model for univalence
is supported by the new papers.

\subsection{Simplicial Assemblies}
\begin{itemize}
\item We will be working with internal presheaves in the category of assemblies.
\item Cofibrations are monics with decidable sets of complementary faces--
  `Reedy decidable`.
\item Fibrations are `Reedy split`--have the lifting operators.
\end{itemize}

Nice, but how does this help? What would we prove here?

I guess I want simplicial pers to be a model. What are they?

I do need a new plan.

To show that simplicial modest sets are a modest for univalence,
We should not have to do much, since the modest sets are already models for a
powerful type theory. The generic modest fibration is a neat trick, but should
not be too hard. I am stuck with vague complaints of coherences.


\paragraph{CZF} So Gambino et al. work within CZF. A model exists in 
the effective topos and should be close to modest sets.

So the value of the paper is that instead of guessing, I now have a roadmap
toward a model structure on assemblies. I also don't need the separate paper on
constructive simplicial homotopy anymore.

\paragraph{new ideas on density}
Not knowing for sure how useful the papers are yet, just let write these 
considerations down.

Use small morphisms instead of just morphisms with small domains. The problem
of finding factorizations becomes the problem of finding fibrant replacements
in slice categories.

I was only in the process of demonstrating a factorization system. Gambino et
al. do much more than that, but the applicability of their ideas on the
category of assemblies is not immediately clean, ironacally because of the
reliance on the internal language, precisely what I was trying to get away from.

This it what the papers can do: either give me something to point to as
evidence for my own claims, or a pointer on how to prove useful result myself.
I am mostly just worried about having nothing left to prove.

I suppose the modest simplicial sets are still interesting, but
we need to bring the arguments into to context of the category of assemblies
and show that the coherence issues don't play such a big role there.

\section{1/7/19}
Important but forgot to mention: the notion of small morphism is important,
and small morphisms are closed under composition. Closure under composition
means being small-filtered, giving all small diagrams a cone. Should also help
with composing small left morphisms.

Each morphism has a fully faithful diagram connected to it--its diagram of 
fibres--that may sometimes offer a simpler view of other diagrams, 
namely as internal functor to such diagrams of fibres. This not only is a good 
family of examples, but it could also give an easier statement of the conditions
we need.

\section{30/6/19}
\paragraph{move to toposes}
Conjecture: 
Suppose that a $\Pi$-pretopos $\ambient$ with natural number object has a dense
(directed) diagram $D$. Then $\ambient$ is a topos. The coequalizer of domains 
and codomains of epics in $D$ is a subobject classifier $\Omega$. The object of
epics $E$ is crucial here--and directedness and important reason it exists.

So, this would be a reason to rewrite on the assumption that the ambient
category is an elementary topos. All the examples are in fact toposes.

Let $m\of X\to Y$ be any monic. Needed are $Y_D$ and $Y_E$ plus morphisms
$p,q\of Y_D\to Y_E$, $r\of Y_D\to D$ and $s\to Y_E \to E$ that commute with
the domain and codomain maps and that somehow classify the monic.
Part of the formula is letting $Y_D$ just be a cover of $Y$ with tuplets
$\tuplet{x\of D_0,y\of D[x],z\of D[x]\to Y}$ and $Y_E$ be commutative diagrams
$e\to m$ where $e$ is a $D$-epic, possibly together with $y\of D[\dom(e)]$, so 
for a map $Y_E\to X$. Yes, $Y_E$ needs to cover $X$ and all equivalent pairs of
$Y_D$. Feel rather complicated, but something like 
$\tuplet{x\of E,y\of D[\dom(x)], z\of D[\cod(x)]\to X}$, with 
$p\tuplet{x,y,z} = \tuplet{\dom(x), y, m\circ z\circ (x\cdot)}$ and
$q\tuplet{x,y,z} = \tuplet{\cod(x), x\cdot y, m\circ z}$.
This ought to do the job and induce the desired


\paragraph{smarter?}
A better way may be: if the object of $D$-epics $E$ exists, then surely the 
object of $D$-monics $M$ exists as well. This should acts as a weakly generic 
monomorphism however, which is all we need.

Thinking backwards: we can cover each object with 'sums' of $D$-objects. Pulling
back the monics might force us to cover the domain again, but then we still get
a cover for each monomorphism by the generic $D$ morphism. 

We need fullness of $D$, but that isn't new is it?

Ultimately, take the epi-mono factorization of the universal $D$ morphism, 
then the fibered product of isomoprhism of the fibers of the monic factor, 
then the quotient of that equivalence relation. What exactly could we be missing
then?

\paragraph{counter}
I suspect that somehow a subterminal could be so great that no $D$ object 
properly covers it, dispite density of $d$. Take $\mathrm{Set}/\omega$. Finite colimits 
of representables are candidate for $D$, they surely fit every bill. The whole
density thing is easy to arrange. There is no way to cover the terminal object
without using `large' objects are indexes. This is a topos, but maybe we can fix 
that using cardinalities as well. E.g. take functions with finite fibres only.
Only worry is that $D$ would not be internal anymore. Okay, so move to teh next 
limit cardinal: subcategory of $\mathrm{Set}/\lambda$ with fibres smaller than $\lambda$.
Not a topos because the subobject classifier is huge. Many more representables,
that sucks. So the exponentials get in the way of a convincing counter here.

\paragraph{Use those exponentials then}
First cover the terminal object with objects of $D$, to sabotage what happened
above. Note that since each object has a unique map to the terminal object, this
simply is the sum of $D$ objects. Call that $C$ and consider $D^C$, or ever 
$D_0^{D_0}$, just to get something that should be big enough to cover
a potential subobject classifier.

We arrive at $D_0$ modulo equi-inhabitation as before, as the smallest possible
solution. Full idea: for each monic $m\of X\to Y$, $m$ is covered by a family of
$D$-morphisms $\set{ m_i\of X_i\to Y_i| i\of I}$. 

Actually, first cover $Y$, than cover the domain of the pullback of $m$ and use 
fullness to argue that this must be a $D$-morphism. Does that work?

The unique lifting properties of epics versus monics are crucial here.
With their help, the pullback of $m$ is already classified and $m$ soon follows
by diagram chasing. There is a map to the monic factor of the universal 
$D$-morphism. 

\paragraph{pressing questions}
Could all $D$-objects be inhabited? Would it matter if they were?
This is another challenge. 

No, we have a universal $D$ morphism, whose codomain is a rather large 
combination of $D$ objects. The way in which we get a subobjectclassifier is
not that sensitive to these problems.

\paragraph{Conclusion}
We might as well assume we are working in a topos, because if there is a
suitable dense internal full subcategory, then there probably is a subobject
classifier. All examples I have in mind are toposes. All we have to do is
explain this choice.

\section{23/6/19}
\paragraph{The construction\dots}
Given a dense directed diagram $D$ and family of \emph{generic left morphisms}
$L$ that live in $D$, there is an object $P$ of pushouts of members of $L$. 
The following dependent limit tracks finite compositions of these pushouts.
\[\prod_{n\of\nno}\set{f\of[n]\to P|\dom\circ f\circ\delta_0 = \cod\circ f \circ \delta_n}\]
There is a morphism that takes these sequences to their composites and the
image of this morphism $A$ will be the object of objects is a new diagram.

Morphisms between the composed pushouts are themselves combinations of pushouts
and morphisms:
\[\xymatrix{
  S_0 \ar[r]^s\ar[d]_{m_0}\pushout & S_1\ar[d]\ar[dr]^{m_1}\\
  T_0 \ar@/_/[rr]_t\ar[r] & \bullet \ar[r]^{\of P} & T_1
}\]
Any commutative square $m\of s\to t$ can be factorized as a commutative 
triangle following a pushout square. Here the commutative triangle consists of
morphisms of $P$, however.

The new diagram $L'$ of left morphisms gives a factorisation system which 
factors morphisms into left and right ones, because this selection of morphisms 
doesn't interfere with the lifting property.

\paragraph{target diagram of generators}
So, small objects. The smallness of the domains of the generic left morphisms
means that $\hom(d,\cdot)$ preserves directed colimits, which is the most
mysterious part. Since we can represent the left factor $l(f)$ of a morphism 
$f$ as a directed colimit, there are now a number of steps we can take to lift 
a generic left morphism $g$ again the right factor  $r(f)$.

Firstly consider that the morphism
$\dom(g)\to \dom(r(f)) = \cod(l(f)) = \colim_{l'\to f} (l')$ 
is a member of $\colim_{l'\to f} \hom(\dom(a),\cod(l'))$.
Secondly, there is an operation that takes this data and generates a new member 
of the diagram: take the pushout $g$ and compose with $l'$.
Finally, the finality of $l(f)$ forces $g$ to factor through $r(f)$

A number of properties is desired fo the target diagram of generators and
obtained only through combining different structure, but what we need is:
\begin{itemize}
  \item closure under composition of the left morphisms
  \item a dense diagram of codomains, with left morphisms pushed out out to all 
  of them
  \item enough morphisms to get a direct diagram
  \item not so many morphism that the left lifting property is lost in the 
  colimit
\end{itemize}

\paragraph{algebraic lifting properties}
When you equip a right morphism with an lifting operator, no guarantees are 
given that lifts of compositions of left morphisms will commute. The 
factorizations constructed above do give such guarantees. This is just an aside.

\paragraph{paper}
Perhaps I now finally have what I need to write the paper I have been working 
on for the past 5 years\dots 

\begin{itemize}
  \item a plausible story for algebraic factorisation systems in simplicial 
  assemblies
  \item a plausible story for extending fibrations along horns
  \item the language of internal diagrams and sheaves
\end{itemize}

Add the motivating example of modests simplicial sets.

\section{22/6/19}
\paragraph{shortly on factorisation systems}
To replace the small object argument, turn the left side of the factorisation
into a filtered colimit. A saturated set of small morphisms is not needed,
but closure under pushouts and compositions is. Care about the morphisms of
the category or the filteredness is going to fail.

\paragraph{what about the algebras?}
Fibrations are algebras already, just not of a monad. The procedure above is
a way to get a free monad, which is the algebraic factorization system. It
doesn't need to consist such structures itself.

I don't think the algebra idea is that helpful.

\paragraph{better approaches}
A finite composition of functions can be encoded as $X \to Y \to [n]$ with
extra structure to get $X_{i+1}\simeq Y_i$ for all $i<n$. The actual composition
still has to be derived. If we moreover know that $X\to Y$ is a pushout of a
coproduct of generic left morphisms, then we are ready. All structure we need 
is present.

\section{21/6/19}
I'd like to look into the factorization systems again. Ultimately, it should
combine two ideas: approximating object with dense categories and using
initial algebras or terminal coalgebras, to create factorization systems.

The following concepts are sort of clear:
\begin{itemize}
  \item the category of small objects
  \item the functors to consider the algebras or coalgebras of
  \item what the morphisms between the algebras should look like
\end{itemize}

The rest is a mess.

Proving that a morphism is an acyclic cofibration, requires knowing the
complementary faces plus a strategy for glueing them in. This strategy 
could be a coalgebra of sorts, breaking down each 

May it would look as follows.
\[\xymatrix{
  A\ar[r]^i\ar[d]_a & B\ar@/^/[r]^{c}\ar@/_/[r]|(.4){l(b)}\ar[dr]_{b} & LB\ar[d]^{r(b)}\\
  X\ar[rr]_f && Y
}\]
Here $c$ is the coalgebra, but $a$ is also the equalizer of $c$ and $l(b)$, to 
ensure that the complement of $A$ won't be send to itself. This only works 
because cofibrations are regular monomorphisms. The risk here is that the 
coalgebra is not well-founded.

\section{19/6/19}

\paragraph{Two more days of thought}
Let $W = \bigcup_{i\of [n]-\set{x,\xi(y)}} U_i$ and let
$V=\bigcup_{j\of[m]}V$.
For faces $f\of W-U_{\xi(y)}-V$, $y$ is a
fine support point. If $f\of W-U_{\xi(y)}-V$, then it subface
$f-y$ doesn't belong to any $V_j$ with $j\neq y$.
For $f\of U_{\xi(y)}-W-V$, $\beta(f)_i\neq \emptyset$ for any 
$i\of [n]-\set{x,\xi(y)}$, hence there are points like $\max\beta$ and
$\min\beta$ to use as supporting points.
\begin{align*}
  \max\beta(\xi(y)) &=y\\
  \max\beta(i) &= \beta(i,\max(\alpha_{\delta(i)})) \textrm{ if } i\neq \xi(y)\\
  \min\beta(\xi(y)) &=y\\
  \min\beta(i) &= \beta(i,\min(\alpha_{\delta(i)})) \textrm{ if } i\neq \xi(y)
\end{align*}
The remaining faces of $U_{\xi(y)}\cap W-V^y$ can all be extended with extra 
points to become member of these difference sets. I didn't want to use $y$ in 
these cases, because we don't want the support point to be removeable and
$y$ is too specific.

I think we have all faces we need now, but there is still a problem.
If $f\of U_{\xi(y)}-W-V$ there is typically no reason why $f-p(f)(i)$ 
should belong to $U_{\xi(y)}-W-V$ for $i\of [n]-\set{x,\xi(y)}$. The argument
would probably be that we can get $f-p(f)(i)$ from other supporting points,
but only if those faces have been added before\dots

Obviously, $W-U_{\xi(y)}-V$ don't need to use this measure. Also, we have to see
whether dimension actually can be left out completely.
What if we just use $\sum(\beta)$?

\paragraph{strategy}
Suppose we always take $\max\beta$. 
The supporting points we get $f-p(f)(i)$ from are always strictly lower. So we 
use $\max\beta$ to determine when a face can be added.
in fact $\sum_{i\of [n]-\set{x,\xi(y)}} \beta(i,\max(\alpha_{\delta(i)})$ could
be a replacement for dimension here.

\paragraph{go through proof}
Let $\sigma\tuplet{\alpha,\beta,\gamma} = \sum_{i\of [n]-\set{x,\xi(y)}} \beta(i,\max(\alpha_{\delta(i)})$.
Let $A_d$ be the union of 
$(\bigcup_{i<n} U_{\delta^n_x(i)}) \cap (\bigcup_{j<m} V_{\delta^m_y(j)})$ with 
all faces for which satisfy:
\begin{enumerate}
  \item $\tuplet{\alpha,\beta,\gamma}\of (U_{\xi(y)}-W)\cup(W-U_{\xi(i)}) - V$
  Also $f$ contains its supporting point.
  This should be part of the first condition.
  \item $d > 2\dim(\beta)+\dim\gamma$
\end{enumerate}
Inaccurate language obviously, the simplex $\tuplet{\alpha,\beta,\gamma}$ 
generates a simplicial set which is a subset of $A_i$.

We need to show a couple of things, one is that the inclusions $A_d\to A_{d+1}$
are acyclic cofibrations, the other that there is a $D$ such that 
$A_D = \bigcup_{i<n} U_{\delta^n_x(i)} $.

So for $(W-U_{\xi(i)}-V)$ we simply take $f\circ \delta_y$, which reduces the
dimensions (when we remove the maximal element of a
segment), may even lands us directly in $A_0$. Hence all of these faces are 
present except the one that fails to reach $y$.

For $(U_{\xi(i)}-W-V)$ it gets a bit more complicated. Most $f\circ \delta_y$
are included because of reasons outlined above. The problem cases are 
$f-\max(\beta(f))$, which remains excluded and $f-\max(\beta(f))(i)$.
These never fall into $V_j$ because $\max(\beta(f))(i)$ itself is still there.
If they don't fall into $W$, then we add the new $\max(\beta(f-y))$ to get a
face with the same dimension but a lower score because points in $\Gamma$ are
cheaper. If they fall into $W$, then maybe we just should add $y$ and be done 
with it--that would require making $y$ cheaper as well! 
That adds 1 to the dimension, but $\sigma$ will have lost more 
($0\of[m]$ is a problem, so perhaps we need to adjust our measure of $\sigma$).

\paragraph{cost model}
Define the cost of $\tuplet{\alpha,\beta,\gamma}$ as twice the number of points
$\beta$ reaches in $[m]-y-\xi_x$ once the number of points in 
 plus once the number of points in $\xi_x\cup\set{y}$ plus the number of points
 $\gamma$ reaches. Now we can say that leaving out or replacing point reduces 
 cost and that there is a maximum cost.

We need to sharpen our definitions.
All $j\of [m]-y$ occur somewhere either way. $f$ reaches $y$ or
more complicatedly, $f$ reaches all $\xi_i$ except $\xi_{\xi(i)}$ plus an extra
point $p$ which is a combination of maxima.

Finally, after all this time!

\paragraph{consequences}
There are ascend functors $A^n_x:\cat S/\horn_x[n]\to \cat S/\simplex[n]$ and
these preserve acyclic fibrations. They have right adjoints $D^n_x$ which 
preserve fibrations, so this is a Quillen adjunction. The unit
$\eta\of\id\to D^n_xA^n_x$ and the counit $\epsilon\of A^n_xD^n_x\to\id$ ought
to be equivalences. This may be another hard to prove fact though. In any case
we are interested in the property that $h\ri D^n_x \simeq \id$, because form
there we get the fibrancy of the universe of modest fibrations\dots

We never got around to the fibrant replacements\dots.

The point of this construction was to avoid minimal fibrations,
which are non constructive. Do I remember why?

Extension instead of `descend', so look for a antonym to replace `ascend':
condensation, reduction, contraction, subtraction, diminution? 

\section{17/6/19}
Let's do this again. The set 
$\gamma_y = \set{ a\of \alpha_i | \gamma(a,\xi(y))=y }$ 
can contain mutliple elements and we have to be careful that they don't get in
each others way. Just consider the set of injections into
 $\product{i\of[n]-\set{x,\xi(y)}}\xi_i$.
There must be some reason we cannot pick the least element here and just use
that?

Our starting point is:
$(\bigcup_{i<n} U_{\delta^n_x(i)}) \cap (\bigcup_{j<m} V_{\delta^m_y(j)})$
And I think the problem is that these just may have no single point in common.
The intersection of $\bigcap_{i<n} U_{\delta^n_x(i)}$ has everything empty
except $\alpha_k$ and $\alpha_{k+1}$. The $V_j$ do the rest, but that seems to
leave us with a set of points to work with. 
The question is, is there any point in $U_i$ that cannot be extended by the
least point of $\product{i\of[n]-\set{x,\xi(y)}}\xi_i$?

The jumping around makes sense if we stick to $y$ as strating point, because
there is an opposing face that causes trouble. Also, faces can get in each
others way, which is a reason to be careful.

The problem is that $U_i\cap V_j$ really do not have any single point in common 
with each other, not even the members of to following set:
$\Gamma_y = \set{\gamma\of\product{i<n}\xi_{\delta^n_x(i)}| \gamma(\xi(y)) = y}$

I think $y$ may be a distraction, i.e. we may have to use it to glue a point of 
$\Gamma_y$ to a member of $V_j$, but using it to glue in everything just makes
things more complex. I am unsure.

The basic strategy is the glue in faces by dimension. This requires an $p(f)$ 
for each face $f$ such that subface $f\circ \delta_p$ is not glued in during the
 previous stage with all the others. Gluing in every face that contains
a specific point works because that point becomes $p$. That won't work with our
starting point though.

The `downsets' start to make sense: they describe a path to a point we want to 
get in first. We have to be specific though. $\gamma$ 
has to reach every element of $[m]$, otherwise it belongs to some $V_j$.

\paragraph{pushout product}
What we are dealing with is a kind of repeated pushout product:
$\horn_y(\xi_{\xi(y)})\Box\cycle(\xi_i)$

See, $\xi\of \simplex[m]\to\simplex[n]$ breaks up the horn 
$\horn_y[m]\to \simplex[m]$ into a list of cycles
$\cycle[\xi_i]\to\simplex[\xi_i]$ and a horn 
$\horn_y[\xi_{\xi(y)}]\to \simplex[\xi_{\xi(y)}]$
The inflation takes the product of most of these and glues them to the
original simplex. This should result in a simplex that is stable under
pullback.

\paragraph{can we not ignore?}
I wanted to focus on $\Gamma_y$, but it seems that we run into trouble then.
A $\tuplet{\alpha,\beta,\gamma}$ belongs to the complement when 
$\beta$ and $\gamma$ bother reach all points of $[m]$ (except perhaps $y$, but 
then we should be able to add $y$ somehwere). $\gamma$ can reach a lot of points
easily, but $\beta$ can compensate for everything that $\gamma$ misses.

So, let's try is this way. We only glue in faces where $\gamma$ has the 
following properties:
\begin{enumerate}
  \item $\exists a\of\alpha_k.\gamma(a,\xi(y)) = y$
  \item $\forall i\of[n]-\set{x,\xi(y)}. \gamma(\min(\alpha_k),i) = \min(\xi(i))$
  \item $\forall a\of\alpha_k-\set{\min(\alpha_k)}. b\of\Gamma_y. 
  \gamma(a-1)\leq b \leq \gamma(a) \to (\gamma(a-1) = b \vee \gamma(a) = b)$
\end{enumerate}
And of course, $\beta_m\neq \emptyset \vee \gamma_m\neq \emptyset$, otherwise
inclusion is not needed.

What I think we need is:
\begin{itemize}
  \item a point $p$ in $\Gamma_y$
  \item a `dense' $\gamma$ that intersects that point.
\end{itemize}
What does this do? The point $p$ cannot be removed and if we remove any other 
point, fuck! 

For most faces, the strategy is to add points to $\gamma$ until the conditions 
are satsified. 

Pick a point $p\of\Gamma_y$. We know it does not belong to $V_p(i)$ and we need
to be careful about this fact.

I think there should be two conditions to ensure $\gamma$ gets full before 
$\beta$ does. For the second condition, $\beta$ and $\gamma$ both ought to be
maximal. If we remove an element from $\beta$, the faces should be included
because of the rule for filling out $\gamma$. Removing an element from $\gamma$
leads to immediate problems, however.

Funny thing is, $\beta$ has to miss an entire range $\xi_i$ of $[n]$, otherwise
none of this will work.

\paragraph{the difficulties}
We need a condition, such that if $\gamma$ satisfies it, then 
all $\gamma\circ \delta_j$ satisfy it, except for one.
To add to the trouble, whatever the condition is,
all $\gamma$ that do not reach all of $[m]-y$ have to satisfy it.
The latter seems to make this impossible.
Okay, part of the condition can be that $\gamma$ reaches $y$, but that is not
enough. $\gamma$ can reach $y$ multiple times and more than once means more 
than one $\gamma\circ \delta_j$ that reaches $\gamma$.
We have to discount specific $\gamma$ that hit $y$ multiple times.
A specific point $p$ with $p(\xi(y))=y$ works better, except that removing any 
such specific point could land us in $V_p(i)$ for $i\neq x$ and $i\neq \xi(y)$.

Can it be made that simple: just ask that $p(i)$ are reached from some other
point as well? Adjacent in $y$ perhaps? i.e. $\gamma(a) = p$ and 
$\gamma(a',\xi(y))\neq y$, while $\gamma(a',j) = p(j)$ otherwise for some $a'$?

Looking at the examples, we more or less need the opposite.
I mean, we start with the faces that have full $\Gamma_y$ and gradually but
strategically remove elements to get dense $\beta$ in.

\paragraph{suddenly noticed}
We are asking that $f\circ \delta_k\of \bigcup_j V_j$ for all except one point.
This is a very severe condition actually\dots what the hell does it mean?
The removal of each point results in some $j\of [m]-y$ not being reached 
anymore, except for the end of this chain. In other words, every point reached
from the end of this chain is reached elsewhere.

More of a clear out operation then.
Could it be like this: there is a $j\of [m]$ such that $\beta \geq j$ and 
$\gamma \leq j$? Nope! $\gamma$ cannot be limited that way.
What about $\max_a(\gamma(a,i))<\min_a(\beta(i,a))$?
On one hand, overlap is not optional.

This has been the problem forever. I cannot get a solid grip on this part of the
problem, no matter what I try.

\paragraph{big picture}
Why is this true intuitively?
It is indeed a matter of using the pushout product multiple times.
It is also this idea of having supplied a support point for these
specific purposes.

If we could show that:
$U_{i\neq x}\cap V_{j\neq y} \to U_i$
Was an acyclic cofibration, would that not be enough?
A pushout of a coproduct of acyclic cofibrations,
Isn't that what we get?

Distribution for $U_i$ would work, but there could be disagreement precisely
on tha simplices we need to glue in, as they aren't covered.

But then, if we could show that for $i\neq x$
$\bigcup_{j\neq y} U_i\cap V_j \to U_i$
was an acyclic cofibration, we would be home right?

We went down this road and as long as $i\neq \xi(x)$
we can use $y$ as support to glue everything in.

The problem is $\bigcup_{j\neq y} U_\xi(y)\cap V_j \to U_{\xi(y)}$.
Still, not having the other around might be a blessing here.
I am unsure.

There is no single edge that belongs to all of $U_\xi(y)\cap V_j$,
but there is a system of interconnected edges.
Could we come up with a different cover then, based on $\Gamma_y$?
That would be nice wouldn't it?

But I thought differently.
Let $V'_j = \set{\tuplet{\alpha,\beta,\gamma}| \beta_j= \emptyset}$.
Now see if $V_j \cap U_{\xi(y)} \to V'_j \cap U_{\xi(j)}$ are acyclic 
cofibrations. Because $U_{\xi(y)} \subset V_j$ when $\xi(j)=\xi(y)$\dots
we need some help if $\xi(j) = \xi(y)$ means $j=y$.
Also $V_j \cap U_{\xi(y)} \to V'_j \cap U_{\xi(j)}$ aren't necessarily easier at
all.

We know that each $p\of \Gamma_y$ is missing from $V_p(i)$.
What about $w_p\of \bigcup_{j\neq p(\xi(j)) } V_j\cap U_\xi(y)\to U_{\xi(y)}$ as 
covering family?
Well, those would be reason to worry about singletons in $\xi$, since we seem to 
miss cover there.
I think we may just run into the same trouble we got into with splitting $V_j$
before: no reason to believe that we get a pushout of acyclic cofibrations,
because the pushout won't uniquely specify how to extend each face. I guess
this is why I use graded constructions in the first place.

\paragraph{pushout product}
This is a relevant insight. The morphism $\xi\of \simplex[m]\to\simplex[n]$ cuts
the inclusion $h\of\horn_y[m]\to\simplex[m]$ into a sequence of cofribations,
$h_i\of\cycle(\xi_i)\to \simplex(\xi_i)$ with one acyclic cofibration 
$h_{\xi(y)}\of \horn_y(\xi_{\xi(y)})\to\simplex(\xi_{\xi(y)})$. All except $h_x$
 are multiplied together and glued back to $h$. Then the whole structure is 
pulled back along $\horn_x[n]\to\simplex[n]$.

The product $\prod_{i\neq x} h_x$ is glued at a point that is stable under 
the pullback and because it is an acyclic cofibration, the result is one as
well. The rest is more delcate however, because the glueing is non-trivial and
because the pullback definately damages the other side.

Maybe that is the trick: to index the operation by the points left out.
It is the same set however\dots

Ok, there is no pushout to make this product work.

What if we cover $U_{\xi(y)}$ with maximal chains?
It probabaly does not get finer than that.

\section{16/6/19}
A general way to show that an inclusion of simplicial sets $f\of A \to B$ is to 
have a subset $C\of B$ of faces, such that for each $c\of C$ and each 
$i<\dim(c)$ except one $c\circ \delta^{\dim(c)}_i\of C$. That way, we can glue
in faces dimension by dimension and use that to proof it is an acyclic 
cofibration.

We are looking at this inclusion:
\[(\bigcup_{i<n} U_{\delta^n_x(i)}) \cap (\bigcup_{j<m} V_{\delta^m_y(j)}) \to \bigcup_{i<n} U_{\delta^n_x(i)}\]
The property that we want to use is reaching $y$ of $m$, but the faces of 
$U_{\xi(y)}$ cannot do that. That is why we need the extra $\gamma$'s.

So we trace out the difference, faces of $U_{\xi(i)}$ that aren't members of
anything else. Firstly, all $z\of [m]-\set y$ have to be represented somewhere,
but because $\xi_{\xi(y)}$ is excluded, all $z \of [m]$ such that 
$\xi(z) = \xi(y)$ but $z\neq y$. 

I think it is best to snake my way up in here:
$\product{i\of[n-1]}\xi_{\delta^n_x(i)}$. Then at the end, add $y$ to finish
everything off.

$\gamma_y$ can contain multiple components and that is the issue. The potential
 maximum is $\prod_{i\neq x,i\neq \xi(y)} \xi_i$ and this we solve using
 initial segments.

\section{12/6/19}

\paragraph{A better representation of the inflated simplices}
Let $\xi\of [m]\to[n]$ and let $x\of[n]$. The inflated simplex $S\tuplet{\xi,x}$
 for this pair consist of tuples of the following form. 
\[\tuplet{
  \alpha\of[a]\to[n+1], 
  \beta\of\product{i\of[n]}(\alpha_{\delta^{n+1}_x(i)} \to \xi_{i}),
  \gamma\of\alpha_x \to \product{i\of[n-1]}\xi_{\delta^n_x(i)}
}\]
The simplicial action is now obvious, because the partial functions can simply 
be composed. The faces are injective maps, i.e. in 
$\tuplet{\alpha,\beta,\gamma}$, $\beta$ and $\gamma$ are injective.

The only missing data is that to be limited to $\horn_x[n]$--there must be an 
$i\of[n-1]$ such that $\alpha_{\delta^{n+1}_x(\delta^n_x(i))}=\emptyset$. I keep
 calling this family $U_i$:
\[U_i = \set{\tuplet{\alpha,\beta,\gamma}\of S\tuplet{\xi,x}|\alpha_i = \emptyset}\]

For the inflated $\horn_y[m]\to\simplex[m]$ we only get tuples that avoid the 
value $y$. There are inclusions 
$S\tuplet{\xi\circ \delta^m_j,x}\to S\tuplet{\xi,x}$ and we want to describe the
 images, which are $V_j$:
\[V_j = \set{\tuplet{\alpha,\beta,\gamma}\of S\tuplet{\xi,x}|\beta_j=\emptyset,\gamma_j=\emptyset }\]
This ominous fibres over $j$ take advantage of the fact that we ultimately end 
up in $[m]$.

There is a third family: $p\of\product{i\of[n-1]}\xi_{\delta^n_x(i)}$. One 
demand actually:
\[W_p = \set{\tuplet{\alpha,\beta,\gamma}\of S\tuplet{\xi,x}|
	\forall a\of\alpha_x.\beta(x,a)=x,\forall i\of[n-1], a\of\alpha_{\delta^n_x(i)}.\beta(\delta^n_x(i),a)\geq p(i)
}\]

See (28/9/17). We have a different representation that may be easier to work 
with, but the proof went like this. To prove the following map is an acyclic 
cofibration:
\[(\bigcup_{i<n} U_{\delta^n_x(i)}) \cap (\bigcup_{j<m} V_{\delta^m_y(j)}) \to \bigcup_{i<n} U_{\delta^n_x(i)}\]
Let $A_k$ consist of all less than $k$ dimensional simplices 
$s=\tuplet{\alpha,\beta,\gamma}\of\bigcup_{i<n} U_{\delta^n_x(i)}$ that satisfy 
one of:
\begin{itemize}
\item $s\of \bigcup_{j<m} V_{\delta^m_y(i)}$--i.e. it is in from the start
\item $\beta$ reaches $y$.
\item $\gamma$ satisfies a special initial or final segment condition.
This condition requires more explanation.
\end{itemize}

\section{14/1/19}
It is difficult to solve the problems for arbitrary categories of generic cofirbations, but for mere families, things are more or less clear now. I mean, I was struggling to understand the morphisms given an arbitrary base category, but I never solved that problem and I don't need to.

\begin{enumerate}
	\item Start with a family of \emph{generic cofirbations} and a family of small objects and create a new category of pushouts of generic morphisms with small domains.
	\item Create a new diagram whose objects are witnessed by zigzag chains, while its morphisms are limited to specific forms.
	\item The density comonad for the latter category is the factorisation system.
\end{enumerate}

Now I think the zig zag chains don't actually help as witnesses. The codomains don't have to be small. So we need something like small joined with a finite number of codomains.

Here is the problem: I have a construction I don't know how to internalize and an internalized structure that doesn't fit into my proof. 

\paragraph{What works?}
There is a finite composition $X_0\to\dotsm\to X_n$ starting with a small $X_0$ and a sequence of generic cofibrations $a_0,\dotsc,a_n$ and morphism $f_i\of \dom(a_i)\to X_0$ such that the morphism $X_i\to X_{i+1}$ is the pushout of $a_i$.

This recursive type may not exist in the general sort of category we are looking in. That is the problem. So I am looking for a work around with the family of small objects.

In the motivating example this is not even a problem. The codomains are representable--as in 'could hardly be more finite.' This is the simplest case: there is a dense full subcategory (full diagram?) which contains the domains and codomains of the generic cofibrations.

Witnessing of cofibrance consist of breaing up a morphism into components and showing each of them is a pushout. I believe we don't need retracts or transfinite compositions at this stage.

So, we end up with a diagram of cofibrations and certain simple morphism between them, which has a dense diagram of domains and is directed. Now the density comond provides morphisms which factor as cofirbations followed by fibrations.

Interesting note: the 'full' diagrams and the 'families' are the final and initial object in the category of diagrams with the same objects, which is why we need no distinction.

To finish the paper, we focus on the case where there is a family of generic cofibrations, whose domain and codomains belong to a given dense diagram. Everything else should then kick in to get the desired results.

\section{17/12/18}
What are the morphisms in the category of transfinite zig-zag chains?
\[\xymatrix{
	C \ar[r]^a \ar[d]_c & D \ar[r]^b\ar[d]_d & \nno\ar[d]^s\\
	C \ar[r]_a \ar[ur] & D \ar[r]_b & \nno
}\]
For starts we could simply consider the straightforward morphisms that preserve all the structure.

The problem with transfinite composistion of cofibrations is that the codomains of the generic cofibrations don't ordinarily have to be small. We run out of small object too soon, which is a problem, because it means we cannot keep the catgeory of generic cofibrations small by keeping the domains small.

The inifitrary chains should be easier to work with than a collection of finite chains of all length, inclusing giving a simpler definition of morphism. On the other hand, we now need more morphisms to keep the factorization clean. Still, I'd say the simplest proposal is good enough. Ignore the zigzags and allow reindexing. Given $\tuplet{a,b,c,d}$ as above and a similar tuplet $\tuplet{a',b',c',d'}$, then a morphism $\tuplet{a,b,c,d}\to\tuplet{a',b',c',d'}$ is a morphism $f\of a \to a'$ with a zero preserving increasing morphism $g\of N\to N$ that commutes with $b$:
\[
\xymatrix{
C\ar[r]^a\ar@{.>}[d]_{f_0} & D \ar[r]^b\ar@{.>}[d]^{f_1} & \nno\ar@{.>}[d]^g\\
C'\ar[r]_{a'} & D'\ar[r]_{b'} & \nno 
}\]
So, the zero presevring increasing morphism emphasizes that we care about the result of the infinite composition, but the individual steps aren't important. The zigzag is evidence for the left lifting property and it is unique when cofibrations are monic, but this evidence is ignored by the morphism, as it doesn't matter for the result.

The reason tranfinite compositions can be composed is that we are working inside an exact ambient category $\ambient$. I.e. $D_\infty$ is a quotient of $D$, by an inductively defined equivalence relation based on the chain of morphisms $D_i\to D_{i+1}$. This defines a new diagram if transfinite compositions in the ambient category.

\paragraph{Finite zigzags}
At this point is may be interesting to consider 'terminating compositions'. So from some $i$ on, $a_{i+1} = a_i$. Bringing back the finiteness this way, the smallness starts to pay off more clearly. 

Now that we know how to do it in the infinite case, we can start considering zigzags over initial segments of $[n]$ and introduce the same kinds of morphism. This time, everything is nice and finite, however.

Doubt is creeping in again. 
It looks like my notion of morphism picks a member of the target to embed into. 
Yeah, we are actually ignoring the tranfinite composition itself. We need to treat the transfinite compositions as diagrams on their own.

Take the finite zigzag and reverse the order. The result is a diagram of simplicial objects coming from another diagram of cofibrations. Once we pay attention to the actual compositions, however, the zigzag can be safely ignored. They are just evidence that the whole composition taken together is a cofibration.

\paragraph{Recap}
Given a diagram of generic cofibrations and a dense diagram, we first combine this into a diagram of generic extensions of small objects and then we take tranfinite compositions as above. We (may) then still need to add identities of small objects as cofibrations. The result is a diagram whose density comonad is supposed to be a factorisation system. How would that work?

The problem is that after factoring $f$ as $r(f)\circ l(f)$, $r(f)$ should have the right lifting property. Because any generic cofibration $c$ has a small codomain, any morphism $c\to r(f)$ should factor through some finite--or at least small--approximation of the factorisation. The pushout is simply another such finite approximation.

The zigzags are now in the way aren't they? It is actually harder to work with these structures now.

\paragraph{Relevance}
In the saturated diagram a morphism tells us something about the lifting property. The morphisms point out potential relations between fillers for the cofibrations. At the same time, some morphisms are needed to get a directed category of cofibation te work with. This is the trouble now. If we don't start with a family, but with a diagram of generic cofibrations, we may break connections that this initial digram has. Adding morphism too carelessly can result in a loss of directedness, however.

Everything is still at stake.

\paragraph{Insight}
We allowed pushouts and compositions as morphisms. Then added morphisms from the base diagram to intervene. With the compositions intervening, it is still okay to let gaps fall between the composites, because it follows the same principles.

The challenge is directedness. This is automatic for sums, but parallel pairs must have coequalizers too. That is the hard part. Morphism have to be limited to eliminate parallel pairs that have no coequalizer. However, the generic diagram may contain morphisms that complicate matters.

I should write what I know and perhaps what I need. If I cannot tell if my construction can handle arbitrary diagrams, just do the discrete version. If I cannot extend fibrations constructively, just do it classically. Leave it to other to work out the full idea.

\paragraph{Generic parallels}
I don't really know what to do with these anyway. Meanwhile, the idea of a finite composition of pushouts of generic cofibrations still works well.

\section{16/11/18}
I have no better idea than the zigzag chains for completing the diagram.

Recap: any diagram in the category of arrows can be combined with a diagram of small objects, so the density comonad becomes a factorization of morphisms.

The zigzags solve the problem that all domains are small, but codomains don't have to be. Meanwhile, they don't solve the problem of missing identities and introduce the problem of to define morphisms between them.

\paragraph{Compositions first}
I have been considering this, but it looks like it cannot work out. Suppose we have a sequence of generic cofibrations $a_i$ whose pushouts compose to form a new cofibration. Vital data about this composition is part of the pushouts, especially about what parts of the domain of $a_i$ are covered by the domains of $a_j$ for $j<i$ and which are part of the domain of the full composition.


Perhaps this can be mitigated with the transfinite composition diagrams.
I.e. we have the morphism:
\[\sum_{i<\omega} a_i \of \sum_{i<\omega} dom(a_i)\to \sum_{i<\omega} dom(a_i)\]

This just seems silly. Freely add transfinite composition by using these obvious `algebras' on the category $\ambient^\omega$. Why wouldn't that work?

The obvious problem is that domains and codomains of generic cofibrations can fail to match up. The solution seems obvious now. Use transfinite zigzags instead:
\[\xymatrix{
C \ar[r]^a \ar[d] & D \ar[r]\ar[d] & \nno\ar[d]^s\\
C \ar[r]_a \ar[ur] & D \ar[r] & \nno
}\]
The composition is still the initial constant zigzag this embeds into.
Why do I like this? Because I expect that these definition simply the definition of morphism between transfinite compositions.

\paragraph{Finite colimit options}
The transfinite composition is a kind of diagram. What if we use a diagram over small categories instead?
We get a kind of closure under small colimits that could kill two bord with one stone.

The idea is that the diagrams we are interested in are exists in the category of cofibrations and zigzag morphisms. 

This isn't going anywhere, because zigzags don't compose.



\section{3/11/18}
Instead of transfinite compositions, use zigzag chains:
\[\xymatrix{
A_0 \ar[r]\ar[d] & \cdots \ar[r]\ar[d]\ar[dl] & A_n \ar[d]\ar[dl] \\
B_0 \ar[r]& \cdots \ar[r]& B_n
}\]
The vertical morphisms are from the diagrams to be completed with compositions. The composition from top left to bottom right is what matters.

\section{2/11/18}
I am unsure if I will be working on this for much longer. It has taken too much time and I feel like I am getting further of target. 

\paragraph{Factorization system}
It now makes sense to me to break up the construction along the way Garner outlined. First turn it into a factorization system, using a dense diagram. At this point the question of what counts as a morphism is relatively easy.

A diagram in the category of arrows looks like this: $ A\stackrel{a}{\to} B\to I_0$, where $I_0$ is the object of objects of an internal category and the arrows in $I_1$ act on both $A$ and $B$. A dense diagram will look like this: $S \to J_0$. So, what we are looking for is tuples:
\[K_0 = \set{\tuplet{i\of I_0,j\of J_0,f\of A_i\to S_j}}\]
Which exists in locally cartesian closed categories. This is just the object of objects of the category. The morphisms are like:
\[K_1 = \set{\tuplet{i\of I_1,j\of J_1,
c\of A_{\cod(i)} \to S_{\cod(j)},
d\of A_{\dom(i)} \to S_{\dom(j)}
}\middle| c \circ a_i = S_j\circ d }\] 
To get a new diagram in the category of arrow we need a little more.
\begin{align*}
C &= \set{\tuplet{i\of I_0,j\of J_0,f\of A_i\to S_j, s\of S_j}}\\
D &= \set{\tuplet{i\of I_0,j\of J_0,f\of A_i\to S_j, s\of B_i +_{A_i} S_j}}\\
c\tuplet{i,j,f,s} &= \tuplet{i,j,f,i_1(s)}
\end{align*}
where $i_1\of S_j\to B_i+_{A_i}S_j$ is the pushout of $a_i$ along $f$.
The dependent pushout is a challenge met by any extensive and exact ambient category.

So there it is. The density monad $c\of C\to D$ produces pushouts of $a\of A\to B$ and hence a factorization system. That is my claim at least.

Basic proof strategy: sheaf reduction? The density comonad of $a$ looks like $(f^a)\otimes a$ and similarly that of $c$. So morphisms between $a$ and $c$, or $f^a$ and $f^c$ and show that these objects have to be similar. The simplest strategy is to looks at the relation between $a$ and $c$ and $\cat I$ and $\cat K$ in particular.

Obviously, there is a forgetful internal functor $F\of \cat K\to \cat I$. Smallness of the bundle $A\to I$ induces an inverse functor $\cat I\to \cat K$. Here we have a connection to the original small object argument. The functor $F$ already induces several functors between the categories of sheaves.

The idea is now that $(f^c)\otimes c$ has isomorphic domains to $f$ and is a pushout of $(f^a)\otimes a$ and this together makes the density monad of $c$ the factorization system got by pushing out out the density monad of $a$.

Let think both parts through. 
\paragraph{sharing domains}
The diagram $S$ being directed may be important now too and even a condition not met yet by the construction. My feeling is that if we have two pushouts $p_*(a_i)$ and $q_*(a_j)$ we need to factor those through some sort of union of their domains. Even if this is already possible in $S$, the new diagram $c$ breaks up those unions.

I think the best solution is to close the diagram $a$ under finite coproducts first and only then get to the dense and directed domains. It should be finite coproducts and we do destroy pre-existing finite product in the process if we are not careful.

I took the finite coproduct out for simplicity, believing that the second step would add them back in. What is going on then?

This could be a mistake. There are many object of $\cat K$ map to each elements of $\cat I$ through $F$. If the fibres of the functor are directed, however, we may be able to reduce the density monad of one to the other.

If we have $\tuplet{i,j,f}$ and $\tuplet{i,k,g}$, then we need a pushout $\tuplet{i,l,h}$. With those pushouts, the density comonad of $c$ reduces to $a$. Because $h$ is the diagonal in the pushout of $f$
and $g$, there is no room for breaking approximations up.

So, the fibres have to be closed under these pushouts. $S$ should have finite colimits, so the fibres of $F$ can have them too. The result is
exactly what we need.

Conditions on smallness:
\begin{enumerate}
\item density, so each object of $\ambient$ is reached by the density comonad,
\item finite colimits of small object are small,
\item the map $A\to I_0$ is small.
\end{enumerate}

\paragraph{Transfinite composition}
The second part of the construction is still a bit vague. The objects are chains of zigzag squares between morphisms. Beyond that, I have no grip on the morphisms yet. Yes, pushout factorization, what does that mean?






\section{5/10/18}
What I have right now, is a combination of properties that imply each other that together tells us a diagram is presaturated.

\section{30/9/18}
Maybe just start with more assumptions on the diagrams, keep on factorizing the proof all the way back to the family of generic morphisms.

So let a diagram have:
\begin{enumerate}
\item dense domains;
\item directed or even having small colimits;
\item the pushouts;
\item the compositions.
\end{enumerate}
I have to figure out what that means exactly, because I have tried and apparently not gotten far enough.

\section{21/9/18}
Given a diagram of the arrow category, there should be a construction for a larger diagram, whose density comonad serves as a factorization system. This exists because the ambient category is a $\Pi$-pretopos with a natural number object. At least that is what I am trying to prove.
The construction of the larger diagram is still a mystery, however.
Transfinite composition is the mystery. Last time we dealt with pushouts and translated them into conditions that relate to density and available morphisms.
I have looked into the composition part. 
This is the situation we have to deal with:
\[\xymatrix{
A_0\otimes D\ar[d]_{a\otimes d} \ar[r] & B_0\otimes D \ar[d]^{b\otimes d} \\
A_1\otimes D\ar[ur]|{\sim} \ar[r] & B_1\otimes D
}\]

The composite should also be represented by a sheaf.

\paragraph{targets}
We are looking for something that looks like $A\to B\to I_0$, a morphism is diagrams actually, because there are morphisms and actions involved. We start with such a structure and modify it it ensure that the domains are directed and dense, while the whole structure is closed under compositions in a suitable sense.

\paragraph{pushout out factorization}
Given pushouts in $\ambient$, $\ambient/\ambient$ has a factorization system where each morphism is a commutative triangle following a pushout square. We simply restricted the commutative triangles to specific kinds.

\paragraph{up-to-iso problems}
Anodyne extensions are closed under composition. When we use a diagram, however, we are not dealing with a property that any morphism can have, but specific instances that are singled out. We probably cannot ask for a structure that is closed under all isomorphic object. So we are stuck with mitigation isomorphisms all over our constructions. This sucks.

Suppose the first first step is just closure of a diagram under finite sums and some of their morphisms. Just the get rid of that part of the problem. 

The compositions have the lifting property because of the inverse of the
isomorphism actually:
\[\xymatrix{
A_0\otimes D\ar[d]_{a\otimes d} \ar[r] & B_0\otimes D \ar[d]^{b\otimes d}\ar[dl] \\
A_1\otimes D \ar[r] & B_1\otimes D
}\]
So forget about compositions isomorphisms and worry about these instead.
We are not limited to specific commutative squares here.

The weakening to more general morphisms only makes things a little bit easier, though. Diagrams still require rather odd structure.

\paragraph{Back off}
This was the idea: the density comonad is actually a factorization system, with $l(f) \simeq f^d\otimes d$. Given a `morphism from the original diagram'--whatever that means--we ask for the left lifting property with respect to $r(f)$.

So instead of a `morphism from the original diagram' we need something to stand in, like $a\otimes d$ with an arbitrary sheaf. I end up with $r(f)^d$ being split epic (at least) and perhaps even an isomorphism\dots but too much seems to follows form just the density comonad.

I am missing something about the density comonad, because it should not be so straight forward that the diagram is essentially closed under composition. 

A lot comes from $r(f)$ being part of the counit of the comonad. This is part of the point of using the density comonad. But now it look like we don't have to proof anything about compositions or density anymore.
It is not that simple. The adjunction makes $r(f)^d$ is a split epimorphism, but the assumed lifting properties tell us it should be an isomorphism.

Counit is isomorphism is equivalent to a fully faithful left adjoint $-\otimes d$. A, but that is not the property we are looking at here. Only the $^d$ applied to the counit of the density comonad gives the isomorphism.

\paragraph{algebraic selection}
I suppose we could start with the sheaves and then get a diagram be selecting particular ones, the algebras for the codensity monad for example. What does that actually do? 
The unit $f \to (f\otimes d)^d$ would have an inverse of some sort that
sends a family of equivalence classes to some pre-image. This touches on
something deep: $f$ is a way to build acyclic cofibrations and
the algebra makes that construction recursive.

Yeah, this should be a problem because we would miss out on the compositions.

The Garner way is more like: the right factor in the construction eventually becomes an isomorphism. But the proof relies on locally presentable ambient categories, which is what we try to work around here and I am unsure how to proceed.

Getting a new diagram this way is probably just a silly dream.

\paragraph{Another sketch}
First consider finite colimits generated from the diagram. At this stage we don't look at morphism too closely. We do want to include identities among the building blocks.

No, try another way. Sheaves act as blue prints for morphisms. Isn't a sequence of sheaves what we are looking for then?
Not in isolation, because we need to push the constructed object out to the correct place.

So a sequence of pairs, where each pair is a sheaf $f_i$ and a morphism $g_i\of \dom(f_i\otimes d)\to X$ to push $f_i$ out along.
Instead of a morphism $g$ could be a cocone, as a way to get it smaller.
Better yet: make is a sequence of pushout squares that match up correctly.

The problem is representing this complex structure as some object of the ambient category as ever.

Extending the diagrams with finite coproducts and their pushouts and the special morphism between them are one step in the direction of making things simpler. We no longer need the pushout, because we can represent them directly\dots
Perhaps we can even stick with certain coequalizers.

\paragraph{Isn't this nuts?}
The cycle and horn inclusions from generic sets, but why want such a set at all?

Smallness of the codomains means we need to take such colimits in account in composition. 

I am using sleepiness, loneliness, sadness, etc. to hide the fact that I am unsure how to solve these problems.

\paragraph{back}
Step one takes pushout of small colimits of the elements of the first diagram and identity morphisms in order to gain a diagram that
\begin{enumerate}
\item is dense on identities (and domains)
\item is small directed
\end{enumerate}
The small directed part should mean something like $\hom(\kappa, f\otimes d)\simeq \kappa\to\hom(1,f\otimes d)$ for small $\kappa$. I don't know if we really need this now. Perhaps just adding certain pushouts is sufficient.

The density just gets rid of the sums and pushout steps of the construction.

For the transfinite composition step, add finite composition to the diagram.

\paragraph{left morphism building kit}
I like this idea of creating a category of left morphism recipes, explaining how to glue together the components until the full morphism comes out. Such a construction could confirm that we have all the left rules in place.

\paragraph{Moving on\dots}
Don't I have a pretty good idea what to do now? I am afraid that I don't because I keep making the same mistakes and there are just too many details I fail to keep track off, no matter what I try.


\paragraph{trying to redistribute}
Keep the first step simpler: assume a diagram of small objects and create a new diagram of pushouts of generic fibrations to small objects.
The second step uses the zigzag squares to get composition functioning.
This unlikely couple, together with the special morphisms should ultimately do it.

Maybe better next time.

\section{7/9/18}

A little recap. I found that for a diagram over of the category of arrows with particular qualities the density comonad is a functorial factorization system. The following properties seem necessary:
\begin{itemize}
\item density and direction of the domains
\item closure under pushout and composition
\end{itemize}
These make the diagram \emph{presaturated}.

There is a construction of a presaturated diagram from a general diagram, relying on spans of morphisms, freely adding pushout and compositions and ensuring a dense and directed set of domains.

I think the external version is pretty straightforward, but I want something that works inside realizability categories. The trouble is, I don't really know how to go about this presaturation step internally.

In an effort to understand the requirements and the construction better, today I should start with sketching the proof and working backward\dots

\paragraph{left morphisms}
Back off a bit.

I think a diagram $D$ over $\ambient/\ambient$ 'generates' morphisms by taking tensors with presheaves in $\ambient$.  
Interesting point: tensors with presheaves in $\ambient/\ambient$ doesn't work. That brings in too many morphisms.
Though the class of left morphisms that occur as tensors with diagrams is large, is generally won't be the entire class of left morphisms. 

This construction tries to select a suitable class of left morphisms and morphisms between them.
It may in fact have little in common with the original diagram.

This only complicates a sketch of the proof: what do we have to go on?

\paragraph{new thought}
Density inside a subcategory of $\ambient/\ambient$: only the morphisms we identified earlier.

It would simplify presaturation, or perhaps make it more exact. It would not be correct though: only left morphisms should be generated. I mean: with only pushouts and commutative triangles, we have too few morphisms to cover morphisms that aren't left morphisms already.

I suppose the density comonad should be full.

This is confusing.

The idea is that we look at the subcategory of the category of arrows whose morphism are compositions of:
\begin{itemize}
\item pushouts
\item `commutative triangles', actually $\tuplet{a,b}\of c\to d$ where $a$ is an isomorphism.
\item retracts
\end{itemize}

In this category the density comonad of the diagram that generates the left morphisms cannot be isomorphic to identity comonad, because not all morphisms are left morphisms. It cannot be full because we admitted too many commutative diagrams.

This isn't going well.

\paragraph{sketching the proof}
The diagram $D$ is modified to have left morphisms with small codomains as objects and commuting square of a special type as morphism. This category is closed under finite colimits, pushouts and small coproducts for arguments given below\dots

This is the point: getting the left factorization as a directed colimit of generic left morphisms. This, however, requires that we work of a much more saturated basis. Why do I want it to be directed though?
The idea is that the closed under pushout somehow follows: the pushout of each finite approximation is itself a finite approximation and the colimit of the pushouts is the pushout of the colimit.

Pushout along what?

This is the point. Let $l\of A\to B$ be a left morphism and $f\of A\to C$ be random. The pushout $p$ of $l$ along $f$ is supposed to be isomorphic to something in the image of the density comonad. Why? I don't think I really get the problem here. What is it that we have to prove?
All small approximation of $f$ are already in the pocket. 

It is as if we want operations of the presheaf categories that witness closure under the desired operations.

Each small approximation $L'$ of the domain of $l$ factors through a small approximation $P'$ of the domain of $p$. So what?
What do the pushouts help us here? Something about the colimit and the pushout commuting. I.e. pushouts of all small approximation together are a pushout of $l$ along a morphism that factors through $f$\dots but how does that help us?

The density of the domains ensures all of the codomain of $f$ is covered, while the approximation argument takes care of the codomain of $f$. Careful though: we combine small identity morphisms from the codomain of $f$ with small approximations of $l$.

We can turn identity morphism into sheaves\dots and somehow get $(\id(\dom(a\otimes d)))^d\to a$\dots I think. At least that gives us a pushout in the category of sheaves that could be the one we need.

A condition comes forth: enough identities must be in there. Density on identities. 

\paragraph{pushouts}
We derive closure under pushout form two conditions on $\otimes d$: it must be dense on identities, as well as be full on commutative squares of two particular (degenerate?) types. If so, there is a pushout in the category of presheaves of which the original pushout is the image (up to isomorphism). 

I have to record the diagram, but I need a break now.

The commutative squares are still reasons for caution.

\[\xymatrix{
& C \ar[r]^\id \ar[dr]^(.75)\id & C \ar[dr]\\
A\otimes D \ar[ur]^f\ar[dr]_\id\ar[r]^\id & A\otimes D\ar[ur]^(.25)f\ar[dr]_(.25)l & C\ar[r] & \bullet \\
& A\otimes D \ar[r]_l\ar[ur]_(.75)f & B\otimes D\ar[ur]
}\]

So, this looks like an alternative to the pushout condition that connects to density more directly. 
Next time, let's see if we can find something like this for composition.


\section{24/8/18}
Time to bang my head against thee problems again.

The small object argument relies on the smallness of the domains of the generic cofibrations. I don't know what to ask from generic diagrams to replace this property. So let's try something else this week.

Starting with a diagram, describe possible constructions of its. Then try to prove that the result is indeed presaturated.

\paragraph{small sums}
Isn't this obvious?

Coproduct completions for internal categories, combined with the 'obvious' operation on the diagram.

Let's take this slow. Simply add finite coproducts at first. So lists of objects will be the new objects. The new morphisms already present a challenge, since in order to be proper coproducts, we need to add coproduct injections and codiagonal maps.

Rather than lists, consider functions from and between finite sets. Here we run into an important difference between product and coproduct completions. Each member of the source must go to some member of the target in the coproduct completion. Each member of the target must come to some member of the source in the product completion. But neither case has to satisfy both, thank to structural morphisms.

In other words, the free coproduct completion of an internal category $\cat C$ takes functions from finite sets to the object of objects $C_0$ as objects. A morphism $\tuplet{x,f\of x\to C_0}\to\tuplet{y,g\of y\to C_0}$ is a pair of functions $\tuplet{h\of x\to y,k\of x\to C_1}$ such that $\dom\circ k = f$, $\cod\circ k = g\circ h$. Nice.

This is a construction involving the full diagram of finite objects and this specific diagram could be replaced with an alternative full diagram of small objects.

Consider a diagram over $\cat C$. This is mainly a morphism $d\of D\to C_0$ with an action from morphisms. 
The completed version should preserve the new coproducts, so $D'$ should be something like this:
\[ \set{\tuplet{x,f\of x\to C_0, a\of x, b\of D}| f(a) = d(b) }\]
The morphism $d'\of D'\to C_0'$ should be obvious. Now the action of the morphisms. For $\tuplet{h,k}\of\tuplet{x,f}\to\tuplet{y,g}$:
\[ \tuplet{h,k}\cdot\tuplet{x,f,a,b} = \tuplet{y,g,h(a),k\cdot b}\]
This is pretty straightforward actually.

In what sense has the diagram gained coproducts now?

Since the terminal object is finite, there is an embedding $\cat C\to \cat C'$ and we can say something about coproducts being isomorphism to members of the diagrams.

\paragraph{alternative}
Presheaf toposes are famously free colimit completions, so could we use that here? I think that relies on $\hom$, which suggest that the only way is to have an enrichment in a more complete internal category.

Rather than using this for coproduct only, start with a category that already has pushouts and transfinite colimits and probably also products.

This suggest that there could be a generic category $\cat G$ of objects and morphisms, which already has the desired properties and can be used to complete the 

I doubt that this really works. It won't be the free completion, but instead add a bunch of extra colimits that get in the way of what we need. The presheaf categories are only a free completion by actually being the terminal solution to an impredicative problem.

\paragraph{pushouts}
The point is to get a directed colimit for the density comonad. Pushout are a mean to that end. But rather than having a collection of small object to push arrows out to, we should consider pushouts that are coequalizers.

Note that this does not come for free. In fact, the diagram we complete this way cannot have too difficult morphisms in it.

Maybe we shouldn't stick use a coproduct completion, but the family of small colimits.

\paragraph{composition}
Maybe the coproducts are the easy parts.

Consider a diagram in the category of arrows and represent compositions of the morphisms it contains.

Start with list of the objects in the internal category $\cat C$. The diagram turns this into a list of morphisms. The domains and codomains won't ever be equal, however. Moreover, we only have one empty list of morphisms.

I guess I am missing something about identities and isomorphisms. A property of presaturated diagrams perhaps: every identity is represented by the diagram. Let's not dwell on that now.

Equalities of domains and codomains is a problem, isomorphisms is not. So the objects of $\cat C'$ are not just (nonempty) lists of objects of object of $\cat C$, but also of isomorphisms between the codomain of each function to the next.

The diagram is not longer a problem, the iso's are clear enough. But what are the morphisms of $\cat C'$? 

I know I need the initial segments. But we cannot just throw the rest out.

It looks like we will destroy every bit of structure that the internal diagram used to have and replace it with very particular diagrams.

\paragraph{pushouts}
Here the only recourse seems to have a diagram of small objects and then to build a new diagram of morphism by pushing out morphism in all possible ways.

The idea is to take pair of objects and then involve the diagram through a morphism. The target diagram uses a pushout along that morphism.

\paragraph{Conclusion}
I don't really see where smallness comes in yet. Maybe I need to actually sketch the presaturation proof and step through it. Let's try that next time.

\section{10/8/18}

Ingredients:
\begin{enumerate}
\item the diagram of generic left morphisms $L$ in $\cat A/\cat A$
\item the dense diagram $s$, with extra demands\dots
\item the natural number object
\end{enumerate}
The extra demand also has to do with composition, but is more subtle. For each internal presheaf $a$ over the same internal category as $s$, there is a morphism $a\otimes s\to a\otimes \top$, where the $\top$ is the terminal presheaf. When morphisms of this form compose up to isomorphism, their compositions ought to be members of $s$ as well. One way to explain this is to lift $s$ to the category of arrows with the help of $\top$ and demand the same closure under composition we saw before.

Small coproducts is the first goal. 

The internal categories become more active now, so let's name them. $\cat L$ is the category of generic left morphisms and $\cat S$ that of small objects. The small coporducts are indexed by functors $\cat L\to\cat S$.

The presaturations object are finite chains:
\[\xymatrix{
&\bullet \ar[dr]\ar[dl]&&\bullet\ar[dr]\ar[dl] &&\bullet\ar[dr]\ar[dl] &&\bullet\ar[dr]\ar[dl] &\\
\bullet &&\bullet &&\bullet &&\bullet &&\bullet
}\]
The morphism pointing left are small coproducts of generic left morphisms. The morphisms pointing right are arbitrary, except that the last one has a small codomain. This chain ought to represent the composition of its pushouts. The natural number object together with locally cartesian closure implies that this is representable.

I don't think the chains help with defining morphisms. Instead look at the left morphism they represent and then use the condition that each morphism of morphisms is a pushout followed by a composition.

To prove that the result is presaturated\dots

Closure under pushouts: density is part of it, as well as closure under certain coproducts. May this is the place where the preservation of colimits comes in more than in proving composition. Or maybe there is a more general property to consider that takes care of both.

\paragraph{internalized smallness}
We consider a diagram $d$, even though that may be more general than we need. We want to say that the objects preserve internal coproducts indexed over themselves. Rather self referential\dots how do we go about it?

One idea is that we can single out a class of $d$-small morphisms, morphism isomorphic to $f\otimes d\to f\times \top$ for some presheaf $f$ over the same internal category $\cat D$ as $d$. If this is closed under composition that means $d$ indexed coproducts of `elements of $d$' are themselves `elements of $d$'. This is a tough concept.

We want something like internal functor $\Sigma\of \cat D^d \to \cat D^\top$ left adjoint to the diagonal to drive how the point. Of course, a $\Sigma\of \top\otimes(\cat D^d) \to \cat D$ works just as well. 
So the idea is that left exact functors preserve internal categories and hence it makes sense to talk about the left adjoint between two internal categories in the category of presheaves over $\cat D$. This should be equivalent to the composition thing.

These first two can be connect through a universal composition. 

I am taking for granted that $d$-small morphisms are closed under pullback. Suppose $b\of B\to A$ is the pullback of $d(f)\of f\otimes d\to f\otimes \top$ along $a\of A \to f\otimes \top$. The morphisms of presheaves $a^\top$ and $b^\top$ have pullbacks $a'$and $b'$ along the unit $f\to(f\otimes \top)^\top$. Now $a'\otimes \top$ is isomorphic to $a$ and $b'\otimes \top$ is isomorphic to $b$ because\dots $^\top$ is faithful?

Perhaps closure under pullback is a property of diagrams over discrete categories that does not hold more generally. I don't see the general case holding.

This complicates some matters, but it might not be important for the end result.

Ultimately I need prove of presaturation. What do we need here?

I cannot really see it now. I am trying to imagine a stage in the proof where some functor needs to preserve small coproducts, but cannot.

\paragraph{Which functors?}
If an object is small $S$, it is $\hom(S,\cdot)$. What is this for a diagram of small objects? Sound like presheaf builder $d\Rightarrow$ should do something. At the same time that seems limited, because we are not considering morphisms to arbitrary objects, but cocones. Yes, intuitively, $d\Rightarrow -$ is the presheaf of cocones with given codomain.

Consider $\hom(f\ri(s)\otimes d,-)$ where $f\of \cat D\dual\to\cat S$ is an internal functor. We could introduce the notion of `small presheaf' over $\cat D$ which means that it is the result of taking pointwise colimits of a presheaf over $\cat S\times \cat D$. This feels comforting\dots

\paragraph{Continue\dots}
It should be a matter of unexpected commutativity:
\[ \hom(a\otimes d,b\otimes d) \simeq \hom(a\otimes d, b)\otimes d \]
This does not make sense yet: even the types don't match up properly.

Maybe something like the 'canonical map has an inverse':
\[ (d\Rightarrow a)\otimes d \to d\Rightarrow(a\otimes d) \]
But the types don't match up\dots

It looks more like a strengthening for presaturation or an equivalent property.

On the other hand though, the interesting filtered colimit is $d\Rightarrow f$. Hence $\hom(A,(d\Rightarrow f)\otimes d) \simeq (d\Rightarrow f)\otimes \hom(A,d)$ for small $A$. 

I am missing something here and therefore getting stuck.

Things seemed to be going so well.



\section{27/7/18}
Sidetracked by the idea of creating an extensional type theory based programming language.


The requirements thing is nice, but why not risk asking for too much?

First we set up a nice diagram to build a factorization system for. Second we show how diagram can be made nice. More niceness makes the prove easier, but makes it harder to get nice diagrams. However, we can take gradual steps to generalize.

I think I want to replace suitable with \emph{presaturated}


\paragraph{density still needed?}
Being closed under pushouts and composition seems enough. Perhaps we need small colimits, but even that is questionable.

I guess the argument used to be that closure under pushout grants density of codomains. I missed something important however that makes closure under pushouts much stronger.

Being closed under pushouts indirectly induces density of codomains.
Being closed under composition indirectly induces 

I feel a bit silly now. We have a class of morphisms in $\cat A$ that are isomorphic to $f\otimes c$ for some sheaf $f$. 

The properties for $c$ we propose is that any pushout $\alpha\of f\otimes c\to g$ is isomorphic to $\beta\otimes c\of f\otimes c \to h\otimes c$ for some $\beta\of f\to h$. Similarly, if $\cod(f\otimes c) \simeq \dom(g\otimes c)$, then there is a morphism $\alpha\of f\to h$ such that $\alpha\times A$ is an isomorphism and $\alpha\otimes B\simeq g\otimes c$ (note the $B$).

I imagine these are pretty straightforward thing to ask of the internal category\dots

We still need to make a diagram commute and filteredness may still be vital here.

\paragraph{confusion}
We had like three requirements, related to the stages of the completing:
density of $A$ to ensure the factorization system, 
filteredness of $I$ to ensure the colimit preservation,
closure under pushout and composition with the desired morphisms.

These come from peeking inside the internal category and proposing properties there.
I take the last property, try to formulate it as a property of the externalisation and the first two don't seem the matter anymore.
How is that possible!?


Perhaps the externalisation is a far stronger versions of the property than I realize.

That must be it.

\paragraph{baby steps}
Perhaps this is the lesson. Give every lemma a single responsibility. That may seem like a way to annoy, but is makes the work easier to digest.

\paragraph{presaturation diagrams}
We have arrived at a pleasant point.
The pushout property is the most powerful and probably requires some density and directedness.

But let's review.
Getting the composition property is probably an afterthought, once we have the pushouts. 

One thing that is not a afterthought: we need an index of domains and codomains in order to test which generic left morphisms fit together. We won't get one for free.

\paragraph{Good work}
I was in bad shape and the weather is hot. Let's be grateful for what we achieved today.

\section{13/7/18}
Where was I?


\paragraph{small completeness}

Specifics: we have a diagram $f\of X \to C_0$. We are interested in the sheaf of families $f\Rightarrow C_0$

The completeness we sought was a matter of compositional completeness.

We know $\dom$ is the terminal sheaf and $\cod$ the terminal diagram.
So $f\otimes g$ has morphisms to $\dom\otimes g \simeq \dom(g)$ and $f\otimes\cod \simeq \dom(f)$.

How do you tell your small universe has all small colimits?
There is a bundle of small coproducts for $u\of U\to V$
\[\function{ \tuplet{f\of V^u,x\of \dom(f),y\of f(x)} } f\of\bullet V^u\]
This should be generated, i.e. a pullback of $u$ along a morphism $\sigma\of V^u\to V$.

The category confuses the matter,
but the plan is essentially the same.

This part is all about guaranteeing 

Good work today.

\section{8/7/18}
The ascent construction is a left Kan extension, modified to work with internal diagrams instead of functors.

The classical case is simply this:
\[\xymatrix{
\simCat/[n] \ar[r]^\simplex\ar[dr]_{S} & \ambient/\simplex[n]\ar@{.>}[d] \\
& \ambient/\horn_k[n]
}\]
Does that mean the right adjoint is the right Kan extension?

We already know how to factorize.
\[\xymatrix{
\simCat/[n] \ar[r]^\simplex\ar[dr]_{K} & \ambient/\simplex[n]\ar@{.>}[d] \\
& \ambient/\simplex[n] \ar@<-1ex>[d]_{h\ri}\ar@{}[d]|\dashv\\
& \ambient/\horn_k[n] \ar@<-1ex>[u]_{h_*}
}\]
So now it becomes a matter of internalizing this\dots

\paragraph{extensional type theory}
I now have the means the introduce my own extensional type theory based on this 'polynomial type' idea. Given $f\of X\to Y$ there is a functor $Z\mapsto Z^f\of \ambient\to \ambient/Y$ right adjoint to the `forgetful pullback' $g \mapsto\set{\tuplet{x,y}|f(x)=g(y)} \of\ambient/Y\to \ambient$. Like the powerset, these types generate all of the right adjoints we associate with locally cartesian closed categories.

\section{2/7/18}
We don't need independent notions of smallness, but we do need a natural number object.

The \emph{small saturation} simply contains the finite initial steps of the saturation. Take sums, retracts, pushouts and compositions. In the latter case we overcome the potential difference in size between domains and codomain using extra pushouts.

Now we said we need small colimits and this remains true. What we need are finite limits and that is plenty.

\section{29/6/18}
Let's start with an outline:

\begin{itemize}
\item motivation
\item description of the construction
\item literary review
\item definitions
\item theorem
\item proof broke down in parts
\item examples
\end{itemize}


\paragraph{Garner}
Monad and comonad on the category of arrows.

I think my construction is the \emph{density comonad} for some $F\of \cat C \to \ambient/\ambient$, except that $F$ is an internal subcategory.
Two things should be difficult. Firstly, the density comonad exists.

Not so fast! The category of compact acyclic cofibrations is already a free completion, designed to make the rest of the construction easier.







Presumed differences:
\begin{itemize}
\item No completeness
\item Internalized \emph{everything}: family of cofibrations, lifting properties, filtered colimit arguments etc.
\item hence the difference should be in the way the monad is constructed, the rest is exactly the same.
\end{itemize}


\paragraph{Deeper understanding}
The construction I came up with is not so weird and is actually closely related to the constructions of Garner and Reihl. In fact Reihls enriched homopty theory is a great support. My biggest obstacle is completeness and I don't think either Garner or Reihl have a solution here.

So that is what my paper will be called:
'A small object argument for incomplete categories'

While the core of the argument is still the density comonad, the way it is constructed and the reason it works are changed.

Lets work this out:
We take an internalized version of $I\of \cat J\to\ambient/\ambient$. The family of cofibrations is re-imagined as a commutative square. Same goes for the bundle of small morphisms.

Eventually we have a saturated version $I'\of \cat J'\to\ambient/\ambient$ similarly internalized.

\paragraph{algebraic small objects}

Garner break things up in three steps:
\begin{itemize}
\item the codensity comonad
\item the lefthand construction with the pullbacks
\item the transfinite composition
\end{itemize}

The first two steps are already modified to work with internal constructions.
The point of divergence is that last one, however. Here I need to skip ahead to the result.
One we have the small saturation of the category of cofibrations, we only need 

If we start from an category rather than a family of morphisms, the small saturation is going to have more morphisms as well.
Here things stop making sense to me.

The small maps ought to be filtered themselves. In $\ambient/I$ the subcategory of small morphisms should be filtered. It is not necessary for small morphisms to be closed under composition.

Should the codomains be small as well? No, we need a family of potential codomains, but those could be 'small colimits' of whatever codomains the cofibrations actually have. I.e. let $I$ represent all generic cofibrations, then the domain of any small morphism to $I$ is fine.

The codensity stuff we win back by working with internal categories, or even families.

\paragraph{necessities}
Image we pick the first category at random, then what makes transfinite compositions unnecessary?
\begin{itemize}
\item have small domains.
\item being small-filtered.
\item being closed under compositions and pushouts. The pushouts require clarification!
\end{itemize}

No smallness conditions here. Well, the 'filtered' may say something.
Yes, because the colimit is not finite, we need the smallness here.

The smallness of the codomains is not necessary--we just need an object of all possible codomains to exist.

\paragraph{the generators}
A functor $I\of\cat J \to\ambient/\ambient$ corresponds to one $[1]\times I \to \ambient$. We replace this with a fibred category like thing.
Ultimately, we wind up with $C\to D \to I_0$ like we have been working with for a long time, together with an action of $I$ morphisms on both ends that the morphism then has to commute with.

\paragraph{What is holding me back now?}
I understand Garner's construction again and note that it both justifies what I did below, but also is more general by allowing categories of generic left morphisms instead of mere families. I don't know how to keep those around. I want to amend my construction 

Okay, remember how we now need cofibrations to be closed under tensors? The small saturation requires that `small tensors' also factor through morphisms in the saturation, but I think they do so automatically.

Small tensors may be the only extra requirement for filteredness.
The crucial thing really is that the is a single generic small morphism. In that case, we only have to worry about finite limits.

A second problem is the smallness of the codomains. It guarantees that the saturation exists as a small category, but technically 


\paragraph{colimit preservation}
This is an important idea: smallness is not random. The functor $\hom(S,\cdot)$ should preserve small-filtered colimits. The bigger the family of small objects, the smaller the number of preserved colimits. But this sounds like a requirement on small objects that we have not formulated properly yet.

Does it come for free?


First of, what is even a small filtered colimit?
Well, a small internal category is an internal category categories whose object of morphisms is small. A small-filtered category is presumably an internal category which has cocones for all internal functors with small domains. A functor from such a category into the ambient category is replaces by a kind of module and the colimit\dots probably is an obvious coequalizer.
\begin{align*}
&f\of X\to C_0\\
&\cdot\of \set{(\gamma\of C_1,x\of X)| f(x) = \dom(\gamma)}\to C_0\\
&C_0/(\gamma\cdot x \sim x)
\end{align*}
The point of smallness would be that $\hom(S,\cdot)$ preserves coequalizers of this shape internally.

So maybe we can simplify further by talking about 'small filtered coequalizers'. I.e. any small family of connected elements has a representative. Precisely, suppose $h\of Y\to Z$ is the coequalizer of $f,g\of X\to Y$. Small filteredness means that if $k\of A\to B$ is small and $(a,b)\of k\to h$, then there are $a'\of A\to X$ and $b'\of B\to Y$ such that $f\circ a' = a$, $g\circ a' = b'\circ k$. Or course $f$ and $g$ can be swapped for symmetry and perhaps even weaker conditions apply.
\[\xymatrix{
& X \ar@<-.5ex>[d]_f \ar@<.5ex>[d]^g \\
A \ar[r]^a \ar@{.>}[ur]^{a'}\ar[d]_k & Y\ar[d]^h \\
B \ar[r]_b \ar@{.>}[ur]_{b'} & Z
}\]
This is related to the arguments about internal filtered colimits that are supposed to be in the Elephant. I only need to know how to guarantee that the category of small objects is small filtered itself, if any requirement beyond cocones for \emph{finite} diagrams is needed.

I am thoroughly confused now. This whole filtered colimits thing made sense once, but now not so much. There must be something wrong with these filtered coequalizers, but I don't know what.

The colimit of the functor may be a coequalizer of a straight forwardly derived parallel pair, but that coequalizer is not what is preserved.
Yes! There is a single object where everything comes together, but in that object the elements are not necessarily the same.

Perhaps we should stick to internal categories of cocones instead of bothering with these coequalizers.

\paragraph{small filteredness of small objects}
Once we assume that there is a generic small morphism and that the small objects of all slice categories are filtered, can we assume that the full internal subcategory of small objects is small filtered?

I suppose the answer is that any small family of objects already provides the upper bound.

You know\dots maybe that does not matter.
\paragraph{the danger}
Given a morphism $f$ the category of small acyclics of $f$ has to be filtered. This is a different requirement than small object merely being small. In fact, we can probably argue now that because colimits exist, the small objects must be closed under them.

The issue is that small morphisms over any morphism must be a filtered category. So now we know: we don't have the liberty to let small objects merely be filtered. We need finite colimits and compositions.

Any cocone of small morphisms factors through the colimiting cone in a small morphism.

\paragraph{The other issue}
Yeah, the examples where one starts with a category rather than the small saturation.

I suppose the big unanswered question is: where is the small saturation supposed to come from anyway?

Close the generic morphisms under small tensors, pushouts, retracts and composition to get them all. At worst we need a natural number object to complete the set. Inside we only use finite compositions, is the idea.

The small saturation should contain all left morphism with small domains. Well maybe not all\dots just the ones that have a small set of generators.

Okay, but that was one approach: first generate the small fibrations and then construct the small cofibrations from them. There is a difficulty with that approach if the codomains are not small.

Still an approach where the saturation is the result of a finitary construction is more traditional and more flexible I guess.

\paragraph{Plan?}
I suppose I am ready to write an introduction which sketches the construction. While I write that, I can make a list of things that need to be worked out in the second half of the paper.

\section{1/6/18}

I think the horn inclusions are not the colimits of simpler acyclic cofibrations given the limited class of morphisms we allowed. No intersections.

So we go ahead and try to benefit from the fact that the colimit is filtered. So how do we manage that?

\paragraph{Filtered colimits and compactness}
For representable $x$, the functor $r(x) = \function y y^x$ would preserves all colimits. If $x$ is a finite colimit of representables, there is a colimiting cone we should  use.

The colimit for the whole object is a limit of colimits and a limit of colimits is the colimit of the limits of the limit is cofiltered.

Let $f$ be a functor $f\of \cat A\times \cat B\to\ambient$--actually, this should be an opfibration in out case. There is a canonical morphism:
\[ \colim_x \lim_y f(x,y) \to \lim_y \colim_x f(x,y) \]
Let $\phi\of\lim_y \colim_x f(x,y)$. For each $y$, $\phi(y)$ is an equivalence class that intersects $f(x_y,y)$ for certain $x_y$. For each choice of $y\mapsto x_y$, however, there is a cocone, which provides the unique member of $\colim_x \lim_y f(x,y)$ that the canonical morphisms sends to $\phi$.

\paragraph{Idea}
Let $s\of S_0\to S_1$ be the generic family of small objects. We only demand that it is closed under finite colimits. We can now define the internal category of small acyclic cofibrations $\cat H$, with the morphisms restricted to the kind of commutative squares show below. This category is not not just filtered, it is closed under finite colimits itself.

Any morphism $f$ factors as $f_1\circ f_0$ where $f_0 = \colim_{h\to f} h$. Of course, every small acyclic cofibration factors through $f_0$. For each $h\to f_1$, the fact that $\cat H$ is filtered gives a construction from below, showing that $f$ indeed has a lifting property. This construction is so generic that we can use it for both horns and cycles, yielding the factorization systems we always dreamed of.

\section{23/5/18}
To get a filtered category of commutative squares $h\to f$ where $h$ is a compact acyclic cofibration, only allow $(a,b)\of h\to h'$ where the factorization of $b$ through the pushout of $a$ is an acyclic cofibration.
\[\xymatrix{
\bullet \ar[r]^h\ar[d]_a\pushout & \bullet\ar[d]\ar[dr]^b \\
\bullet \ar[r]\ar@/_/[rr]_{h'} & \bullet \ar[r]^(.4){b/a} & \bullet
}\]

Claim: the pushout of two such morphism exists within the category.
\[\xymatrix{
&& \bullet \ar[r]^a\ar[ddr]^(.4)f\ar[d]^(.7)e & \bullet\ar[r]^b & \bullet \ar[ddr]^h \ar[d]_g\\
\bullet\ar[r]_i\ar[urr]^c\ar[ddr]_{c'} &\bullet\ar[urr]^(.4)d\ar[ddr]_(.3){d'} &
\bullet\ar[rr]^j && \bullet\\
&&&\bullet\ar[rr]_m\ar@{.>}[ul]^k &&\bullet\ar@{.>}[ul]^l \\
& \bullet \ar[r]_{a'}\ar[urr]^(.6){f'}\ar[uur]_(.7){e'} & \bullet\ar[r]_{b'} & \bullet \ar[urr]_{h'}\ar[uur]^(.7){g'}
}\]
The big square $f\circ c = f'\circ c'$ is a pushout and $k$ is the factorization of the $e$-$e'$-cone through it. Since $m$ should simultaneously be a pushout of $b\circ a$ along $f$ and $b'\circ a'$ along $f'$, but perhaps those don't coinside. In that case let $h$, $h'$ and $w$ be the colimit of the $W$-shaped diagram involving $b\circ a$, $f$, $b'\circ a'$ and $f'$. The $j\circ k$-$g$-$g$-cone commutes and therefore factors as well, inducing $l$. 

Difficulty remains in showing that $k$ and $l$ are a morphism and $m$ is an acyclic cofibration. This might have been easier with coequalizer.

\paragraph{Thoughts}
It is hard to tell how important precisely these morphisms are, after all, would this not work for a greater class of morphism? The trouble is staying within acyclic cofibrations.

On the other hand, we see to have a unique filler for all filling problems, which seems so much nicer than the transfinite compositions produce.

At least it all looks possible now.

\section{20/5/18}
An important idea in the proof of yesterday is that $f_0$ should be a filtered colimit of compact (connected) acyclic cofibrations. We cannot make that happen with mere pushouts, but there is hope for transfinite compositions.

Usually a good approximation of an object in terms of other objects is to take the a colimit, so we want to do this here too: $f_0 = \colim_{h\to f}h$.

The idea is to use the extra compositions to add the joins required for the directed colimit.

The simplest idea is to add copies of each cofibration for each $n\of \nno$, but to require that $i < j$ is a morphism is not a decidable monic. The difficult joins get lifted on a higher limit. That might not work because the result is not a directed category. 

Even if the coequalizers were present, a coequalizer of a parallel pair of morphism between acyclic cofibrations, might not be an acyclic cofibration, precisely because the identification of equivalent point introduces cycles. I imagine the easy way out is to fill in this cycles, but how do we catch them and what do we fill them with?

I don't believe I actually have a solution for this anymore.

\paragraph{Would this help?}
We need cocones in the category of commutative squares $h\to f$ where $h$ is an acyclic cofibration. Coproducts are easy, but what about the cofibrations?

\[\xymatrix{
A\parr\ar[d]_h & A'\ar[r]\ar[d]_{h'} & X\ar[d]^f\\
B\parr & B'\ar[r] & Y
}\]

If we first fill the rightmost square, a free filler won't factor through the coequalizer of the pair $B\rightrightarrows B'$. Fill the outer square first to get a commuting morphism $B\to X$ and derive a new diagram:

\[\xymatrix{
& A+A \ar[r]^{h+h}\ar[d]\pushout & B+B\ar[d] \\
A\parr\ar[d]_h & A' \ar[r]\ar[d]_{h'}\pushout & \bullet \ar[r]\ar[d] & X\ar[d]^f\\
B\parr & B' \ar[r] & \bullet \ar[r] & Y
}\]

If we now fill the rightmost diagram, I imagine a filler for the coequalizer could be fashioned from it. Maybe not: only the $A+A$ range of $B'$ is forced to adhere to a pre-specified lifting. Worse still, there may be not better way, because the morphism $B\rightrightarrows B'$ could overlap, conflicting in its prescriptions for $B$.

It seems probable that this all has been tried before and then forgotten because it just wouldn't work. 

It look like the category of compact acyclic cofibrations of $f$ is not directed. While colimits exist among more general compact morphisms, a cocone with an acyclic cofibration is missing. 


\section{19/5/18}

\paragraph{the other small object argument}
Instead of bothering with transfinite compositions, we start with a larger family of (acyclic) cofibrations. Let's work this out in the external case first.

Instead of just considering horns, consider all acyclic cofibrations between simplicial which are finite colimits of representables. Let $\set{h_i\of A_i \to B_i |i\of I}$ be this family.

Let $f\of X\to Y$ be any morphism of simplicial objects. We factorize as follows. First let $h_f\of A_f\to B_f = \sum_{ i\of I, h_i\to f } h_i$--this is a sum of morphisms between the appropriate sum of domains. There is a canonical morphism $h_f\to f$ (actually a commutative square) which we factorize using a pushout.
\[\xymatrix{
A_f\ar[r]^{h_f}\ar[d]_{a_f}\pushout & B_f\ar[d]\ar[dr]^{b_f} \\
X \ar[r]^{f_0}\ar@/_/[rr]_f & Z \ar[r]^{f_1} & Y
}\]
Now $f_1$ is supposed to be a fibration.

The core of the argument is that $f_0$ is a filtered colimit of acyclic cofibrations which are colimits of representables and that $\ambient(A_i,-)$ preserve those. Given $(c\of A_i\to Z,d\of B_i\to Y)\of h_i\to f_1$, $c$ factors through some $B_j\to Z$ and the pushout of $h_i$ along this factorization gets us a new member $h_k$ of the family of `compact' acyclic cofibrations.
\[ \xymatrix{
 & A_j\ar@/_/[dd]_(.25){h_k}\ar[d]^{h_j} \ar[r] & X\ar[d]_{f_0} \ar@/^/[dd]^f\\
A_i \ar[d]_{h_i} \ar[r]_{c'} \ar@/^/[rr]^(.25)c \pushout & B_j \ar[r]\ar[d] &Z\ar[d]_{f_1}\\
B_i \ar[r]\ar@/_/[rr]_{d} & B_k\ar[r]\ar@{.>}[ur]^e & Y
}\]
The filler $e$ comes from the fact that $h_k\to f$ factors through $(a_f,b_f)\of h_f\to f$.

To make this work constructively we either need all choices of $B_j$ to result in the same filler, or there must be a canonical choice\dots or both. I think it will be a bit of both: enumerate the family of $h_j$ and use partial sums, but all available choices of morphism $h_j\to f$ must work out.

To complete the proof, we need to show that $f_0$ is a filtered colimit. The morphism $a_f\to A_f\to X$ is a regular epimorphism, because for each $x\of\base(X)$ the identity map $\simplex[\dim(x)]\to\simplex[\dim(x)]$ is a `compact' acyclic cofibration, hence a term of $h_f$.

Pushouts preserve regular epimorphisms. I remember struggling with this, so let's work out the diagram:
\[\xymatrix{
\bullet \ar@/^/[r]\ar@/_/[r]\ar@{}[r]|\varnothing & \bullet \ar[r]\ar[d]\pushout & \bullet \ar[r]\ar[d] & \bullet \\
& \bullet \ar[r]\ar@{.>}[urr] & \bullet \ar@{.>}[ur]
}\]

This makes $f_0$ the coequalizer of an exact fork and the idea is to get a filtered diagram by taking pushouts of pullbacks for finite sets of $h_i$. In order to get the result to be a colimit, we need to coequalize stuff, but coequalizers of acyclic cofibration can be cyclic. This is what my problems have revolved around all the time.

Okay, it turns out there are big problems left to solve here.
The coequalizing members can add additional simplices to the original structure, thus filling in any accidental cycles.

Generally taking the coequilizers for the codomains is fine. coequalizer of the domain may have cycles we need to fill in. While we have a filler for the joined cofibration, it is not going to commute\dots

\paragraph{The point of a transfinite composition}
A pushout does not allow us to build on the faces we already have, which is why it cannot. A better strategy is to use a transfinite composition that doubles as a filtered colimit somehow.

I am unsure how exactly to reconcile the two.

From the desire for directed limits is seems lie we should work with chains of morphisms between acyclic cofibrations:
\[\xymatrix{
A_0 \ar[r]^{a_0}\ar[d]_{h_0} & \cdots\ar[r]^{a_{n-1}} & A_n\ar[d]^{h_n} \\
B_0 \ar[r]_{b_0} & \cdots \ar[r]_{b_{n-1}} & B_n 
}\]
Here all $b_i$ would be regular epimorphisms and $B_n$ would be connected. Each stage add missing equalizers for the one before it that is the point.

For the construction in the core of the proof, simple chains of acyclic cofibrations make sense.

In either case, the question is: what are the morphisms?



\section{18/5/18}

\paragraph{Cofibrant generation}
Everything I wrote is based on the internalized version of the notion of a small family of generic cofibrations. However, I got greedy and tried to make the lifting property with regard to each member of the family a special case of the lifting property for a single morphism. I am unsure of this works anymore and it certainly doesn't make the descent theorem harder to prove.

General ideas:
\begin{itemize}
\item the whole paper is based on an internalized version of \emph{cofibrant generation}
\item this notion of cofibrant generation hides a more \emph{natural characterization of (acyclic) cofibrations} in terms of decidability properties. For acyclic I haven't determined what this property is however.
\item nor have I found a replacement for the \emph{small object argument} that permits fibrant replacements.
\item the definition of the lifting property for families isn't correct and requires an update throughout the paper.
\end{itemize}


\paragraph{small object argument}

For a morphism of simplices $f\of A \to B$, start with the monic
$\function{a}\tuplet{0,a,f(a)}$ of $\base(A)\to \nno\times\base(A)\times \base(B)$ and the epic $\function{\tuplet{n,a,b}}b$. I want to modify $\nno\times\base(A)\times \base(B)$, first select elements and then take a quotient.

Suppose $f = g\to h$ is the result of a small object like construction. The filler could work as follows. Every $x\of\base(\dom(g))$ is an equivalence class of tuples $\tuplet{n,b,a}$, where $n$ is the `birth date' of the, $b$ is the image of $g$ and $a$ is some bookkeeping we need to do. For each horn and each selection of tuplets, there is a least birth date that does not occur and for this birth date $n$ there is a tuplet $\tuplet{n,b,a}$ whose equivalence class in $\dom(g)$ serves as the filler for the fragments.

The extra bookkeeping is unavoidable however.

Each horn filler introduces a simplex that intersects the horn in a cycle: the base of the horn. We need to keep track of this one.

The generations could actually be about extra dimensions needed to get the acyclic inclusion back to $A$. I.e. $\tuplet{b,a}$ contains a bigger simplex $b$ of $B$ and a monic of $\simCat$ to indicate that the new face was introduced over that bigger face. This introduces new problems because $B$ does not have to be a fibrant object.

We might need to keep a collection of elements of the codomain $B$ that together act as a kind of cover. The members represent simplices that need to be filled before the current one can, all the way back to simplices that directly derive from members of $A$.     

Constructions are known, but we need to kip ahead of the line to the end result in order to get what we need. 

The members of $C=\dom(g)$ combine $b\of \base(B)$ with $k\of[\dim(b)]$ to indicate how $b$ was filled in,
but also $[\dim(b)]\to \base(C)$ to point to the other simplices and we are still missing the restriction maps here.

We are looking for a free filler algebra. We don't have a clear path to its construction, with may just go beyond what is available here.

\paragraph{lisp}
Take the horns and the restriction maps and turn them into operators in an operads like structure\dots There is some kind of multicategory in this somewhere. 

The generic operators are $\xi\of\Ar(\simCat)$ and $\set{ h_j[i] | j\leq i\of\nno }$. The types that determine valid compositions are the dimension of the simplices involved\dots almost.

The product in $h_j[i]\of [i-1]\times[i-1]\to [i]$ hides the overlap of the simplices the operator is supposed to combine.

The product is a higher order operator that introduces new morphisms 

So what about finite colimits as objects?

We can indeed build a family of (acyclic) cofibration between finite colimits of simplicial objects--a set that is recursive and probably decidable, if in a highly non trivial way. The lifting property with respect to this family implies the lifting property with respect to 

The internal subcategory of small objects and fillers given for all cofibrations in those categories. The advantage seems clear however.

I am afraid things are still not that simple, because of the restriction maps. Actually the problem is that the product is still overly complicated.

I think I found a way in:

\[ \xymatrix{
& X\ar[r]|f & Y\\
%
\sum_{i<n} \simplex[n-1] \ar[r]\ar[d]\pushout & 
\horn_k[n] \ar[u]|a\ar[d]\ar[r] & 
\simplex[n] \ar[dd]\ar[u]|b \\
%
\sum_{i<n} C_i \ar@/^{3ex}/[uur]|c \ar[r]\ar[d]\pushout & 
\bullet \ar@/^{3ex}/[uu]|(.7){c'} \ar[d]|p\pushout \\
%
\sum_{i<n} D_i \ar@/_{3ex}/[uuurr]|(.6)d \ar[r] & 
\bullet \ar[r]|q & \bullet \ar@/_{3ex}/[uuu]|{d'} \ar@/_{3ex}/[uuul]|{e} 
}\]

The idea is that the commuting $c\of \sum_{i<n} C_i\to X$ and $d\of \sum_{i<n} D_i\to Y$ are implied by $a$ and $b$. Pushouts then induce the maps $c'$ and $d'$, forming a new commutative square with $q\circ p$, which is a cofibration of finite colimits of simplicial sets. Hence the filler $e$ exists.

Now this would be the complex product of types envisioned above.

\paragraph{New way}
By skipping ahead to the end result this way, we can actually perform the small object argument in order to produce a full factorization system. We might be getting close to Garner. No, distinctly no because we have a category of small objects closed under small colimits, which in our case means \emph{finite}.

We are also stuck with a rather awkward notion of `generated'. 

If this works as advertised, it could replace much of the paper.

\paragraph{review of the small object argument}
The category is assumed to have all small colimits and small homsets. The smallness and the domains of the generic cofibrations is small. 

The assumptions look absurdly broad for actual horn inclusions and cycles. I want to do the opposite. Have an internal category of small objects for my construction. Then freely generate the filler algebra.

Since all the objects are finite colimits, we don't even need to stick to the format of the proof above that badly. It becomes a matter of carefully putting together the various colimits. The covering by a small sum of representables gets us where we need to be.

\paragraph{summary of the finite simplicial set approach}
With the small object argument, we have to repeat the pushout until we get a transfinite composition up to a sufficiently high cardinal. I want to be done at once, so I get a larger family of cofibrations to take the pushout over.

Basically, I assume that pulling back an acyclic cofibration along morphism with specific domains preserves acyclic cofibration.

No that isn't it--I know the structure of the pushout. I know what each simplex there looks like and use that information. Being covered by a small family of \emph{representables} is important, as well as accounting for all origins of representable objects.

There is an important parallel though--the new family of cofibrations is not small, let alone the object of lifting problems, but the codomains of individual members are. This has an impact on the pushout, I struggle to pin down now. 

\[\xymatrix{
\bullet \ar[d]\ar[r]^{\sum h} & \bullet\ar[d]\\
X\ar[dr]_f\ar[r]& Z \ar[d] & \bullet \ar[l]\ar[d]^{h'}\\
& Y& \bullet \ar[l]
}\]

Its something like: take $\dom(\sum_{h\of P} h)\times_Z\dom(h')$. The functor $(\cdot)\times_Z\dom(h')$ preserves finitely filtered colimits, due to the finiteness of $\dom(h')$. This is what we get a finite family of colimits covering this specific one.

I am unsure that I have the key now. 

\paragraph{again}
Here:
\[\xymatrix{
\bullet \ar[d]\ar[r]^{\sum h} & \bullet\ar[d]\\
X\ar[dr]_f\ar[r]& Z \ar[d] & \bullet \ar[l]\ar[d]^{h'}\\
& Y& \bullet \ar[l]
}\]

The argument is that there is a finite family $H$ of representables covering $\dom(h')$. For each of those representables, we can find a lifting problem that introduced it into the pushout. Said otherwise, a finite 

I see what I did wrong. The representables don't grant maps into codomains. Now the covering gets in the way of combining the other lifting problems.

I should just have started the update of the paper.

\paragraph{Category of transfinite compositions}
Still try to capture \emph{fibrancy} in an algebra.

Finite simplicial object represent the types of the domains of the operators well. If we stick with full simplices for codomains, we get a simpler setup.
 
Get rid of the pushout, it is to dangerous.

The 'operators' are acyclic cofibrations $A \to \simplex[n]$ combined with maps $[m]\to [n]$, which cannot be members of $A$. 

'operators'. So how do we apply them? The lifting problems are the answer. 

Here I may be seeing something I missed before.
Suppose $a\of I\to J$ is one of the small cofibrations. Each face $j\of\base(J)-\base(I)$ is an 'operator'.
I suppose there is an equivalence, along the lines of $a'\of I'\to J'$ being a sub-acyclic cofibration, contain the same operator.

We are back with describing the product in a sensible way. 

That was the whole problem from the start. There may not be a simple join because any straightforward method introduces cycles.

The `operators' are faces of codomains of acyclic cofibrations. The missing data is a way to select `operators` for each.


\paragraph{alternative characterizations}
Horn fillers introduce two new simplices, the whole filler and its base. So perhaps acyclics can be characterized by a decidable subdivision of the new faces. Seems like a stretch though.

Not helpful.

\paragraph{conclusion}
I prefer puzzling over writing so much that I rarely get to writing. Hmm\dots


\section{4/5/18}

The ascent functor $A\of \ambient\s/\simplex_P \to \ambient\s/\horn_P$ how does it work? For representables $r\of \simplex[n]\to \simplex_P$ it is sort of clear what $A(r)\of R(\simplex[n])\to\horn_P$ looks like. First fortify $r$, then take the pullback.

For $g\of Y\to \simplex_P$, construct $A(g)$ in two steps. First, each $y\of\base(Y)$ corresponds to a representable $\simplex[\dim(y)]\to \simplex_P$. First sum over all $R(\simplex[\dim(y)])$, then take a quotient that glues simplices to their restrictions.


Put simply, $g(y) = \tuplet{p,\xi}$, where $p\of P$ and $\xi\of[m]\to[n]$. 

\paragraph{simplifications}
The main trick in all of this, is replacing external coproducts with indexed coproducts over discrete families.

Perhaps this allows us to represent the lifting operator in a simpler way. For each $f\of X\to Y$ in $\ambient\s$, there is a family of lifting problems $p\of P\to \set\geq$. The members of $P$ are commutative squares $h\to f$, where $h$ is a horn inclusion and $p$ tells us which, by specifying dimension and top edge. This means there is a universal lifting problem, whose solutions are lifting operators.
 
Note: we are dealing with a parallel lifting problem. The operator has to be a morphism in $\ambient\s/P\disc$, or in a transposed set up over $\ambient\s/\set\geq\disc$, or it doesn't work.

The following diagram in $\ambient\s/\set\geq\disc$ would work:
\[\xymatrix{
\horn_{\set\geq}\ar[d]\ar[r] & X^P_{\set\geq}\ar[d]^{f^P_{\set\geq}}\\
\simplex_{\set\geq}\ar[r]\ar@{.>}[ur] & Y^P_{\set\geq}
}\]
Each problem $p\of P$ contain a map $a\of\horn_j[i]\to X$ and a map $b\of\simplex[i]\to Y$ such that $b\circ h = f\circ a$ and these maps induce the commutative square above. This is the universal lifting problem for $f$. Its solutions are realizers of $f$'s fibrancy.

This is great news. We only need descent along the family of horns, without worrying about larger set of problems.

\paragraph{discrete pullback lemma}
A discrete morphism in $\ambient\s$ in our case is a pullback of a morphism from $\ambient$. If cofibrations and acyclic cofibration are closed under pullbacks form those, we don't even have to bother with slice categories over discrete objects. Just having a lifting operator for the 'family' is enough.

This lemma must be equivalent to something in the definition of the factorization system--something that sets it apart from the normal factorization systems. A lemma about enriched factorization systems in other words.

The category $\ambient\s$ is enriched over $\ambient$ and also has ambient embedded. Any enriched factorization system should therefore allow us to pull back its left morphisms along pullbacks of morphisms in $\ambient$, even if left morphism aren't generally closed under pullbacks. It this true though? It comes down to this: if we have a lifting operator for a coproduct of cofibrations, can we constructively split it up into lifting operators for individual cofibrations? No, because not every individual lifting problem extends to a lifting problem for the entire family. This won't fly.

I have done this before and concluded that it wouldn't work. The universal lifting problem has to exist in a slice over a discrete object, otherwise it just won't work. However, we can restrict our attention to $\ambient\s/\set\geq\disc$ thanks to adjunctions.


\paragraph{mistake?}
Perhaps the lifting property in the start of this paper is too weak. It might work out if we consider the enrichment over $\ambient/P$ rather than over $\ambient$. Very tiresome.

The object of lifting problems is just rather different,
being a sum over the possible horns rather than a product.

Once we have that, does a version of the discrete pullback lemma become acceptable?

In any case, my presentation is not clear enough and too hard to remember.

\paragraph{empty space}
At this point is really seems like a mistake that an empty $[-1]$ simplex does not exists. Would initial object for $\simCat$ change that much?

Every simplex would have an extra object $X[-1]\of\ambient$ and $!\of [-1] \to [n]$, would grant a new morphism $X[n]\to X[-1]$. The result could effectively be a family of simplicial sets and might accidentally solve a lot of problems for us.

There could be a model structure on families of simplicial sets.
There would be an advantage if this somehow reduced the indexed coproducts we need to simpler constructions.

The extension problem remains.


\paragraph{Back to the functor}
Not to knock the insights of this morning. We can now solve the problem of descent along the family of horn inclusions and know that things work out\dots or can we?

We got a lot of leverage out of the descended morphism simply being a modest fibration. The transposition throws a curve ball here. That is why we need to prove descent for all indexed sums of horns.

%
Let $g\of Y\to \simplex_P$. What is $A(g)\to A(Y)\to \horn_P$?
$\simplex_P$ consists of a problem $p$ which has some parameters, like the dimension of the horn to be lifted and a simplex $\xi\of[m]\to [n]$ that is part of its codomain and $k$ the top edge of the horn. 
First approximation $\sum_{y\of\base(Y)} \mathbf{nds}[\dim(g(y))]\times\mathbf{nds}(\prod_{l\neq k} \xi_l)$--barring the cases where both sequences are empty. Also, limit to cases $\tuplet{y,\alpha,\beta}$ where $g(y\cdot\alpha)\of\horn_P$.

Generate an equivalence relation from:
\[\tuplet{y\cdot\phi,\alpha,\beta}\sim \tuplet{y,\phi\circ \alpha,\phi\circ \beta}\]
The quotient is $\base(A(Y))$.

The rest is going to be more painful. 
\begin{align*}
\dim\tuplet{y,\alpha,\beta} &= \#\alpha+\#\beta-1\\
A(g)\tuplet{y,\alpha,\beta} &= \tuplet{p,\xi'}\\
\tuplet{y,\alpha,\beta}\cdot\phi &= \tuplet{y,\alpha\cdot\phi_0,\beta\cdot\phi_1}
\end{align*}

If $g(y) = \tuplet{p,\xi}$, then $A(g)\tuplet{y,\alpha,\beta} = \tuplet{p,\xi'}$ with $\xi'$ is $\xi\circ\alpha$ extended with $\#\beta$ copies of $k$. 
Similarly, $\tuplet{y,\alpha,\beta}\cdot\phi = \tuplet{y,\alpha\cdot\phi_0,\beta\cdot\phi_1}$ relies on cutting a part $\phi_1$ form the middle of $\phi$.

We can represent non-decreasing $\xi\of[m]\to [n]$ as morphisms $[n]\to \nno$ by counting the number of elements in their sections. The morphism in the slice category $\simCat/[n]$ similarly become families of morphisms.

Idea: $\alpha\of[a]\to[n]$ and $\beta\of[b]\to[n]$ therefore have a `join' $\alpha\sqcup\beta\of[a + b + 1]\to[n]$. The lack of empty elements makes it harder to maintain.

There are two morphisms $a\of [\#\alpha - 1]\to[\#\alpha + \#\beta - 1]$ and $b\of[\#\beta - 1]\to[\#\alpha + \#\beta - 1]$ fixed for each $\tuplet{y,\alpha,\beta}$, which are surjective together. For each $\phi\of [i] \to [\#\alpha + \#\beta - 1]$, $\phi_0$ is the pullback of $\phi$ along $a$ and $\phi_1$ is the pullback of $\phi$ along $b$. $A(g)\tuplet{y,\alpha,\beta} = \tuplet{p,\xi'}$, where $\xi'$ is completely define by $\xi'\circ a = \alpha$ and $\xi'\circ b = \function{x}k$. The division depends on the morphism part of $g(y)$, $\#\alpha$ and $\#\beta$.

We need to keep track of these two morphisms, to help out the the future.

The only thing left to define is what $A$ does to morphisms, but that should be obvious.
\[ A(m)\tuplet{y,\alpha,\beta}\sim \tuplet{m(y),\alpha,\beta} \]

A lot of particles are mentioned, but not properly named. Make sure that they are.

\paragraph{Ascents}
I take the descent of a single fibration as an example of gluing, but that actually solves the wrong problem.

Actually, the modest fibration $f\of X \to \horn_?$ is a gluing problem and for each gluing problem, we need a separate descend. We similarly need a separate ascend left adjoint, for each problem.

We are dealing with a $P$ indexed set of fibrations, each of which needs its own descend.

The construction I had in mind, might be off, due to a confusion between dependent products and coproducts. The construction works on a by-element basis, but one of the challenges is to prove that the infinite family of elements adds up to a single filler operator.

So a problem consists of a single horn $\horn_j[i]\to V$ that needs a filler. Since there is a family of horns, the object of lifting problems exists $P = \sum_{j\leq i\of\nno}\ambient\s(\horn_j[i], V)$. 

The category $\ambient\s/P\disc$ contains a horn inclusion $\horn_P\to\simplex_P$, by reindexing from $\ambient\s/\set\geq\disc$ and the universal modest morphism by reindexing from ambient.

Think of $\ambient\s$ as a simplicial object up to isomorphism, its $n$-simplices given by fibrations $f\of X\to \simplex[n]$. The by element decent lemma tells us that the whole category is fibrant, in the external sense. We need this to be true in the internal sense as well, there should be a lifting operator.

\paragraph{another route}
Write a paper about this construction in the category of simplicial sets, perhaps without the axiom of choice, or other powerful assumptions.

We could probably go further and show the same principle applies to many categories of simplicial object.

The problem is and always was to get the actual operator.

\paragraph{parametric}
I really have a hard time telling the difference between a descend for a fibration and a family of descents for a family of fibrations.

It also seems like giving a family of all objects is responsible f

The `category is fibrant' has a better route: show that descend works along arbitrary acyclic cofibrations. That is the inevitable consequence.

Weakly invertible cofibrations. It is not that simple, because $\horn$ is not fibrant. These crutches do not exist for all acyclic cofibrations. However, the weak inverse makes descent trivial.


\paragraph{Big challenges seem smaller?}
Collect all acyclic cofibrations with simplices as codomain.
I guess that collecting the cofibrations is easy, but that filtering the ones with cycles out is hard, though not impossible. Perhaps simply checking all the cycles and checking that they are filled is enough.

Let $F(X)$ consist of tuples $\tuplet{a,x,\xi}$ where $a\of A\to\simplex[n]$ is an acyclic cofibration, $x\of A\to X$ is an arbitrary morphism and $\xi\of [m]\to [n]$ is a monomorphism.
Perhaps we need to work with quotients, or with families of such, but this is my candidate factorization.

The inclusion of $X$ should be the trivial example. Showing that the result is an acyclic cofibration should rely on the whole thing being a pushout (hence the quotient) of cofibrations.

Why is it a fibration though?
I guess the gluing is almost just as obvious. Idea: the quotient means we have to deal with many possible representations of the component simplicial objects. Moreover, gluing together acyclic cofibrations may actually be quite hard, as simply uniting them could introduce unwanted cycles. Still, if a suitable combination can be found in each case, which respects the equivalence, there is a lifting operator as desired.

\paragraph{conclusion}
This was not a very productive day. Maybe I should just give up on this project. Or ask for help. I have to think about it.

\section{20/4/18}
Over the weeks I have been thinking about the simplified construction,
and along the way, lost confidence again.

A morphism $f\of X\to \simplex$ \emph{ascents} along $\horn\to\simplex$ by gluing simplices from $x\of X$ over $\horn$ with supporting structures over the tip of $\horn$, which doesn't really depend on $f$. What to glue where?

A first approach makes $\base(A(f))$ consist of pairs $\tuplet{x,y}$ where $x\of X$ and $y\of\mathrm{nds}(\prod_{l\neq k}\xi_l)$. But $f(x) = \xi$ is not enough, since the must be an action of $\simCat$.

Perhaps $\tuplet{x,\phi,y}$ where $f(x) = \xi\cdot \phi$. This solves the action problem. Don't we get too many simplices that way?
Revenge of the equivalence:
\[ \tuplet{x,\phi,y}\sim \tuplet{x,\chi\circ\phi,\chi\circ y} \]
Note that this only works if $\xi = \xi'\circ \chi$. Random $\chi$ can leave you with tuples where $\xi\circ \phi\neq f(x)$. We should name the function that maps $y$ to $\xi$. The limitation clearly is crucial.

\paragraph{More bounds}
Return to the idea that $f(x) = \mathrm{supp}(y)$. We have no proper action on the left hand side, but we can start with the free action. Use the equivalence relations to reduce the equivalence classes:
$\tuplet{x,\chi \circ y,\chi\circ\phi}\simeq \tuplet{x\cdot \chi,y,\phi}$
This is starting to look like something.

It works like this now: $\tuplet{x,y,\zeta}\sim \tuplet{x\cdot\zeta,y',\id}$ if $y = \zeta\circ y'$.

Confusing stuff and it only gets worse. The action of $\simCat$ is supposed to be distributed among $x$ and $y$. $\dim\tuplet{x,y,\zeta} = \dom(\zeta) + \#(y)$ and so $\tuplet{x,y,\zeta}\circ\phi$ is going to be $\tuplet{x,y\circ \phi_0,\zeta\circ\phi_1}$, etc.

The distribution is actually still here together with the tensor product. Reason to trust this was the right approach all along.

\paragraph{the story now}
For a long time, I saw no way to construct the left adjoint.
I realize it is possible and try to improve my prove of descend with it. I was stuck on distribution for a while, considered replacing them
with a product with a more independent construction, but now I think a direct description of the ascend functor is better.

`Ascend' is a good find.

The mechanism of the distribution and the adjoint pair of functor it induces is still there. We have to watch out not to introduce a right actions of $\simCat$, because that does not exist.

We now focus on the left adjoint first, however and show how it preserves acyclic cofibrations. The right adjoint now naturally preserves fibrations. Secondly, because ascent after direct image is identity, inverse image after descent is identity as well, thanks to adjointness and Yoneda lemma's. Existence and preservation of modesty follows follows quite directly from assumptions.

\paragraph{writers block} Besides the technical complexity, I also struggle just to structure all the information I need to present.


We don't need general distributions, they are just a construction I use.

\paragraph{another sketch}
Let $S$ in $\ambient$ consist of tuples $\tuplet{\xi,k,y,\phi}$ where 
$\xi\of\base(\horn_{\leq})$, 
$k\of \cod(\xi)$, 
$y$ is a nondecreasing sequence of elements in the poset $\prod_{l\neq \top(p)} \xi_l$ where $\xi_l = \set{i \of [\dim(p)] | \xi(i) = l }$, 
$\phi\of\Ar(\simCat)$ such that $\dom(\xi) = \cod(\phi)$.

We can not even define a right action, because $\xi$ is in the way.
The $\xi$'s are standing in the way now.

I am getting frustrated again. As soon s I try to sketch the proof, I lose track of the structure and don't understand what I am doing anymore.

\paragraph{more integral}
So we have $g\of Y\to\simplex$. Ascent does two things. It adds simplices and takes the pullback. Could the extra simplices come form $g$ itself? Specifically, $\simplex{x,y}$ where $g(y)\not\of\base_{\horn}$? Note that both sides would need to admit elements where the other remains empty, but otherwise the simplices in the ascended version connect included and excluded elements.

This looks like a strange way of folding the structure.

I have trouble believing the structures are even related\dots

Okay, applying restrictions to $y$ can lead outside of the complement.

$S$ could be pairs $\tuplet{\alpha,\beta}$ where $\alpha\of\base(\horn)$ and $\beta \of \base(\simplex)-\base(\horn)$. The idea being that the tensor product would essentially create the pairs above.
It still doesn't work though, since the compliment is not a simplicial set.

This is not as specific as before. There is a particular $\delta_k\of[n-1]\to[n]$ and $y$ is supposed to come from its fibre.

That is a way of looking at it.
The $\xi$ is confusing me now, so I try to get rid of it. This could be a way, but for now it only seems more troubling.

Starting with $g\of Y\to \simplex$ and $y\of Y$, we know that $y$ are only preserved if $g(y)\of\base(\horn)$. To preserve the structure, we want to smear $y$ it out, like a convolution.

I am completely lost right now. Trying to fashion the support out of $Y$ itself only confuses me more.

\paragraph{Now what}
The right action is something much more subtle now.
If $f(x) = y\cdot \phi$ then $\phi\circ x$ exists and $f(x\circ \phi) = y$. Now the tensor makes sense to.

So $S$ consists of tuples $\tuplet{\xi,k,y,\phi}$ as described. There are a number of projections. In one direction we go $\xi\circ \phi + \dim(y)$, in order to get to $\horn$ and this is supposed to work out as a morphism of simplices to $\horn$. The other is more straightforward: to $\xi$, where the rule $\xi = \xi'\circ \chi$ then $\tuplet{\xi,k,y,\phi}\simeq \tuplet{\xi',k,\chi\circ y,\chi\circ \phi}$ almost starts making sense, except that we cannot glue anymore. Instead
$\chi\cdot\tuplet{\xi,k,y,\phi} = \tuplet{\xi',k,\chi\circ y,\chi\circ \phi}$
Here I spot trouble: what if $\xi'\circ\alpha = \xi''\circ \alpha$?
That makes $\alpha\cdot$ ambiguous.

While there must be a functor in there, it is hiding itself really well.

So what? $\tuplet{x,k,y,\phi}$ where $y$ is a nondecreasing sequence in $\prod_{l\neq k} g(x)_l$ is better? Now we let $\tuplet{x\cdot \chi,y,\phi}\sim\tuplet{x,\chi\circ y,\chi\circ \phi}$.

No clean tensor then, because we lack a clean product. At least, the tensor representation is assume to cast more than it is worth. We just use the ascent functor.

Peace.


\section{6/4/18}
Using the new description of the left adjoint to prove that acyclics get preserved.

Let's once again return to the `simple' case of two horns.

For $\xi\of [m]\to[n]$, $L(\xi,k)$

$\simplex[m]\times F(\xi)$ where the latter consists of nondecreasing sequences of $\sum_{k\of[n]}\prod_{l\of [n]-\set k} \xi_l$.


Strange tensor of simplicial sets:
$X\otimes Y$ with \[(X\otimes Y)[n] = X[n]+Y[n]+\sum_{i+j+1=n} X[i]\times Y[j]\]
The problem is the action of $\simCat$ on this tensor. The functions that splits up $\simCat$-morphisms according to dimension in order to 
seems rater complex.

The basic tensor above should simply split the action in two actions:
the lower range applies to $X$ and the upper to $Y$.

We need a fibred version of this in $\ambient\s/\simplex[n]$: for each $k\of [n]$ we split the action morphism in two parts.

Actually, we can turn this around. First of all $X\otimes Y$ with the action just described has a morphism $X\otimes Y \to \simplex[1]$ which I used at one point.

I am striving for 'orthogonality': the idea is to describe the fortification as a tensor product with a constant, because this hopefully simplifies the generalization to arbitrary fibred categories.
It looks like it is going to be rather specific to the simplices though.

Perhaps not totally useless\dots
It is going to be like this:
We will have $f(x)\of \base(\simplex[n])$
and $g(y)\of \base(\simplex[n])$.
These have a combination $f(x) \otimes g(y)$ of combined dimension, which explain how the action is split up.
This looks like structure on $\simplex[n]$ itself. It seems to be burried much deeper though.

\paragraph{Could more elements help?}
A bigger tensor product allows for more way for the action to be cut up.


$X\otimes Y$ would consist of triplets $\tuplet{\beta,x,y}$ where $\beta\of [n]\to\bool $ is a not necessarily monotone function, $x$ is a simplex of $X$ whose dimension is the numbers of zeros in $\beta$ minus one or some placeholder if there are no zeros. 
Similarly, $y$ is a simplex of $Y$ whose dimension is the number of ones in $\beta$ minus one, or a placeholder if there are no ones. 
There could be something with indiscrete simplicial sets.
The action does not seem to come any more easily.

\begin{align*}
i_b(n) &= \min\set{i\of\dom(\phi) | \beta(\phi(i)) = b, \forall m < n. i_b(m) < i}\\
\phi_b(n) &= \#\set{j\of\cod(\phi) | \phi(i_b(n))\geq j, \beta(j) = b}
\end{align*}
NB: off by one errors lurking everywhere\dots
With the help of these, let:
\[ \tuplet{\beta,x,y}\cdot\phi = \tuplet{\beta\circ \phi,x\cdot\phi_0,y\cdot\phi_1} \]

We now definitely have too many elements. 

\paragraph{fibrewise}
We have a kind of product:
$\base(\simplex[n])\times\base(\simplex[n]) \to \base(\simplex[n])\times\base(\simplex[n])$
It combines non decreasing maps into nondecreasing maps on combined domains.

I really want this tensor product to be a thing. Too much is hinging on the ordering of $[n]$ however.

The indiscrete tensors basically create new simplicial objects by glueing every simplex of one to every element of another. Sounds like a recipe for contractible simplicial objects, which does not look good. Yet some glueing together is exactly what we do.

\paragraph{deeper insight}
I thought in terms of a functor $S\of \simCat/[n]\to \ambient\s/\simplex[n]$. To represent this functor more easily, I already introduce a kind of tensor product construction, showing (non trivial) the simplices of $S[n]$ are new simplices glued between a source and a target simplex. This potentially allows us to represent the co-descent functor more easily. Yes, we can surely combine two tensors into a simpler one.

The new tensor product is like an indiscrete sum. I worry that it will be too indiscrete.

There is a great number of ways a $\phi\of[m]\to[n]$ can be split up in two parallel morphisms and have each act on a different part of the structure. Worse still, we need $n+2$ subdivisions to handle all composite simplices. The simplest solution of using the lower range for one and the upper range for another won't do.

Introduce an indiscrete union of $\simCat$.
Let $\alpha\of[p]\to[r]$ and $\beta\of[q]\to r$. Define
$\alpha\sqcup\beta\of[p+q+1]\to [r]$ by:
\begin{align*}
\alpha\sqcup\beta(n) &= \min\set{ k | \exists i,j. i + j = n, (\alpha(i) = k \land \beta(j) < k ) \lor (\alpha(i) > k \land \beta(j) = k )}
\end{align*}
The struggle goes on.

We need $\alpha \to \alpha\sqcup\beta$ and $\beta \to \alpha\sqcup\beta$, with all the commutativity implications. It should also be clear that for each $\gamma\of[n]\to [r]$ there are $n$ pairs $\tuplet{\alpha,\beta}$ such that $\alpha\sqcup\beta = \gamma$. Finally, $\sqcup$ should be a functor $\simCat/[r]\times\simCat/[r]$

Let $\phi\of [m]\to [n]$. Invert it as follows: $C(\phi)\of [n]\to \nno$
satisfies $C(\phi)(i) = \#\set{j\of [m]|\phi(j) = i}$. There is like a universal bundle for $[n]$ and this is the characteristic function.
We can go the other way around: given $f:[n]\to\nno$, let $S(f)\of[(\sum_{i\of[n]} f(i)) - 1] \to [n]$ and let 
\[S(f)(i) = \max\set{ k\of[n] \middle| i \geq \sum_{j < k} f(j) }\]

With this translation, $\alpha\sqcup\beta$ is simply the conjugate of $+$ on $\nno$. Morphisms are harder to define in this setup. The simplest solution is just to stick to initial segments.

\paragraph{where we are}
The left adjoint combines elements from the pullback with these extra elements using this indiscrete sum construction. Intuitively, the Indiscrete sum commutes with the pullback, so the simplices like they add some decoration to simplices in the ordinary pullback.

Such commutativity is worth noting! The descend construction could be described as taking the dependent product, after modifying the structure to give it stronger lifting properties. 

There is a great advantage to doing this over the horn, however. Let's not forget that.

A new wind\dots

The discrete sum is a problem however. Combining simplicies of complementary dimension is simple and makes a lot of sense. Simplicial objects require something extra however, which involves a choice on about  interleaving the posets that looks highly specific and crucial.


A `path bundle`? Put a structure over $\horn[n]$ which is locally like the projection $\simplex[1]\to 1$, but manages to capture the complexity of the product.

The path bundle $P\to \horn_k[n]$ has two disjoint sections. The of the elements are paths according to which two elements will be joined together. $P$ consists of pairs of simplices to be joined together 

The bundle ought to be a fibration and we will see about the local trivialness.

How would that work out though? 
\begin{align*}
\base P &= \base \horn + \base \horn + \sum_{i < n} \horn[i]\times\horn
[n-i-1]
\end{align*}
All the complication winds up in the definition of the action, which is what we have been struggling with all day. Does this help us define the bundle though?

We need the action below to work for the bundle above, so we need to know which restriction maps to apply. That does not seems to be encoded here.
$[i]+[j]\to [i+j-1]$ or something like $2^{\set\leq}$

\paragraph{what about}
Another explosion. No, what I am thinking is exactly what I rejected because we we forced to cram simplices together in a way that violate the ordering.

So we have the indiscrete two element thing that almost tells us what we need.

But we need something for each pair in the product.

To cover all the bases, we need $\horn \sqcup \horn \to \horn \times 2_i$. The extra $2_i$ is needed to determine how the action of $\simCat$ is divided between the to parts of the simplex. 


\paragraph{closing}
There is a serious problem with modifying fibration first and then taking the dependent product: descended fibration have to pullback to themselves. If we don't lose the modifications in the pullback, descend fails for the original fibration, but if we lose the modifications in the pullback, descent fails for the modified fibration\dots I think. Better check this out. 
Actually, pullback and fortification do not commute. Consider how fortification makes sure that $d_k\of[n-1]\to[n]$ becomes a preserved acyclic cofibration.

I essentially have a more direct way of defining codescent. Let $f\of X\to \simplex$.
$\base CX$ consists of pairs $\tuplet{x,y}$, where $x\of \base X$ and $y\of \mathbf{nds}(\prod_{l\neq k} f(x)_l)$--note that $\mathbf{nds}(\prod_{l\neq k} f(x)_l)$ has the empty sequence as element when the product is empty and this has a huge impact on what pairs are valid--or $x\of
\base\horn$ and $y$ is a non empty member of $\mathbf{nds}(\prod_{l\neq k} f(x)_l)$. We add a lot of simplices and glue simplices of $X$ to them as well.
The restriction map is very complicated--based on the idea that the connecting simplices are glued in over $k$--but I promise it exists.
The trick is obviously that simplices get padded with extra points over the top edge of the horn, so they aren't destroyed in the pullback anymore.

Even with we add variables for genericity, its should be clear that if we can take another horn inclusion, the pullback after the fortification leaves an acyclic cofibration. We show how missing faces can now be glued in dimension by dimension. Hopefully the problem with the restriction maps does not make the proof completely unreadable.

After this is done, we introduce the actual descend functor, using a Yoneda-lemma like idea. The preservation of modest morphism should be trivial and that descend inverts pullback should be clear as well.

Done for today.

\section{23/3/18}
\paragraph{The codimension problem}
We need our structure to be a functor from the category of elements of $\simplex$ to $\ambient\s$. While this means there is an action involving arrows of $\simCat$, it is not a total action on that category. So those parts will have to be reworked. That wasn't very hard to fix.

Perhaps we can improve on the description of the action somehow. Let's not try today.

\paragraph{The painful bit}
The inverse image functor sends acyclic cofibrations to acyclic cofibrations that are stable under pullback along the horn.

How does that work?

We can easily see that the inverse image functor adds simplices that are fortified.

\section{9/3/18}

Begin with the 'simple case' and generalize.

The left adjoint modifies acyclic cofibration so 

\paragraph{A minute}
Starting with $\xi\of[m]\to[n]$ just let $S(\xi,k)$ be pairs of maps $\tuplet{f,g}$ where $f\of [i]\to[m]$ and $g\of [j] \to \prod_{l\neq k} \xi_l$. I.e. $g\of[j]\times[n-1] \to [m]$ such that $\xi \circ g\tuplet{x,y} = y$ if $y < k$ and $y+1$ if $y \geq k$.
Same data, different representation. This will have impact on the simplicial structure, though.
\begin{align*}
\dim\tuplet{f,g}&=\dom(f) + \dom(g) + 1\\
f_*(k) &= \min\set{i\of\dom(f) | f(i) > k}\\ %needs better symbol
\tuplet{f,g}\cdot\phi &= \tuplet{f^\phi,g^\phi}\\
\textrm{where } &f^\phi(i) = f(\phi(i)) \textrm{ if } \phi(i) < f_*(k) \\
\textrm{and } &f^\phi(i) = f(\phi(i)-\dom(g)) \textrm{ if } \phi(i) \geq f_*(k) \\
\textrm{and } &g^\phi(i) = g(\phi(i)-f_*(k)) \\
s(\xi,k)\tuplet{f,g}(i) &= f(i) \textrm{ if } i < f_*(k)\\
s(\xi,k)\tuplet{f,g}(i) &= k \textrm{ if } f_*(k) \leq i \leq f_*(k) + \dom(g)\\
s(\xi,k)\tuplet{f,g}(i) &= f(i-\dom(g)) \textrm{ if } i > f_*(k) + \dom(g)
\end{align*}
The helpful $f_*(k)$ point to where $g$ is glued to $f$.
This approach is clearer, despite the complexities. Demonstrating that this does define a simplicial object may be less straightforward.

And then we do find a downside: there is no room for empty $f$ or $g$. Is should be possible for a simplex in $S(\xi,k)$ to completely belong to the fortification, or to the normal simplex. This way it cannot. This makes the calculations above more complex.

So we have to take into account that either $f$ or $g$ may have an empty domain. This is a special case where the computation above do become simpler however. Also, what really matter here?

The combination with the pullback introduces the limitation that $f$ must skip an element of $[m]$ different from $k$.

So what about these structures matters now?
Besides the simplicial structure, we also need a cosimplicial structure. Somethin like:
\begin{align*}
\phi \cdot  &\of S(\xi\circ \phi,k) \to S(\xi,k)\\
\phi \cdot\tuplet{f,g} &= \tuplet{\phi\circ f,\phi\circ g}
\end{align*} 
That is fine.

Another important point is the intersection lemma. The fortification part respects intersections of simplices.

\paragraph{elusive descend then}
Preservation of restriction action provides an opportunity to focus on a number of generators and perhaps a set of relations. But we option not to work that way. 

So the idea is that morphism $S(\xi,k)\to f$ replaces an actual simplex.

Think about generators

For $\xi\of [m]\to[n]$ and $k\of [n]$. There are monomorphisms $a\of\bullet \to [m]$ that are 'maximal' for the property that $\xi\circ a$ is part of the horn, $n - 1$ of them, to be exact. Then there are monomorphisms $b\of \xi_{\neq k} \to \prod_{l\neq k} \xi_l$, which also look like generators. We need to pair these up again and discuss how they may overlap.

Every pair of generator can overlap where they differ in only one point. 
Actually, $b$ is a bigger problem here, simply because there are so many of them.

What does this have to do with the fibration $Df\of DX\to\horn_{?}$ we want to descend?
Generators map to $\horn_{?}$ as well. For each generator, pick an element $x\tuplet{a,b}$ of the fibre of $f$ over $xi$.
Generators $\tuplet{a,b}$ and $\tuplet{a',b'}$ can overlap and that overlap implies a pair of morphisms of simplices $\tuplet{\phi,\phi'}$ such that $x\tuplet{a,b}\cdot \phi = x\tuplet{a',b'}\cdot \phi'$.

Since we need to do this over all $\xi$ with the same codomain--and provide functors to link the generators together, we only gain complexity by not using full simplices for $S$.

\paragraph{reversal}
When arguing that acyclicity is preserved I used to make a big point out of the generating elements. Okay, I remember why I should: quotients of acyclics can be cyclic.

Further subdivisions: $g$ as a sequence 

\paragraph{Another mistake!}
The right action is not actually from $\simCat$! The 'codimension' does not solely determine whether the action is defined. This is not a big problem, but awkward.

\paragraph{Closing}
I haven't regretted stopping to work on this paper for other activities in a long time. This was a rather good day of work.

\section{23/2/18}
\paragraph{Can't help replanning}
We separate two sides: the existence of the functors and their specific handling of cofibrations.

Acyclic cofibrations are closed under discrete morphisms. Is this a kind of discreteness that is orthogonal to a kind of connectedness?
Right lifting property with respect to 'simply connected' morphisms I guess. Which generalizes to: indecomposables are codiscrete--although in this case we are talking about a different kind of indecomposable.

In any case, we deal with model structures on many different categories here and their interrelations. So while we have a generic discrete family of acyclic cofibrations in $\ambient/s$, these 


Perhaps I am entangling two things that should not be entangled at all. One is a theory of model categories. The other is purely about constructive descent.
Of course, the descent theorem is about a constructive variant of the simplicial model structure. 

We always need a single object or morphism in $\ambient$ to realize various theorems. So it is not enough to\dots

There is a connection with the left adjoint of an adjunctions preserves the left morphisms in a factorization system, of the right adjoint preserved the right morphisms. We need to amend for the extra property that left morphisms are closed under 'discrete pullbacks', i.e. all categories have discrete morphisms and all functors preserve them.

What am I looking for now?
The individual case where we look at whether the codescent of a horn inclusion along another is an acyclic cofibration is complex. We need to make the case that this complex construction can be carried out parametrically, not just over all combinations of horn inclusions, but also when additional parameters (the object of all problems) are involved.
There is a discrete object of problems $P$. Each problem translates to a simpler problem $P \to C$ involving just a single combination.

Arguably, we are looking at the question of descent along acyclic cofibrations. Yes, ultimately we only need it for one. We have decent along a specific acyclic cofibration and we need it elsewhere.

I imagine descending a fibred product or coproduct and then somehow getting back what we need. This is complicated yet again.
I am starting to suspect that the orthogonality of discrete morphisms is very relevant here. First of all, discrete morphisms are fibrations, which is why we can apply descent to a composition involving a discrete morphism. How are monomorphisms fibrations? Well, none of the acyclic cofibrations have empty domains. Empty fibres are therefore allowed.

Descent takes the fibred product and then adds some extra faces. These faces never cross discrete boundaries, crucially because all acyclic cofibrations are connected. None of that helps to reduce the larger problem.

An approach that starts with the simplest solution and then generalizes it would have to be very sophisticated to take the interactions between discrete morphism an acyclic cofibration into account. I see little benefit in my case.

\paragraph{Other options}
Do much more inside the slice categories.
Use partially ordered objects.

\paragraph{different construction}
We described the constructions with the partially ordered objects, but there are alternatives.

For each $\xi\of\Ar(\simCat)$, $k\of \cod(\xi)$ and $p\of\nno$, we have a combination of morphisms. The first $a\of[p]\to[2]$ splits up the domain in three parts, $a_0$, $a_1$ and $a_2$. 
We get three morphisms $b_0\of a_0 \to \xi_{\leq k}$, $b_1\of a_1\times[n-1]\to \xi_{\neq k}$ and $b_2\of a_2\to\xi_{>k}$. Now we need some boundaries on what $b_1$ can do. 
 
Little progress today.

\section{9/2/18}
I remember that I was naming things more explicitly in order to make the proof easier to read.

What can I reasonable hope to achieve this day?




\paragraph{All the monads}
The category of simplicial objects $\ambient\s$ is a category of algebras for a monad on $\ambient/\nno$. That gives a slot of intuitions.

Coyoneda--every object is a colimit of representables:
\[
\colim_{\simplex[n] \to X} \simplex[n] \simeq X
\]
Well, this is not the proper dual.

In slices $\ambient/\s$ we get other objects of representables.
We can still say that every object is an indexed colimit however.

Enriched projectives maybe?
The idea is that the sections functor down to $\ambient$ preserved regular epimorphisms. Every object is covered.

What is the point? The 'projective resolution' has to make it simpler to define $D$.

The distance between intuition and implementation is to great. I keep
forgetting how it works.

\paragraph{god help me}
The monomorphisms are a good reduction. So the monomorphisms of $\simCat$ are acyclic cofibrations. Pulling back along the generic acyclic cofibrations fails to preserve this however.

We have a general method for 


\subsection{Descent, classically}
I am starting backwards here. We do the following pullback, where:
\[\xymatrix{
\bullet\ar[r]^f\ar[d] &\bullet\ar[r]\ar[d] & \horn_l[m]\ar[d]^g\\
\simplex[i]\ar[r]_{\simplex(h)} & \simplex[j]\ar[r]_k & \simplex[m]
}\]
Under the assumption that $i<j$, $\simplex(h)$ is an acyclic cofibration. In many cases $f$ is too. We need it to be true always. Solution:
Introduce another functor $S(g,k)\of\simCat \to \ambient\s$ that gives better simplices.
\[\xymatrix{
\bullet\ar[r]^{f'}\ar[d] &\bullet\ar[r]\ar[d] & \horn_l[m]\ar[d]^g\\
D(g,k)[i]\ar[r]_{D(g,k)(h)} & S(g,k)[j]\ar[r]_{s(g,k)} & \simplex[m]
}\]
The point is that each monic is send to a preserved acyclic.

How do we use this though?

The constructions are generalized abstract nonsense and I lack the ability to express them properly. 

Ultimately, the descend functor is defined in such a way that $\hom(k, Df)$ must be $\hom(g\ri(s(g,k)),f)$. Moreover, all of this must be parametric in $g$ and $k$, otherwise it will not result in the needed lifting operator.

\paragraph{Split}
I want to rigorously separate the technical details of the lifting operator from the construction of the descend functor. That is the only way to keep my baring here.

I think the notion of sending monics to acyclic cofibrations is spot on.

That 'category' $\cat P$:
The objects are pairs $\tuplet{\xi,i}$ where $\xi\of \Ar(\simCat)$ and $i\of\cod(\xi)$.
A morphism $\tuplet{\xi,i}\to \tuplet{\xi',i'}$ requires that $i'=i$ and is a morphism $\phi\of \dom(\xi)\to\dom(\xi')$ such that $\xi = \xi'\circ \phi$.

I keep struggling with all the abstract nonsense.

Another approach: $D$ is the coequalizer of easier functors. 

One way was the bimodule, the structure with both a left and a right action, not necessarily compatible.

The elements are actually morphisms $S \to X$, but probably part of a fibred product, so 
\[\Sigma c\mapsto {\set{a\of A|b(a) = c} \to \set{ x\of X | d(x) = c}}\]
The equalizer annoyingly is $\function x {f(x\cdot \phi)} = \function x f(x)\cdot \phi$. The action $f\cdot \phi = \function x{f(\phi\cdot x)}$. 


\paragraph{fine grain}
Let's start with an adjoint pair of functors with certain properties,
Like sending 

Note that we just take for granted now that fibrations are closed under indexed coproducts. Eventually, we will introduce this fact at the start and use that where ever it is convenient.

\paragraph{distributions}
The notion of a distribution is difficult enough when slice categories are not involved, but can we derive the more general construction form the simpler one?

One direction seems to come about by accident. The left adjoint already sends morphisms to a slice category. Does the right adjoint still do the right thing though?

'There is a functor with these properties'
What we started out with, was a target for the representable objects.
So $\Phi \of X\nrightarrow Y$.
The sum of all those representables is the 'projective' cover of $Y$.
We can also view $\Phi$ as target for the terminal object.

\paragraph{projectives}
The ideas is that we define the functors from projective resolutions.
What does that really help, though?

The trick is to get the adjunction from a most amount of structure, in a fairly generic way. The definition I have looks clumsy and overly technical.

Perhaps we can replace the right action with something easier.

I was kind of hoping we could replace it with the equivalence it induces. 








\section{4/2/18}
What about free fibrations?
We can freely add a lifting operator to a simplicial set. In fact, several structures are in the paper already. The problem in categories of algebras preserve liftings and we want to consider morphisms that do not. Can we recover those with an exact completion?
I am afraid that the exact completion will not add anything useful because the parallel pair will be a pair of morphisms.

This talk of monads suggest that we could construct an fibrations-acyclic-cofibration factorization system, in the form a lifting operator monad in a slice category. I think the problem is that the unit is not an acyclic cofibration. The fibred monad is hard to construct.


\section{12/1/18}
Back in business.

I am really confused again. The construction is just too complicated.
The object $S$ should consist of tuples:
\[ \tuplet{p,s,t,x} \]
Here $p$ is the problem $\horn_i[j]\to V$,
The $s$ is an element of the 'source' simplex and 
the $t$ is an element of the 'target' simplex;
both are elements of $\Ar(\simCat)$ with codomain $i$.
Finally, $x$ is a suitable nerve of a suitable poset.

This is frustrating.

The category $\cat P$ consists of pairs $\tuplet{p,\pi}$ where $p$ is one of the problems $p\of\horn_i[j]\to V$ and $\pi$ is a morphism of $\simCat$ with codomain $i$. What are the arrows? There are only arrows in the fibres over each problem. There we only have $\phi\of\tuplet{p,\pi\circ \phi} \to \tuplet{p,\pi}$.

Breathe.

There is a functor $\cat P\times_P \cat P\dual \to \ambient$ we want to represent. It should work somewhat like this: 
$\tuplet{p,s,t,\phi\cdot x} = \tuplet{p, s\circ \phi, t, x}$
$\tuplet{p,s,t,x}\cdot \phi = \tuplet{p, s, t\circ \phi, x\circ \phi}$.
depending on $p$ we factor $t$ though a non decreasing $w$.
That is what the poset is for.


\paragraph{Diversions}
Equalizers (as domains) induce coequalizers on homsets. No that is not right. Only if the codomain is injective. Injective envelopes do help with that.

Proving the equality of functions whose domain is defined as a equalizer is the problem here. Topos theory suggests the following solution. For $f,g\of X \to Y$, where $X = {z\of Z|p(z)=q(z)}$
compare the following relations instead of the functions:
\begin{align*} 
F &= { (z,y)\of Z\times Y | p(z)=q(z),f(z) = y } \\
G &= { (z,y)\of Z\times Y | p(z)=q(z),g(z) = y } \\
\end{align*}
This might be complicated because $Z$ could be a sum of other types types and $f$ and $g$ may do a case analysis.

Still, it seems like we can reduce the problem to finding the contradictions in $p(z)=q(z),f(z) \neq g(z)$. Fine, not the same thing as straightforward equation solving, but easily within reach of Prolog e.g.

That should be the general strategy: model checking, where we search for examples where an expression violates the assumption connected to its type.

\paragraph{Back to work}
Figure out how this part has to work again.
No I am giving up for today.

\section{29/12/17}
How do we prove descend?


\paragraph{properly defining the object of problems}

In general, it may be smart to introduce default function names
for every bit of structure often used. I.e. an object of a slice category is a pair $P = \tuplet{\base(B),\mathbf{supp}(B)}$ etc.

Beyond that, I just need some consistency.


\paragraph{ambition}
Actually turning this into a programming language\dots
So all the structure on $\ambient$ becomes definitions for types and functions. There is no real computation beyond the unification of paths, because type checking requires this.

Much of what we define goes beyond $\ambient$, however. A simplicial object is a type and a couple of functions on top. The proper class of simplicial objects exists on a whole other level than the internal structure we can prove the properties of.
We can add it to the language as a kind system, where kinds are closed under limits somehow, but little more.

Perhaps the 'proper class as a kind' clarifies my world: take the exactness of $\ambient$. The pseudoequivalences in $\ambient$ are tuples of morphisms satisfying certain equations: a proper class. Our assumption is that there is a function that takes an element of this class to a coequalizer.
Here things get interesting: to provide a unique factorization we need another function. The path unification algorithm has to enforce uniqueness, otherwise 

I don't know about feasibility. I think what I need is more than just path unification, to prove equalities than cannot be derived.

\paragraph{the right pullback?}
I don't see yet how the fact that the pullback $s_\xi\ri(k_P)\of \horn_P\times_{\simplex_P}S_\xi \to S_\xi$ is an acyclic cofibration, will ultimately factor into the proof. Perhaps a factorization provides an easier way to establish that some morphisms are acyclic cofibrations.
I think it is a red herring.

Most monomorphisms between simplices over $\simplex_P$ get preserved in the pullback along $k_P$ because they factor through it. There is literally one family of exceptions, which is the focus of the proof.

\section{17/12/17}
No nerve? We take the nerve of $S$ and then use it in the construction of an adjoint pair of functors. Can we combine the constructions and skip the nerve altogether? I suspect the answer is no.

There clearly is an adjunction, now that I think of it. The left adjoint takes a simplicial object $X$ to the ordered object:
\[ \set{\tuplet{x,n}|x\of\base(X),n\leq \dim(x)} \]
Where $\tuplet{x,n}<\tuplet{x',n'}$ if and only if $x=x'$ and $n<n'$. Morphisms pose no problem.
In order to get transposes of simplicial morphisms, we need to demand that $f(\tuplet{x\cdot\phi,n}) = f(\tuplet{x,\phi(n)})$... so we take the quotient be the least equivalence $\sim$ that makes $\tuplet{x\cdot\phi,n}\sim \tuplet{x,\phi(n)}$. This has consequences for the ordering as well. A nondecreasing map now transposes to a map into the nerve.

Does this help us somehow? It is kind of interesting that we don't need dimension anymore. We just deal with posets. Also, rather than a monad on the category of poset, we ought to get a comonad.
A! The ordering is not always decidable because it extends equality. Decidability may be crucial in several crucial cases. That is an important point.

\paragraph{Planning}
The idea that power the latest rewrites is to let the structure of the proof determine the structure of the text. This seems impossible right now. So we need another structure.

'distributions' or 'distributors' of simplicial sets. Descend is a 'distribution', a generalized function that takes values beyond simple simplices.

We don't actually need the structure on $\horn$. The one on $\simplex$ is fine, but it is similar in nature.

I walk away with a couple of questions:
\begin{itemize}
\item What is this adjunction with posets all about. Can it make our live simpler?
\item How to structure the section on descend?
\end{itemize}

The left adjoint sends cycle and horn inclusions to isomorphisms. It destroys structure that is unavailable in the category of posets.
Posets are a reflective subcategory, I guess. The truncation to the lowest dimension.

Back planning.

The basic story is that we start with the dependent product and note that it already preserves acyclic fibrations and then explain why other fibrations are not as lucky. I don't prove that there is no simpler alternative\dots

\paragraph{I remember}
After taking the fibred product, we end up with a fibration that cannot solve all lifting problems. So we glue them back in\dots
The trick is to create a new simplicial object that has a simplex were the product has a hole.

The poset $S\to\set\leq$ guides this process, but its role is rather indirect. We can figure this out.

\section{15/12/17}
What to do today?

Some of the posets really look like dependent sums of exponentials. I keep struggling with that fact, because it keeps looking like a simpler exponential will do the trick.

The object of problems is $\set{ \tuplet{\xi,k,l} | \xi\of\Ar(\simCat), k\of \dom(f), l\of\cod(f) }$.
The descend functor and its left adjoint depend on $\cod(\xi)$ and $l$ only.
The object of problems is actually $\hom_{\set\geq}(\horn_{\set\geq},V)$? Only if we forget that we have to solve a family of lifting problems!
Once we take those, we see that the problem space is actually a pullback:
\[ P\of \set{ \tuplet{\xi,k,l,v} | \xi\of\Ar(\simCat), k\of \dom(f), l\of\cod(f), v\of\horn_l[\cod(f)]\to V } \]

Over this problem space we find the families of horn inclusions to descend along. It only depends on $\cod(f)$ and $l$, with the rest of the variables sitting there, doing nothing.
The cosimplicial stuff works with the richer sets and depends on the same dimensions of course. It is easy to forget which side has the codirection.
We should have a simplicial set over the horns, whose underlying object has an independent cosimplicial structure over the simplices the horns are included in.

A slightly easier way to view this cosimplicial, is as a family of posets (po-objects?) over $P$, or once again, rather its projection onto the relevant indices. Here we get a unexpected dependence on $\xi$, however.

We may have a real problem here. We need to proof that a 'codescend' construction along a specific horn preserves specific acyclic cofibration. Inspection now suggests that the codescend construction depends on the acyclic cofibration we are trying to lift. This is not permitted.
There is no direct dependence: $\xi$ is the value of the cosimplicial structure. We have a family of posets $A$ and a map $b\of\base(A)\to\base(\simplex_\leq)$ and the $\xi$ that is worrying us, is simply this $b$. So no real problem.

The construction is actually rather strange than. For each element of $\base(\horn_\leq)$, we get a collection of factorization through other posets over their codomains. Those other posets are really best indexed with their target pairs\dots.
That is how it works: there is a cosimplex of posets over $\base(\simplex_\leq)$. The nerve preserves the cosimplicial structure and adds a morphism to $\horn_\leq$. 

\paragraph{down to earth?}
The category $\ambient/\nno$ has two monads $-\otimes\simCat$ and $\simCat\times-$. Simplicial objects are algebras for $S$ and cosimplicial objects are algebras for $C$. Everything comes together in this category, including the discrete problem objects, families of posets over them etc. So can we just work here? The functor requires two dimensions on every object.

We are dealing with endoprofunctors on $\simCat$.

I have cleared all the obstacles, but the sheer complexity prohibits progress.

\begin{itemize}
\item the adjunction is our argument for preservation of fibrations.
\item it is also to source of preserved $M$.
\item the bimodule that generates the adjunction is fucking complicated itself.
\item we haven't even started showing that is sends the generic family of acyclic cofibration to a family of cofibrations.
\end{itemize}

There seems to be no birds-eye view here. Everything is in the fucking details.

\paragraph{details}
The underlying object:
\begin{align*} S = &\set{\tuplet{\xi,i,0,j}| j\of \dom(\xi)} \cup\\
&\set{\tuplet{\xi,i,1,j}| j\of \cod(\xi) - \set i\to\dom(\xi),\xi\circ j = d_i}\\
\end{align*}

Where $d_i$ is the inclusion $\cod(\xi) - \set i \to \cod(\xi)$.
Its ordering:
\begin{align*}
\tuplet{\xi,i,0,j} < \tuplet{\xi,i,0,j'}&\iff j< j'\\
\tuplet{\xi,i,0,j} < \tuplet{\xi,i,1,j'}&\iff j\leq i\\
\tuplet{\xi,i,1,j} < \tuplet{\xi,i,1,j'}&\iff \exists k\of \cod(\xi) - \set i. j(k) < j'(k) \\
\tuplet{\xi,i,1,j} < \tuplet{\xi,i,0,j'}&\iff i < j'
\end{align*}
Note however that we still have to take the nerve to see this monster in its full glory.

The important non decreasing map:
\begin{align*}
s\of S &\to \set\leq\\
s\tuplet{\xi,i,0,j} &= \tuplet{\xi(j),\cod(\xi)}\\
s\tuplet{\xi,i,1,j} &= \tuplet{i,\cod(\xi)}\\
\end{align*}


This is the most simplified version, without the map to $V$ hanging around to cause confusion.
The nerve defines its own dimensions. Important point though: the morphisms cannot cross over to different $\tuplet{\xi,i}$ because the ordering doesn't connect any of those. 

The nerve takes non decreasing maps $\sigma\of[n]\to S$ and creates a simplicial object from them. We take a subset by the way: 
\[ D = \set{ \sigma\of N(S)|s\circ \sigma \of \base(\horn_{\set\leq}) }\]
This immediately shows how to map to the horn. 

If $\xi = \xi' \circ \phi$, then $\phi\of\tuplet{\xi,i}\to\tuplet{\xi',i}$ and: 
\begin{align*}
S(\phi)\of S\tuplet{\xi,i}&\to S\tuplet{\xi',i}\\
S(\phi)\tuplet{\xi,i,0,j} &= \tuplet{\xi',i,0,\phi(i)}\\
S(\phi)\tuplet{\xi,i,1,j} &= \tuplet{\xi',i,0,\phi\circ j}
\end{align*}
So the `codimension' of $\tuplet{\xi,i,j,k}$ is $\dom(\xi)$ and $S(\phi)$ defines the cosimplicial structure. Note that:
\[ s\tuplet{\xi',i}\circ S(\phi) = s\tuplet{\xi,i}\]

Suppose $\sigma \of D$. The first two elements $\sigma(0)_{01}$ is all we need to get were we need to be in $\base(\simplex_{\set\leq})$. Done!

\paragraph{Conclusion}
I propose that we just give the descend construction and then demonstrate its properties one by one.

\section{1/12/17}
I have a first draft of a section on cosimplicials now. How much does it do for me?

We need to work out the details on the cosimplicial object. That determines both why $D$ is actually a descend functor that preserves fibrations.

There is a mismatch between the total set of problems, en the solution in the sense that the solutions aren't necessarily different. I.e. $P$ has many members that have the same solutions. There should be some map for this.

\paragraph{nerves}
Since nerves make things easier, find a poset to represent the set of problems.

\[ P = \set{\tuplet{i,j,k}|i\of\nno,j\leq i, k\leq i}\]
Where $\tuplet{i,j,k}\leq \tuplet{i',j',k'}$ if $i=i'$, $j=j'$ and $k=k'$. That is because the first to number serve as indices to the set of problems.

The subset $Q = \set{\tuplet{i,j,k}\of P|j\neq k}$ allows us to define the functor $S$ in an easier way. Given $f:X\to P$ we extends the domain is an unfortunately complicated way. For each $i\of\nno$ and $j\of[i]$ we add the slices of $[i] - j$ to the fibre over $j$. The new ordering puts the slices above $x\of X$ such that $f(x)\leq j$ and below $x\of X$ where $f(x)>j$. That is it.

Too much work perhaps. I feel we only need only one good monotone map and do the rest in the category of simplicial sets. The domain is still a coproduct of two different posets with extra inequalities added to the ordering.


\section{17/11/17}
The construction of the adjoint functors is easiest to understand when we consider that all of the categories are algebras of monads on slice categories of $\ambient$. Given two simplicial objects $A$ and $B$, a bimodule $A\nrightarrow B$ is a simplicial object over $B$, with a morphism $m\of\base(M)\to \base(A)$ and an left action $\cdot$ of $\simCat$, such that $\xi\cdot x$ is defined if $\dim(m(x)) = \dom(\xi)$ and $\dim(m(\xi\cdot x)) = \cod(\xi)$.

Let's forget about $B$ for now and focus in this weird $M$ part. One functor $M\ri\of \ambient\s/A\to\ambient\s/M$ is defined by first taking the pullback along $m$ and then taking the quotient by an equivalence relation: $\tuplet{x\circ \xi , y}\sim\tuplet{x,\xi\cdot y}$. The simplicial structure of $M$ now comfortably turns this into a new simplicial set. What about preserving morphisms? Because morphisms commute with the restriction action on $A$, the quotient is well defined and the way that the new restriction is defined poses no difficulties. Hence, functor.

Another functor $m_*\of\ambient\s/M\to \ambient\s/A$ is defined by first taking the fibred product $\prod_m(X)$ and then by taking the equalizer of the two restriction actions definable on this product: $f(\xi\cdot x) = f(x)\cdot \xi$ for all $x$ and $\xi$ where $\cdot$ is defined. Here the monad plays a clearer role. There are two algebras for the same monad on the product and we pick the element where both actions agree.
Once again, we have to ask whether this works well with morphisms, but the pointwise definitions hardly form a challenge.

That $m_*$ preserves modesty follows from our assumptions about modesty. What about adjunction?

For starts, we already have an adjunction between the pullback and the fibred product. The coequalizer and equalizers fit together to make the adjunction between $m\ri$ and $m_*$ work.

Reintroducing $B$, we get a simpler adjunction $\ambient\s/B\to \ambient\s/M$ in the form of the reindexing functor and its left adjoint. When applied to the descend problem, $B$ is the family of horns and $A$ is the family of simplices. This idea of fattening becomes a little but clearer, although some strange shit happens on the way back down to $A$. At that point the specifics of the construction are required to prove that the descend functor is right inverse to reindexing as it should and that its left adjoint preserves coequalizers.

Note: $\tuplet{x\circ \xi , y}\sim\tuplet{x,\xi\cdot y}$ means the projection to $y$ is not well defined! This means that the result is no simplicial set over $M$ nor a member of category $\ambient\s/M$.

Note: $M$ should be closed under quotients. Is it though?


\paragraph{rewriting ideas}
\begin{itemize}
\item Use object of lifting problems more often. This may be easier to follow than arguments about lifting problems in slice categories. Emphasize the importance of $\ambient$-indexed coproducts everywhere.
\item Try to use intuitions about monad to do the pushout product and pullback exponential better.
\end{itemize}



\section{3/11/17}
The construction uses nerves of partially ordered objects of $\ambient$. The Yoneda lemma tells us that this is a fully faithful subcategory of the category of simplicial objects.

Let's start making a new to do list:
\begin{itemize}
\item rewrite 'descent' with the new proof;
\item find and rewrite proofs that may be easier to follow using nerves;
\item write a section on nerves alone if useful.
\end{itemize}

Can I outline the new descent chapter?

Start as usual by outlining the properties of the class of modest morphisms. Why would anyone care? Why did we want the universe to be fibrant?
I explained that there is no model structure on general simplicial objects and a minimal requirement is that the universe is part of the model category.
We conclude however that this is no issue here, because the descent construction gives the universal morphism a codomain.

Describe descent. Here we got in trouble because we need to generalize. There is a family of descend constructions, one for each horn-inclusion. Ever worse: for each $\xi\of[m]\to[n]$ and each $k\of [n]$ there is a special object $s\of\tuplet{\xi,k} \of S\tuplet{\xi,k} \to \horn[n]_k$ and the descend $Df$ of $f\of X\to \horn[n]_k$ is defined in such a way that $\simplex(\xi) \to Df$ is isomorphic to $s\of\tuplet{\xi,k} \to f$.

We can ignore how $s\of\tuplet{\xi,k}$ is defined for a while, because we don't need the details to show that $D$ is defined, preserves modest objects and that it has a left adjoint, all using the structure of $\ambient$. A small constraint makes $D$ right inverse to reindexing, meaning it is a descent functor. The final nail is the lifting property. The functor $D$ preserves fibrations, if its left adjoint preserves acyclic cofibrations, than it right adjoint preserves fibrations. We reduce the problem to the family of cofibrations, so that ultimately, we only need to show that a single object is an acyclic cofibration.

So all that is left now is the descend proof that relies on all the nervy details. 

\paragraph{structural integrity}
I suppose a lot can be done without even knowing the specific morphism we will be descending along. We have a keep in mind that there is more than one though.

There is a family of morphisms to descend along: $A\to B\to I$. Once again I am looking for an elegant abstract description of the construction I need.
I don't have it yet.

There is an (internal) category $\cat B$ of $\ambient$ that represents the representable objects of $\ambient\s/B$. What we want to describe is a functor $S:\cat B\to \ambient\s/A$. However, to point is to internalize everything. The object $\cat B$ must become an internal object of $\ambient\s/A$ and $S$ must become some structure over it. It becomes a profunctor $\cat B \to \cat A$, which can be represented as a bimodule. On both sides the action it derived form the category of simplicial sets however.

That is where the 'sheaves are algebras' view comes in. Once we are in a slice category, restriction let's us define a monad and sheaves are algebras for this monad. The $A$ and $B$ about are similarly algebras. The object $S$ provides two dimensions for each of its elements and two actions. 

What is $\cat B$ exactly? I keep feeling like we cannot just use the underlying object $\base(B)$ of $B$, but haven't got a fix on the alternative.

There is $a\of S\to \base(A)$, $b\of S\to \base (B)$ with $a(x\cdot\xi) = a(x)\cdot\xi$ and $b(\xi\cdot x)\cdot \xi = b(x)$? The last equation is not quite natural. Leave it out.

I keep getting stuck here. Does the higher level of abstraction buy me
anything?

\paragraph{Stick with it}
In $\ambient\s/B$, the underlying object of $B$ represents the representable functors of $B$. The functor needs much more. For each $b\of\base(B)$ we have a whole simplicial object to describe and we need the morphisms too. This underlines the fact that $S\to B$ is not a morphism of simplicial sets at all.

I feel bad. I just want to get this over. It isn't getting any good though.


\section{28/9/17}
Let's try again.

\begin{proposition} The inclusion $(\bigcup_{j\neq b} U_j) \cap (\bigcup_{i\neq a} V_i)\to (\bigcup_{j\neq b} U_j) $ is an acyclic cofibration.
\end{proposition}

\begin{proof}
Let $K$ be the image of $\kappa\of \prod_{j\neq b}\set{i\of\dom(\beta)|\beta(i)=j} \to S\tuplet{\beta,b}$. 
Let $\mathfrak K$ be the set of faces $k\of K$ such that $k(0)$ is the least element of $K$ and if $k(p+i) \leq k \leq k(p+i+1)$ then $k(p+i)=k$ or $k(p+i+1) = k$.
Let $\mathfrak A$ contain $f\of U_{\beta(a)}$ such that $k\subseteq f$ for some $k\of \mathfrak K$, $f - k(i) \of \bigcup_{i\neq a} V_i$ for $i \leq \max(\dom(k))$, but not $f - k(\max(\dom(k)) \of \bigcup_{i\neq a} V_i$.

Let $A_0 = (\bigcup_{j\neq b} U_j) \cap (\bigcup_{i\neq a} V_i)$ and let $A_{i}$ be the union of $A_0$ with less than $i$ dimensional faces $f\of (\bigcup_{j\neq b} U_j)$ that satisfy one of these conditions:
\begin{itemize}
\item $f(p) = a$ for some $p$
\item $f\of \mathfrak A$.
\end{itemize}

For all $f\of A_{i+1} - A_i$, $f\circ d_i$ are members of $A_i$ safe one. If $f$ contains $a$ then each of the $f\circ d_i$ where $i\neq p$ satisfy $f(q) = a$ for some $q$ and hence are included in $A_i$. The face $f\circ d_p$ is not in $A_i$ because the only $i$-dimensional faces without $a$ are in $A_0\cup\mathfrak K$, but $f\circ d_p \of A_0\cup\mathfrak K$ implies $f\of A_0\cup\mathfrak K$ and hence $f\not of A_{i+1} - A_i$ as assumed.
If $f\of\mathfrak A$ then $f\circ d_i$ either intersect the same points of $k$ as $f$ and are therefore in $A_i$, or omit one of the points. Those will all be in $A_0$ except for the last by definition.

Because of this relation, the inclusion $A_i\to A_{i+1}$ is a pushout of a coproduct of horn inclusions and therefore an acyclic cofibration. Because acyclic cofibrations are closed under composition, so is $A_0\to A_i$ for all $i\of \nno$.
The propositions holds because $\bigcup_{j\neq b} U_j = A_{i}$ for some $i$.

If $f\of A_0$, if $f(p) = a$ for some $p$ or $f\of \mathfrak A$, then this is trivial.
If $f\of U_j$ for $j\neq \beta(a)$ and $j\neq b$, then the extension of $f$ with $a$ is a member of $U_j$ as well, so $f\of A_{\dim(f)+1}$.
Otherwise look for the greatest $k\of\mathfrak K\cup{\emptyset}$ such that $k\subseteq f$. If not $f - k(i)\of A_0$ for some $i\of \dom(f)$ then $f\of \mathfrak A$. If $f - k(i)\of A_0$ for all $i\of\dom(k)$, then there is a point of $K$ between $\max(k)$ and the next value of $f$ we can add, or $k$ would not be the greatest. The extended function $f + k\of\mathfrak A$ hence $f\of A_{\dim(f)+1}$.

Since $U_j$ are finite dimensional, all faces of $\bigcup_{b\neq j} U_j$ are member of $A_i$ from some $i$ on and this proves that the inclusion is an acyclic cofibration.
\end{proof}

After tying my head in a knot for so long, the result is almost insultingly simple. This does give confidence though.

\section{27/9/17}

\begin{proposition} The inclusion $(\bigcup_{j\neq b} U_j) \cap (\bigcup_{i\neq a} V_i)\to (\bigcup_{j\neq b} U_j) $ is an acyclic cofibration.
\end{proposition}

\begin{proof}
Let $K$ be the image of $\kappa\of \prod_{j\neq b}\set{i\of\dom(\beta)|\beta(i)=j} \to S\tuplet{\beta,b}$. If $K$ is non empty, let $k$ be a $\dim(K)$-dimensional face of $k$. This means we cannot add an extra point to $k$ without leaving $K$.
Let $\mathfrak K$ be the set of faces $f\of U_{\beta(a)}$ that have the following property. There is an $n$ and $p\of \dom(f)$ such that 
$f(p+i) = k(i)$ for all $i\of[n]$ and
$f\circ d_{p+i} = f - k_i \of (\bigcup_{i\neq a} V_i)$ but not $f_\circ f_{p+n} = f - k_n \of (\bigcup_{i\neq a} V_i)$.

Let $A_0 = (\bigcup_{j\neq b} U_j) \cap (\bigcup_{i\neq a} V_i)$ and let $A_{i}$ be the union of $A_0$ with less than $i$ dimensional faces $f\of (\bigcup_{j\neq b} U_j)$ that satisfy one of these conditions:
\begin{itemize}
\item $f(p) = a$ for some $p$
\item $f\of \mathfrak K$.
\end{itemize}

For all $f\of A_{i+1} - A_i$, $f\circ d_i$ are members of $A_i$ safe one. If $f$ contains $a$ then each of the $f\circ d_i$ where $i\neq p$ satisfy $f(q) = a$ for some $q$ and hence are included in $A_i$. The face $f\circ d_p$ is not in $A_i$ because the only $i$-dimensional faces without $a$ are in $A_0\cup\mathfrak K$, but $f\circ d_p \of A_0\cup\mathfrak K$ implies $f\of A_0\cup\mathfrak K$ and hence $f\not of A_{i+1} - A_i$ as assumed.
If $f\of\mathfrak K$ then $f\circ d_i$ either intersect the same points of $k$ as $f$ and are therefore in $A_i$, or omit one of the points. Those will all be in $A_0$ except for the last by definition.

Because of this relation, the inclusion $A_i\to A_{i+1}$ is a pushout of a coproduct of horn inclusions and hence an acyclic cofibration. Because acyclic cofibrations are closed under composition, so is $A_0\to A_i$ for all $i\of \nno$. All we need to show now is that $\bigcup_{j\neq b} U_j = A_{i+1}$ for dimension $i$ of $\bigcup_{j\neq b} U_j$. As you might have guessed, this is the hardest part.

If $f\of A_0$, if $f(p) = a$ for some $p$ or $f\of \mathfrak K$, then this is trivial.
If $f\of U_j$ for $j\neq \beta(a)$ and $j\neq b$, then the extension of $f$ with $a$ is a member of $U_j$ as well, so $f\of A_{\dim(f)+1}$.
If $f\of U_\beta(a) - A_0 - \mathfrak K$, then we can add a point of $k$
 to get a member of $\mathfrak K$, because \dots
\end{proof}

I cannot finish the proof yet, because I am unsure where we actually can add points of $k$ to any $f$. Alternatively, we replace $k$ with all faces of $K$ of maximal dimension though and retain all the properties I think are important:
\begin{itemize}
\item if $f$ contains all $k$ but removing a point always results in something from $A_0$, then $f$ must be of $U_j$ for some $j$ by some sort of pidgin hole principle.
\item the number of elements of $\mathfrak K$ is limited, such that removing a point of the critical segment never lands in $\mathfrak K$. Hence the property: if $k(i)\leq l \leq k(i+1)$ then $k(i) = l$ or $k(i+1) = l$.
\end{itemize}

\section{25/9/17}
I have no confidence in yesterdays solution anymore.

Let stop calling it $B$ and instead call it $K$, the image of $\kappa\of \prod_{j\neq b}\set{i\of\dom(\beta)|\beta(i)=j} \to S\tuplet{\beta,b}$. I think we need a sequence of points $k_0,k_1,\dots \of K$ and only add a face $f\of U_{\beta(a)}$ if it contains an initial segment of this sequence. Furthermore, $f-{k_n}$--which is $f$ minus the point $k$--is a member of $\bigcup_{i\neq a} V_i$ for all $n$ except the greatest $n$ for which $k_n$ is in the image of $f$.

If $f\of U_j$ for $j\neq b$ and $j\neq\beta(a)$ we should not include is. Somehow the sequence $k_n$ can help to determine this. 
If know that if $f\of (U_{\beta(a)} - \bigcup_{i\neq a} V_i$)
and $f - \kappa\tuplet{j_0,\dotsc,j_n}\of \bigcup_{i\neq a} V_i$,
then $f - \kappa\tuplet{j_0,\dotsc,j_n}\of \bigcup_{n\neq a} V_{j_n}$.
The reason is that $\kappa\tuplet{j_0,\dotsc,j_n}\of V_j$ for $j\not\of\set{j_n}$ and hence $f$ would be too, against the first assumption.

I keep changing my mind about what will work here. I suppose the worst case scenario requires the maximum number of points in $K$ to work. Any face of $K$ that has the same dimension as the nerve.
On the other hand, we seem to reduce the number of possibilities of $f$ quite significantly in the first step, which gives me the feeling that far fewer points can give us what we need.


It seems like $f-K$ determines if $f$ is part of $U_j$. Since $\bigcap_{\beta(i) = j} V_i \subseteq U_j$ we want to use the $k$ to establish this. Take the smallest fibre of $\beta$ and pick $k_n$ such that each forces one of the $V_i$. Each $k\of K$ allows $f$ to escape, however.

Each $k\of K$ limits $f-K$ to a disjunction of $\#\cod\beta - 2$ of $V_i$. Each step gives and intersection that due to the distributive law only gets bigger. I see the number of members only growing along the way. But we strike out the intersections that contain all members of a fibre, because $f$ is not allowed to hide in those intersections. That is ultimately why a maximal solution does succeed. 

\section{24/9/17}

The cause of our problems is that the $V_i\cap U_{\beta(a)}$ don't have a single point in common. Pick a point $p$ in $B$ and is basically tells you it won't be present in any of the $V_{p_i}$.
For $U_j$ where $j\neq \beta(a)$ and $j\neq b$, the point $a$ serves this purpose, but $a$ is not in $U_{\beta(a)}$.

The is a problem with $f$ where $f\circ d_k$ is in $V_i$ while $f$ is not should probably be glued in from some top edge inside $V_i$. 

If we start with a single $p\of B$ are top edge, we run into the problem where $f - p\of V_i$ for some $i$. The nerve $V_i$ unhelpfully supplies a face that we don't want to be there.
These $f$ need to be glued in around a different top edge, which also is in $V_i$.

We know that $f$ should contain $p = \bot_B$, but we need to make an extra demand, like if $f-p\in V_i$. Note that there may be more $i$ where this happens.
To make sure that we can add these faces, we need to make a new demand on $f$. I suppose it should have a specific alternative point which we will use to glue in this face.
The best would revolve around the least $i$ that does not occur in $f$
other than in $p$. 

So the options are $f$ has $a$, $f$ has $p$ and all $p_k$, $f$ has $p$ and $p[k]+$ for the least $k$ such that $f$ doesn't hit $p_k$.

Complicated but doable.

Either $f$ can be extended with $a$ or for all $y\of \cod(\beta)-\set{\beta(a),b}$ there is an $x\of \dom(f)$ such that $s\tuplet{\beta,b}(f(x)) = y$--$f$ is surjective on this subject. We can then compute an alternative top edge $t(f)$ and demand that $f$ hits both $t(f)$ and the least point $p$ of $B$.

Reducing the number of values that $t(f)$ can have is probably a good idea. Perhaps we can limit it to the top point of $B$.
Sounds good.

So two options: $f$ contains $a$, $f$ contains the extremes of $B$ and the rest cases.

Generally, we would like a decidable property that neatly splits $f$ in two classes, closed under taking sub-faces that determines which point we will need for gluing.

No, it is either $\bot_B$ and all of its members, or $\bot_B$ and $\top_B$. If $f-\bot_B\of V_i$, then we use $\top_B$, which therefore must be hit in the image of $f$.

That is all.

\paragraph{2-point-solution ?}
Seeing this makes me wonder if we ever need more than 2 points in $B$. 

So $S(\xi\of[m]\to[n])  = s(\xi)\of[m + 2]\to [n]$. This doesn't do descend properly, as is changes $\xi$ that must be preserved in pullbacks. I don't believe we can fix this in a way that leaves a functor and that matters for how $V_i$ are mapped, implying potential disaster.

\section{23/9/17}
Let's put in some extra time. For each face $f\of U_{\beta(a)}-(\bigcup_{i\neq a}V_i)$ there is a set of points in $B$ there we might use as supporting points for gluing $f$ in. Technically we can use any point of $B$ to do the actual gluing, but there seems to be a problem.

The difficult cases are quite restricted actually:
\begin{align*}
&\forall x. s\tuplet{\beta,b}(f(x))\neq \beta(a)\\
&\forall j\of\cod(\beta) - \set{b,\beta(a)}.\exists x.s\tuplet{\beta,b}(f(x)) = j\\
&\forall i\of\dom(\beta) - \set a.\exists x.f(x) = \lambda(i) \vee \exists y.f(x) = \kappa(y) \land y(\beta(i)) = i
\end{align*}

Exclusion based on missing certain points still feels like a good idea. We will be punching holes in $f$ and demand that all resulting subfaces are included at an earlier stage safe for one. So at the lower stages we need to exclude $f$ that point. Unfortunately, the top edge shifts around and we need to account for those shifted edges as well.

At this point I am wondering how the old proof could even have worked. There we don't try to force ourselves to fit everything in dimensionally.
Perhaps that will simply never work.

Top selection should not be based on existing points, but on the possibility to add.
So well order $B$--at least the subset where $x(\beta(a)) = a$--and pick the least $p\of B$ such that $f$ can be extended with it.
Perhaps we never run into any restrictions here and glue in faces with a single edge in $B$.
Alternatively, we need to connect some faces to this edge before we can proceed.
That is unlikely to work for all the base cases though.

The conditions above tell us something about the distance between a faces here and the faces included at the start. Perhaps enough to determine the dimensional offset.


\section{22/9/17}
The inclusion that must be an acyclic cofibration is:
\[ \bigcup_{i\neq a,j\neq b}(U_j\cap V_i) \to \bigcup_{j\neq b}U_j\]
The problem face is $U_{\beta(a)}$ because it lack the point $a$. All the $V_j$ contain $a$. The other faces $U_i$ contain it. So in that case we go by dimension to add the faces. Any surprises here?

This clears once thing up: the ordering of $S\tuplet{\beta,b}$. The posets are joined in a way that make it contractible--i.e. that its nerve is a contractible simplicial set. If we take the coproduct $\dom\beta$ and $B = \prod_{i\neq b}\set{j\of\dom\beta|\beta(j)=i}$ we wont get this property. We put $B$ above $b$ in $\cod\beta$ to make sure that pullbacks preserve it. So if we are going to connect $B$, it must be at the same level as $\beta_b = \set{j\of\dom\beta|\beta(j)=b}$. A by-pass would turn the poset in-contractible, so we need to pick place in $\beta_b$ to insert $B$. The canonical places are the top and the bottom.

Now when we seek to fill out $U_j$ for $j\neq b$ and $j\neq \beta(a)$ we
have $a\of V_i\cap U_j$ for $i\neq a$ from which we go up by dimension. 
In these cases, the inclusion $\bigcup_{i\neq a} V_i\cap U_j \to U_j$ is
mostly about $B$: $V_i$ miss points in $B$ that $U_j$ contains. Going up dimension by dimension may be overdoing it, but is far simpler than figuring out which points are missing. So we reduce the case of a monic monotone map $[n + 1]\to U_j$ to the cases where $[n]\to U_j$ all the way down to $a:[0]\to U_j$, all needing to have in common that $a$ is in there. I don't see how we can fail.


Obviously, if $b=\beta(a)$ we are done. Only if $b\neq\beta(a)$ we are left with a troubled face $U_{\beta(a)}$ to glue in. Why troubled? The pieces $U_{\beta(a)}\cap V_j$ for $j\neq a$ are connected, but may not have a single point in common. That is why we introduced the helpers $W$.

We are still considering faces $[n]\to U_{\beta(a)}$. We want to reduce the case $[n + 1]\to U_{\beta(a)}$ to cases where $[n]\to U_{\beta(a)}$, but we need to be more careful this time because of shifting
base points.
Just like we ignore faces that don't contain $a$ in the first example, we should probably ignore faces that don't contain all of $B$ this time.

At this point we indeed keep arguing that some faces are present because
greater faces have been added at an earlier stage, perhaps even as part of filling out $U_j$.

I am working towards an alternative to dimension for $f:[n]\to U_{\beta(a)}$. Take the sum of $f(i)$ where $f(i)$ is not a member $B$ e.g.
This is going put a lot of distance between $f$ while clustering others together. Removing a point generally reduces the sum (unless $f(i) = 0$ unfortunately). 

You know what? Just focus on faces $f:[n]\to \dom(\beta)$ and do a similar trick, i.e. $|f| = n + \sum_{i\of [n]} f(i)$. We
will be looking for a way to add all of $S\tuplet{\beta,b}(f)$ and the
idea is that we can do induction over $|f|$. After all, $f\circ d_i$ all have lower norms. A, but we still need to pick a base point!

Let's not be stingy and just say what we want.
For each $j\of \cod(\beta)$ there is a least $i$ such that $i \geq f(k)$ whenever $\beta(f(k)) = j$. These least $i$ both determine the base point we will use and the stage of
construction at which $S\tuplet{\beta,b}(f)$ can be glued on. We would
like to deal with the fact that we are not starting from $1$ in each fibre of $\beta$, but that might not be a big problem in the proof. We do have to be careful about dimension.

\paragraph{Recap}
Outline of the new descend chapter:
\begin{enumerate}
\item Introduce the descend functor and its left adjoint.
We are dealing with slice categories here and explaining the functor
already involves nerves of posets, presumably. We have to deal with general theories that connect slice categories to categories of elements. Moreover, we lift functors using all structure of $\ambient$ at our convenience.
\item Prove that descend is right inverse to reindexing and prove the preservation of modest fibrations.
Both should follow easily form the definitions.
\item Reduce the problem of preserving fibrations to the problem of showing that a single family of morphisms is acyclic.
The definition of contractible morphism should help here, though we juggle many diagrams to get where we need.
\item Proof that this family of morphism is indeed acyclic.
This is what I am struggling with now.
\end{enumerate}

The basic tactic is to assign each face $[n]\to\bigcup_{j\neq b}U_j$ a turn to be included, in such a way that the turn of $f:[n + 1]\to\bigcup_{j\neq b}U_j$ comes after those of $f\circ d_i:[n + 1]\to\bigcup_{j\neq b}U_j$.

Some general principles for computing terms: 
If $f$ hits $\lambda(a)$, its dimension is its turn.
If $f$ can be extended to a $g$ that contains $\lambda(a)$, its dimension plus 1 is its turn.
The remainder either intersects $B$ or can be extended to extend it. They must be part of $U_{\beta(a)}$ and have a fair number of dimensions to avoid inclusion in $U_j$ for $j\neq \beta(a)$. In fact, $\cod(\beta) - 2$ is the least, considering that $s\tuplet{\beta,b}\circ f$ must hit every point in $\cod(\beta)$ except $\beta(a)$ and $b$.
The rule is similar: hitting a number of points in $B$ qualifies $f$ for inclusion at a certain stage. Fewer points means $f$ will only be included indirectly. Since $V_j$ don't contain all of $B$ only working with simplices to contain all of $B$ may not work however.

The old approach put all members of $B$ in order and demanded that a downset be included in the construction. We threw out this demand. What does that do to the stages?

The least thing we can demand of $f$ is that it includes all its support points. For each monic $m\of[\cod(\beta) - 2]\to [\dom(f)]$ such that $s\tuplet{\beta,b}\circ m = d_{\beta(\alpha), b}$ there is a point $x\of B$ such that $x_m(i) = f(m(i))$, $x_m(\beta(a)) = a$. We demand the inclusion of these in the image of $f$. This determines the inclusion stage.
This leaves us without a obvious pivot however.

We could add a combination of two demands. Firstly, there is a point $x\of B$ such that $f$ contains all points $y\of B$ such that $y\leq x$.
Secondly, $f(i) \leq x_{s(\beta,b)(f(i))}$. We still use dimensions to stage these, seeing as the number of point necessary bumps up the dimension of $f$ quite a lot. But can we glue this one in now?
 
\paragraph{reviewing the old proof}
Without the total ordering of $B$, there are a lot more morphisms to take in account there. If we follow the same tactics as before we simply demand that $f$ hits all points of $B$, however.
Now the rule for this family of morphisms is that $f$ comes after $g$ if $f\geq g$. So that is something to bump the stage up for.

Let's review: a face $f\of [n]\to U_{\beta(a)}$ cannot be extended to contain $a$. We therefore need to glue it, using its faces of codimension 1. The morphism $f$ has at least one pivot point to work with. Trading points with $a$ suggests a minimum of dimension plus 2-- --but would that work for points of $B$ that $f$ hits?
For each point that $f$ hits in $B$, first remove that point. That becomes a new target. We get the same analysis: outside of $B$ we can switch points with $a$ to get them at a stage of minimally dimension plus 2 and adding the dimensional we already have, the stages becomes plus 3. Hence the general rule seems to add at least the number of points in $B$ that $f$ hits to the dimension, but they do this themselves don't they? Dimension plus 2 seems sufficient.

I now get something like this. A face $f\of [n] \to \bigcup_{j\neq b}U_j$ belongs to stage $n$ if $f(i) = a$ for some $i\of [n]$. It belong to stage $n + 1$, if $(f \leftarrow a)$ is a function $[n + 1] \to \bigcup_{j\neq b}U_j$. Here:
\begin{align*}
(f \mathop\leftarrow a) (i) &= f(i) \textrm{ if } f(i) < a\\
(f \mathop\leftarrow a) (i) &= a \textrm{ if } f(i) > a, f(i - 1) < a \\
(f \mathop\leftarrow a) (i) &= f(i - 1) \textrm{ if } f(i - 1) > a
\end{align*}
Finally it belongs to stage $n + 2$ if $(f \leftarrow a)$ isn't a member of $\bigcup_{j\neq b}U_j$.

The stages are subsets $A_i$ of $\bigcup_{j\neq b}U_j$ and supersets of $\bigcup_{i\neq a,j\neq b}(U_j\cap V_i)$ defined as unions of various stages according to the classification just made. We show that $A_0 = \bigcup_{i\neq a,j\neq b}(U_j\cap V_i)$ that $A_u = \bigcup_{j\neq b}U_j$ for some $u\geq\#S\tuplet{\beta,b}+2$. Finally the real issue: is $A_n \to A_{n+1}$ an acyclic cofibration?

We have a good idea of what the new functions are. 
\begin{itemize}
\item For the faces $f$ where $f(i) = a$, all $f\circ d_j$ where $j\neq i$ are of stage $n - 1$.
\item For the faces $f$, if $f \mathord\leftarrow a$ belong to the result, then $f\mathord\leftarrow a$ belongs to the same stage.
\item For the faces that cannot be extended $f\circ d_j$ presumably have only two sorts: those that are extensible and which therefore life at stage $n$ by the preceding argument and those which aren't by the induction argument. It doesn't look like we need to be picky with the top edge, pivot etc. anymore.
\end{itemize}

I am missing something crucially important:
It is possible to find too many restrictions at a lower stage!
Precisely one \emph{must} be missing! The first two types of faces shouldn't be a problem because of the $V_j$.
The third type is trouble, however. The reason we don't need to be picky
is the reason why it won't work.

First make another distinction, between those $f$ that already intersect $B$ and those that don't. Those that don't will only be added as part of a face that does at the same stage. For the $f$ that intersect $B$ we presumably pick one of the intersection points as pivot.
We need to pick the top edge that puts $f$ in one way or another. The face of $f$ that lacks edge must have the same stage and not appear at a low stage.

The old solution was to restrict the points outside of $B$, while including all points inside of $B$. The lexicographical ordering does some strange things here.

Be specific:
\begin{itemize} 
\item Only the intersection $f \cap \lambda\of [m]$ determines what the top edge will be.
\item If $f$ does not contain this top edge, then it will only be added as part of the extension with that top edge, which should always be possible.
\item For pivots other than $a$ we need an offset from the dimension. I have a pretty good idea what it should be, but I need to think about this.
\end{itemize}
Removing point of $f$ inside $B$ either results in removing the top edge and we are safe from this now. Otherwise nothing important happens. So move on to removing points outside of $f$. This could change the proper top edge. That means that alternative top edges need to go first.

The number of edges I would connect to $f$ is:
$\prod_{j\neq b, j\neq \alpha(b)}\set{i|s\tuplet{\beta,b}(f(i)) = j}$
This is big enough to be the proper dimensional offset.
The canonical choice of pivot is also determined by this product as well: $a$ if the product is empty, the greatest element of the product with $a$ inserted at index $\beta(a)$ otherwise.

I see a proof. I am unsure whether a simpler construction would not suffice, but I have something workable now.

We have three factors that determine that stage:
\begin{itemize}
\item fundamentally dimension.
\item the number of possible top edges in $B$
\item whether the face already contains the chosen top edge, or need to be extended to include it.
\end{itemize}
The last bit is still a puzzler. I think we are safe because counting the number of possible edges in $B$ gives enough room to add all of them if needed. If we subtract the points that $f$ already hits, however, I get the feeling that we are getting the timing perfectly right.

\paragraph{final thoughts}
Perhaps it could be much simpler: glue in the faces according to dimension, just leave out the ones that could get in the way later. With a top edge selection strategy we can actually predict which faces might get in the way later (the ones missing the selected top edge). I have some doubts that this will actually do it for $B$ however.

Suppose $f$ cannot be extended to $a$. We want to make sure removing the top edge result in something not already included in the structure. 
Now we pick a point different from the top edge. How can we be sure that one is included? If the top edge of the less dimension thing is the same, no problem. If the top edge of the less dimensional thing is different, problem. The subface was not included at its stage unless its edge was is part of the current face.

Perhaps we have been too selective: just demand that a face is connected to a shared subset of the leaves. That means $B\cup\set{a}$. In other words, any point of either $a$ or $B$ will do. For many faces the argument that it was glued on relies on extending the face with suitable points. In other cases the intersection proves enough. A, but here we run into the opposite problem: we remove a top edge and find that the sub face was already included. Hence, the inclusion no longer acyclic.

Yet another idea: if $B$ is nonempty, just pick an point and use that one for all faces. At each stage, we just glue in the faces that have this point in it. How could that fail? The base cases might cause trouble now. I think I need Lumsdaine's counterexample to show why that won't work.

\section{9/9/17}
We use the posets $S\tuplet{\beta,b}$ and sub-posets to explain the construction. There are some bigger step we can take: a handful of 'faces' sharing a common vertex, included into a bigger face is an acyclic cofibration. The second stage generalizes form a single vertex to a collection of connected vertices. This way we can both prove descent, but also pushout products.

I think we generally need a strategy to deal with the collection of connected vertices. That prevents useful generalizations.

\section{8/9/17}

\paragraph{Recap}
We wind up with tuplets of five elements in $D\otimes \simplex_P$.
\begin{enumerate}
\item a morphism $\alpha$ that implements a category action.
\item a number $a\of\cod(\alpha)$, which tell us which horn we are trying to preserve.
\item a morphism $\beta$ with $\dom(\beta) = \cod(\alpha)$, which tell us about the target simplex. This hold the most data.
\item a number $b\of \cod(\beta)$ declaring which horn we want to pull back along.
\item a morphism $\sigma$ into the partially ordered object $S\tuplet{\beta\circ \alpha,b}$, which similarly to $\alpha$ is a target for the category action.
\end{enumerate}
The equivalence relation tells us that:
\begin{align*}
\tuplet{\alpha\circ\phi,a,\beta,b,\sigma}&\sim
\tuplet{\alpha,a,\beta,b,s(\phi)\circ\sigma}\\
\tuplet{\alpha\,a,\beta,b,\sigma}&\sim
\tuplet{\id,a,\beta,b,s(\alpha)\circ\sigma}\\
\end{align*}
This reduces the number of elements to deal with to four.

So what makes this a simplicial object again? 
\begin{align*}
\dim\tuplet{\alpha,a,\beta,b,\sigma} &= \dom(\sigma)\\
\tuplet{\alpha,a,\beta,b,\sigma}\cdot\phi &= \tuplet{\alpha,a,\beta,b,\sigma\circ \phi}
\end{align*}

So that is what $D\otimes h$ looks like. Let's try to show that it is an acyclic cofibration.

\paragraph{The problem}
The codomain consists of those $\tuplet{a,\beta,b,\sigma}$ where $s\tuplet{\beta,b}\circ\sigma$ misses a point in $[\cod(\beta)]-\set b$.

The domain consists of those $\tuplet{a,\beta,b,\sigma}$ in the domain where $\sigma$ misses a point in $[\dom(\alpha)] -\set a$. This means that that point neither appears directly or as part of a tuplet in $s(\alpha,b)$. Note $\cod(\alpha) = \dom(\beta)$.

That is the analysis. Showing that this is a cofibration should be relatively straightforward. We already explained how to decide that an
is part of the domain and faces only stand out for being injective.

To show that the morphism is an acyclic cofibration, we divide the
codomain in stages, each of which can be shown to be pushouts of sums
of cofibrations. Here the pain starts.
\begin{itemize}
\item Stage zero is the domain. 
\item The next few stages add all faces that contain $a$. Sometimes this requires several steps of adding faces, going up the dimensions one-by-one. In other words, $\beta$ determines how many stages are needed.
\item The last few stages deal with cases where we are forced to work around $a$. Instead we use the tuplets in $S\tuplet{\beta,b}$ as points to work with.
Think subsets of $S\tuplet{\beta,b}$. In fact that is what we replace the old faces with: subsets of this poset.
\end{itemize}

Perhaps tracking with more general posets and using mostly dimension to glue in new faces, is better way to make the construction understood.

\begin{align*}
U_i &= \set{x\of S\tuplet{\beta,b} | s\tuplet{\beta,b}(x) \neq i } \\
V_j &= \set{\lambda(x)\of S\tuplet{\beta,b} | x \neq j }\cup\set{\kappa(x)\of S\tuplet{\beta,b}| \forall k\of(\dom(\beta)-\set b). x_k\neq j } \\
W_{\kappa(p)} &= \set{\lambda(x)\of S\tuplet{\beta,b} | \beta(x) = b \vee x \leq p_{\beta(x)} }\cup\set{\kappa(x)\of S\tuplet{\beta,b}} \\
\end{align*}

The change now is that these aren't totally ordered sets. The starting point is the $\bigcup(U_i\cap V_j)$. The goal is $\bigcup(U_i)$. We start with gluing in all faces that contain the point $a$. Then we switch to the $\kappa(p)$ points if necessary.

\section{25/8/17}
What if the lexicographical product isn't a functor?
$\tuplet{0,1} < \tuplet{1,0}$
Suppose $\phi\of[1]\to[1]$ satisfies $\phi(x)=0$.
Since $\tuplet{\phi,\id}\tuplet{0,1}=\tuplet{0,1}>\tuplet{0,0} = \tuplet{\phi,\id}\tuplet{1,0}$.

Is this a problem for my construction?
\begin{itemize}
\item The functor $K$ of $\simCat$ would have to cover sufficiently many different cases to suffer from this problem.
\item A big part of the argument is an adjunction of functors at the slice category level.
\item The actual construction of the filler relies on the lexicographical
order.
\end{itemize}

What can we do now?
Take another route to $K_!$ and hopefully $K^*$ that doesn't go through $\simCat/[n]$.
There may be advantages to that.
Horns live in the categories of simplices, not in the slice category. That caused some awkwardness with having to prove that $K_!$ preserves intersections.
The lexicographical product is involved in the construction of the fillers, but it may not be that important.

\paragraph{back to the drawing board}
We replace $\xi\of\simplex[m]\to\simplex[n]$ with a \emph{space} that makes the simplices robust for pulling back along the horn. This is done
by adding supporting vertices for the simplices that would be cut out.

What is this space like?

The simplicial object $S\tuplet{\xi,k}\to\simplex[\cod(\xi)]$ confusingly must still consist of
pairs ${\phi,x}$ where $\phi$ is a morphism $[n]\to[\cod(\xi)]$. The $k'$ add room for elements that are at the same height.

We know that $S\tuplet{\delta^k,k} = \id$. No choice in that\dots
Lets probe: if $\xi'$ hits $k$, its companion should be able to pick one of the new edges there. Like $\phi_k\to \prod_{i\neq k} \xi_i$.

I know how many vertices I need. I know that the need to be above vertex $k$. I am unsure about the rest however.

The functorial setup was too restrictive, so while the number of edges is correct, we have to permit more higher dimensional simplicial sets.
I there are two obvious choices:
\begin{itemize}
\item allow every possible ordering of remaining egdes.
\item take the partial ordering that arises naturally.
\end{itemize}
The latter is more restrictive to let's stick with that one for now.

The ordering of $\xi_k + \product_{i\neq k}\xi_i$ is relevant as well.
We now allow simplices to jump from one set to the other in a specific order, which mean we glue the new faces to existing simplices above $k$.
Let's stick with adding the new faces in a specific place in the existing ordering.

\mathbfdef{supp}
We introduce a new partially ordered set $S\tuplet{\xi,k} = (s,\leq)$ where
\begin{align*}
s &= \dom(\xi) + \prod_{i\neq k} \xi_i\\
\supp(\lambda(x)) &= \xi(x) \\
\supp(\kappa(x)) &= k\\
\lambda(x) \leq \lambda(y) &\iff x\leq y \\
\kappa(x) \leq \kappa(y) &\iff x_i\leq y_i (\forall i\neq k)\\
\lambda(x)\leq \kappa(y) &\iff \xi(x) \leq k \\
\kappa(x) \leq \lambda(y) &\iff k < \xi(x)
\end{align*}

For $\phi:\xi\to \xi'$ the function $\phi\of S\tuplet{\xi,k} \to S\tuplet{\xi,k}$ we now let
\begin{align*} S\phi(\lambda(x)) &= \lambda(\phi(x)) & S\phi(\kappa(x)) = \kappa(\vec\phi(x)) \end{align*}
That way we indeed get a morphism of partially ordered sets.

Now the simplicial set we aim at is the \emph{nerve} of this partially ordered set.


\paragraph{back in the game?}

The left adjoint would be another tensor product divided by an equivalence relation. Perhaps we can even construct it in one go.
It kind of looks like using the nerves eliminates a lot of waste, meaning that we no long need the equivalence relations.

The descend functor should then be simpler as well. For $f\of X\to\horn_k[n]$
\[ \prod_\xi(\supp \backslash \xi \to X_\xi) \]
With the usual naturality constraint.

I got the feeling I am missing something.

Each $S\tuplet{\xi,k}$ is one representable, so the left adjoint
is forces to take every one of these in account.
It looks more like: 
\begin{align*}
\base(D\ri(f)) &= \set{ \tuplet{x,s} | x\of\dom(f),s \of \nu(S(f(x)))}/{\mathord\sim}\\
\textrm{where } & \tuplet{x\cdot\phi,s} \sim \tuplet{x,\nu(S(\phi))(s)}
\end{align*}
Here $\nu$ stands for the nerve that adds many additional morphisms.

The right adjoint consists of natural transformations form this nerve.

This is nothing new. Ordinarily we'd take a functor $\simCat_{\set\geq}\to\ambient\s/\horn_{\set\geq}$ and spin of the adjunctions. Circumstances don't let this be a functor, however.

Profunctor like structures do it, but they must be internalized in
$\ambient$. That means we take $\horn_\leq$ and $\simplex_\leq$ and make
a bundle of sorts over them.

Suppose we re-imagine this as a morphism $K\to \base(\horn_{\set\geq}\times\simplex_{\set\geq})$ with lots of extra structure. This is where the nerve comes in.

That profunctor would look like this:
\begin{align*}
D &= \set{\tuplet{\beta,b,\sigma}|
\beta\of\Ar(\simCat),
b\of \cod(\beta),
s\tuplet{\beta,b}\circ \sigma\of \base(\horn_b)}\\
d_0(\tuplet{\sigma,\beta,b})&=\tuplet{s\tuplet{\beta,b}\circ\sigma,b}\\
d_1(\tuplet{\sigma,\beta,b})&=\tuplet{\beta,b}\\
\delta\cdot\tuplet{\sigma,\beta,b}&=
\tuplet{s(\delta)\circ\sigma,\beta\circ\delta,b}\\
\tuplet{\sigma,\beta,b}\cdot\gamma&=
\tuplet{\sigma\circ \gamma,\beta,b}
\end{align*}
In here, all the $s$'s are connected to the partially ordered sets above.
I am having great trouble getting this one right.

\newcommand\To{\mathbin\Rightarrow}
The descend functor applied to $f\of X\to \horn_{\set\geq}$ is 
$(D\To f)\of (D\To X) \to \simplex_{\set\geq}$.
\begin{align*}
\base(D\To X) &= \set{\tuplet{x,y}|
x\of D_y \to \base(X),
f\circ x = d_0,
\forall y,\phi.x(y)\cdot\phi = x(y\cdot \phi)}\\
& \textrm{where }D_y = \set{x\of D|d_1(x)=y}\\
(D\To f)\tuplet{x,y} &= y\\
\tuplet{x,y}\cdot\phi &= \tuplet{\lambda z.x(\phi\cdot z),y\circ\phi}
\end{align*}
The arrow mapping is relatively straight forward:
\[ (D\to m)\tuplet{x,y} = \tuplet{m\circ x, y} \]


Now that we have hidden the complexity of the nerve, this looks surprisingly simple.

The left adjoint for $f\of X\to \simplex_{\set\geq}$ is $D\otimes f \of D\otimes X \to \horn_{\set\geq}$.
\begin{align*}
\base(D\otimes X) &= \set{\tuplet{x,d}\of \base(X\times D)|f(x)=d_1(d)}/\sim\\
& \textrm{where }\tuplet{x\cdot\phi,d}\sim\tuplet{x,\phi\cdot d}\\
(D\otimes f)\tuplet{x,d} &= f(x)=d_1(d)\\
\tuplet{x,d}\cdot\phi &\sim \tuplet{x,d\cdot \phi}
\end{align*}
Now the arrow mapping satisfies:
\[ (D\otimes m)\tuplet{x,d} \sim \tuplet{m\circ x,d} \]
That $m$ is a morphism makes this work.


If I have done this right, this should be an adjunction. Moreover, it should be evident that the construction preserves modest sets, at least if finite object are modest.

\paragraph{The actual descent}
We can not simply work with 'an' acyclic cofibration. We need to take the family of all cofibrations is account. This may get confusing
We only find the family of horns in $\ambient\s/\set\geq\disc$. The functor $D\otimes$ lives on $\ambient\s/\simplex_{\set\geq}$. 
The problem object $P$ satisfies \[P = \set{\tuplet{\xi,k,l}|\xi\of\Ar(\simCat),k\of[\dom(\xi)],l\of[\cod(\xi)] }\] 
All we need to add to $P$ to get the family of all horn inclusions in the slice $\ambient\s/\simplex_{\set\geq}$ is $\simCat$ morphisms $\phi\to \dom\xi$.

A clearer definition:
\begin{align*}
\base(\simplex_P) &= \set{\tuplet{\alpha,a,\beta,b}| 
\alpha,\beta\of\Ar(\simCat),\cod(\alpha)=\dom(\beta),
a\of\cod(\alpha),b\of\cod(\beta)}\\
\base(\horn_P) &= \set{\tuplet{\alpha,a,\beta,b}\of \base(\simplex_P)|\alpha\of\base(\horn_a[\cod(\alpha)])}\\
\supp\tuplet{\alpha,a,\beta,b} &= \tuplet{\beta\circ \alpha,b}\\
\tuplet{\alpha,a,\beta,b}\cdot\phi &= \tuplet{\alpha\circ \phi,a,\beta,b}
\end{align*}

This provide two object and an inclusion in the slide category, to which we apply functor $D\otimes-$ above. And then we prove that the result is a discrete family of acyclic cofibrations.

We wind up with tuplets of five elements in $D\otimes \simplex_P$.
\begin{enumerate}
\item a morphism $\alpha$ that implements a category action.
\item a number $a\of\cod(\alpha)$, which tell us which horn we are trying to preserve.
\item a morphism $\beta$ with $\dom(\beta) = \cod(\alpha)$, which tell us about the target simplex. This hold the most data.
\item a number $b\of \cod(\beta)$ declaring which horn we want to pull back along.
\item a morphism $\sigma$ into the partially ordered object $S\tuplet{\beta\circ \alpha,b}$, which similarly to $\alpha$ is a target for the category action.
\end{enumerate}
The equivalence relation tells us that:
\begin{align*}
\tuplet{\alpha\circ\phi,a,\beta,b,\sigma}&\sim
\tuplet{\alpha,a,\beta,b,s(\phi)\circ\sigma}\\
\end{align*}
Note that $\alpha=\id$ is not (always) an option, though, because it isn't part of the horn.

So that is what $D\otimes h$ looks like. Good luck showing that it is an acyclic cofibration.

\section{11/8/17}
The biggest problem is the adjunction between $D$ and $K$ on $\ambient\s/\simplex_{\set\geq}$, methinks.
Perhaps the problem set is technically bigger, but conceptually, all we need there is a good story about \emph{powers} or \emph{tensors} and \emph{cotensors}.

We have a solid description of the representables of $\ambient\s/\simplex_{\set\geq}$, i.e. pairs $\tuplet{\xi\of\Ar(\simCat),k\of \cod(\xi)}$ with morphisms between the domains. It is a coproduct of categories, but vitally a indexed coproduct $\ambient$. Lets call this category $\cat P$ for now.

Proving generic statements is the right way to go. What works in the practice of computer programming, will work in the practice of theorem proving.

The have a functor $P\of \cat P\to\cat P$ with preserves intersections. This functor of representable induces an endo-adjunction of $\ambient\s/\simplex_{\set\leq}$, consisting for the covered functors $K\dashv D$. Of these $D$ is supposed to be the simplest, so let's start with $K$!

For an object $f\of X \to \simplex_{\set\geq}$ we seek an object $Kf\of KX\to \set \simplex_{\set\geq}$. We know that there won't be a direct construction, but that we first make two other object maps $K_1f$ and $K_2f$ and a pair of natural transformations $K_2f\to K_1f$ for which $Kf$ will be the coequalizer.

About $K_1f$: here $f$ produces $\tuplet{\xi,k}$, the underlying object. There is another bundle $b_1\of B_1\to \simplex_{\set\geq}$ where 
\begin{align*}
\base B_1 &= \set{\tuplet{\beta,\xi,k}| \cod(\beta) = \norm{\xi ,k} }\\
\dim(\tuplet{\beta,\xi,k}) &= \dom(\xi) \\
\tuplet{\beta,\xi,k}\cdot\phi &= \tuplet{K_1(\phi)\circ \beta \phi,\xi\circ \phi,k} \\
b_1(\tuplet{\beta,\xi,k}) &= \tuplet{\xi,k}
\end{align*}
Pulling back along $f$ generates the $K_1f$ object, but the structure is all wrong.

This would be amazing: an object $B$ such that $D = \cdot^B$ and $K =B \times \cdot$.
It won't work out that way because the structures are wrong. We might get a span of morphisms $c,d\of B\to \simplex_{\set\geq}$\dots
Surely it can't be proper morphisms though? What I have trouble with is the idea that we might be able to find a span of morphisms of simplices,
such that $K$ and $D$ are the result of pullbacks and pushouts along those morphisms. The changes in dimension are the clearest problem.
There must be two different simplicial structures on the same object to overcome that. 

The $K_2f$ is a more complicated variant, supposed to capture pairs of equivalent elements. Pairs of commutative triangles sharing a domain. Both embellished with an element of $f$ that becomes equal after restriction. This is supposed to tell us which members of $f\ri(B_1)$ to equate.

Forgetting structure is the goal. We know that $f$ can be represented as a coequalizer of coproducts of representables and its morphisms as well.
For this we might introduce the 'co-yoneda lemma' or something. Simpler yet: presumably we are dealing with internal projectives and coverings by those.
Now we get to a higher level of clarity and completely loose track of the rest.

\paragraph{looking at simplicial sets differently}
The coequalizer of coproduct of representables suggests that all of our categories are exact completions of some sort, depending on how easily we can represent morphisms.

I thought I worked this out before. We look at $\ambient/\nno$ and then a monad on this category to get the option of sending a simplex to a degenerate simplex. The simplicial sets are algebras for the monad, while we are now looking at the Kleisli category and hence the 'free objects' in a sense among the simplicial objects. I think these free object a projective in an enriched sense, i.e. the enrichment in ambient is regular in the covariant variable, if the contravariant is free. Yet it is possible to represent all objects as pseudoequivalence relations of free objects and all morphisms as morphisms of the pseudoequivalence relations, by finding a particularly full covering (perhaps we are dealing with a 'resolvent embedding').

We can define the functor $K$ on the free objects, show that it preserves equivalence relations and use that to define the functor for all simplicial objects.
We still have nothing on $D$.

Precise generic statements.

\paragraph{back to $D$}
The construction of $D$ ought to be simpler, because a simplicial object is like a functor and we just compose functors.
The representation we use is a complication, but only slightly so, I think.

Keep in mind that we combined to constructions to shorten the text. There is a perfectly ordinary adjunction giving by reindexing and its right adjoint, which unfortunately does not preserve model structures. We modify the model structure on one side and give adjoint endofunctors to connect the models structures.

Our presheaves are algebras for a monad in a slice of $\ambient$. The monad is similar to the monad belonging to a monoid action, but since the action doesn't preserve dimension, the action is invisible.

If we return to the presheaves over the full simplex, it look like we are just pulling back along a morphism of underlying objects, which is why $K$ must be like composing with the same morphism. In either case we need to do something about the lost monadic structure.

That is a good way to look at it\dots

Objects of $\ambient\s/\simplex_{\set\leq}$ are algebras for a monad on $\ambient/P$. There is a morphism $k\of P\to P$ and we define the functor $D$ be pulling back along this morphism. So what happens to the algebra structure then? There is a specific mapping:
\[ K_1\of \set{ \tuplet{\xi,k,\phi} | \cod(\phi)=\dim\tuplet{\xi,k} } \to \set{ \tuplet{\xi,k,\phi} | \cod(\phi) = \dim(K_0\tuplet{\xi,k}) } \]
With it help, we can show that the pullbacks have the same algebra structure.

The other direction is harder, because composing with $k$ doesn't preserve the algebra structure. However, we should be able to work with a quotient of the free algebra. Start with $f\of X\to P$:
\[ M(k\circ f) = \set{\tuplet{x,\phi}|\cod(\phi) = \norm{ f(x) }}\]
Now $\tuplet{x\cdot\phi,\chi} \sim \tuplet{x,K_1(\phi)\circ \chi}$. The structure of ambient is sufficient to provide a quotient $M(k\circ f)/\sim$ and morphisms factors nicely through these quotients, providing the sought after functor $K$.

Viewing slices of $\ambient$ as categories of algebras for various closely related looks smart. Maybe something to work into previous chapters of the paper.

For the adjunction, this is even better. The unit $g \to DKg$ is $\function y \tuplet{y,\id}$. It is probably an isomorphism.
The counit $KDf \to f$ is $\function{\tuplet{x,\phi}} x\cdot\phi$. Does that make sense?

The construction relies on a kind of factorization of $k\circ g$ through a morphism $Kg\of KY \to P$, where $KY$ is a suitable quotient of the free algebra.
$Df$ is simply a pullback. $Kg$ is the initial algebra through which $k\circ g$ factors. Clearly $g$ factors through $DKg$ due to the property of pullbacks and $KDf$ through $f$ through initiality. Isomorphism $g\to DKg$ is equivalent to $K$ being fully faithful, which may help\dots Big factor is $k\of P\to P$ being monomorphic. Initiality is needed as well. For initiality $(Kg,Kh)\simeq (k\circ g,Kh)$, but $(k\circ g,Kh)\simeq (g,h)$ because $k$ is monic?

Why do I want $DKg\simeq g$ anyway? I want $h\ri(D(h_*f))\simeq f$. The morphism $k$ being an endomorphism of $h$ takes care of this.

\paragraph{Wider perspective}
The right adjoint allows us to descend morphisms along the family of horn inclusions.
It 'descends' in the sense that the right adjoint is right inverse to the reindexing functor.
To show that it preserves fibrations, we show that the left adjoint preserves cofibrations.

The further power/cotensor stuff is a way to proof this for all families of modest objects over all horns at once.
The extra parameter does little other than witness that everything what we do is generic. Make that two extra parameters,
because we also have to consider all possible lifting problems.

On the other hand, we already have the parameter of the horn we descend along, giving a grand total of three parameters.

So bring that down to one generic one $\norm:P\to \nno$, to start with.
This is enough. We can define the simplicial set, the monad and the adjunction.
No, don't go to general simplicial sets, stick to these 'projectives'.
Also consider that $k\of P\to P$ is a functor, but absolutely no morphism of simplicial sets.

This is good enough.
\begin{enumerate}
\item The first parameter is that of horns $H\to \nno$. This we need for defining our functor $k$.
\item The second parameter is that of lifting problems $L\to H\to \nno$. Not more complex, but for each pair of horns and each morphism of the codomains, we need a point to show preservation.
\item The third parameter is modest families $M\to H$. There is an object of modest families over horns. everything we have proved so far holds for this family. Importantly, closure under products suggest that modest sets survive descend.
\end{enumerate}
The third and second parameters have no direct relation. This is something to be wary of.

I don't feel like I have the perspective I need yet.

There is a nasty mismatch somewhere. The set $P$ may be our object of problems, but it isn't the underlying object of $\simplex_P$.
This confuses. 

Above, we are talking about simplicial objects. A simplicial object induces a category of elements. The morphisms are copied from $\simCat$. We define a functor $F$ and derive functors between the slice categories.
We can do this with any simplicial set and any functor of the elements. The slice categories have the benefit of a subtle form of completeness.

So what do we do exactly?
\begin{enumerate}
\item Show how functors between categories of elements induce adjoint pairs of functors between slice categories.
\item Define for each $p:P\to H$ such a $\simplex_P \to \simplex_P$. Let $L\subseteq H$ stand for the elements of horns, 
then we show that a composed left adjoint does preserve cofibrations.
\item Finally argue that all right adjoints preserve modest sets.
\end{enumerate}

Going from top to bottom:
Slice categories are categories of presheaves over internal categories of ambient and internal functor induce adjoints pairs of functor between slices.
The descend functor is composed of the direct image along the family of horn inclusions and reindexing along a specific endomorphism $k$ of $\simCat_P$. 
It therefore has left adjoint $K$. This left adjoint preserves discrete families of cofibrations, which makes $D$ preserve fibrations. direct images and reindexing both preserve modest families, hence $D$ does too.
\section{30/7/17}

There is a family of special fibration that withstand pulling back. The really hard part is connecting the descend to this family.

\paragraph{All problems}
The object of all problems is 
\begin{align*} 
P &= \set{\tuplet{\xi,k,l}|\xi\of\Ar(\simCat),k\of\dom(\xi),l\of\cod(\xi)}\\
p\tuplet{\xi,k,l} &= \tuplet{\dom(\xi),k}
\end{align*}
This is the one we want. The $p$ is the one we make the power over. The power is fine but the other object is much harder to do. The basis is still okay:
\[ q\tuplet{\xi,k,l} = \dom(\xi)+\norm\xi_l \]

The representables of $\ambient\s/\set\leq\disc$ are what I used as the key. That will work.

\section{28/7/17}
The global structure changes dramatically.

If $V$ is the universe, the morphism $\ambient\s/\nno\disc(\simplex_{\set\geq},V)\to \ambient\s/\nno\disc(\horn_{\set\geq},V)$ is a split epimorphism. 
The object $P=\ambient\s/\nno\disc(\horn_{\set\geq},V)$ is the object of lifting problems. By descending along $\horn_P\to \simplex_P$ we get where we want.
After we pin down what the descendant looks like, we just need to demonstrate that it is a modest assembly.
Here is where the real pain lies.

Fatten the simplex and then pull back. That is all we need to make things work.

Now the modesty is just in the way. All we really need is a grasp of the problem. 
All combinations.
Somehow just showing that horn inclusions are equivalences.

We make descend adjoint to a construction which is not the same as simply pulling back,
Although it comes close. Could we skip ahead and describe 

Nothing really changes about the structure of the proof.

\section{14/7/17}
Since $\ambient\s$ is sort of like a topos, we can represent its objects as coequalizers between sums of simplices. This representation allows us to extends any functor $K\of \simCat \to \simCat$ to a functor $\ambient\s\to\ambient\s$: the right Kan extension of $Y$ along $YK$ if $Y$ is the Yoneda embedding.
Technically we have a far larger class of lifting problems to address internally. We need a functor $\ambient\s/\simplex_{\set\leq}\to\ambient\s/\horn_{\set\leq}$, which has a right adjoint and which preserves cofibrations.

We can subdivide a little and use the family of horn inclusion to define a model structure first.

\paragraph{recapitulate}
We need a lifting operator for the universe of modest objects. We realize it by descending fibrations along the family of horn inclusions. The descent operator must produce a fibration whose pull back is the original fibration. We turn this into a functor, which has a left adjoint and then prove the left adjoint preserves cofibrations.

Ultimately we bring it down to a single family that is proven to be a family of cofibrations.

The descend construction itself matters very much and must be applicable to all modest fibrations.
Proving that the descended morphisms are fibrations is done by reducing the lifting problems of the descended morphisms to lifting problems of the original morphisms. This is what the left adjoint is useful for. Finally, 


For each $\xi\of [m]\to[n]$, $k\of[m]$ and $l\of[n]$ there is a strengthened cofibration 

\paragraph{strategy}
We want to put the family of horn inclusions central, so let's just rewrite the section that way and see where we get stuck.





\section{30/6/17}
Left to do:
\begin{enumerate}
\item ensure that every proof of cofibrancy satisfies the new definition.
Done.

\item continue the other updates, namely the new family lifting property.
\item restructure the descend proof to be less hand-wavy as well.

\item make the proof that contractible morphisms are acyclic fibrations more readable.
\item surjective or epic in $\simCat$, make up your mind!
Epic is it.
\end{enumerate}


Technically $D\of \ambient\s/\simplex_{\set\leq} \to \ambient\s/\horn_{\set\leq}$.
The reason $D$ preserves cofibrations is that it is a 'partial' left adjoint $K$ that preserves acyclic cofibrations. It is in the wrong place to a 

The functor $D$ is indeed a Kan extension, but of a right adjoint to $K$.
That is how it preserves fibrations.

The problem object combines a morphism $\phi\of\simplex[m]\to\simplex[n]$ with horns at both simplices. Worse still, to prove that it has the lifting property, we need to split things up even further.

There is no Kan extension of $K$ along $\Delta$, but we can do every power and coequalizer.
These would be the enriched projectives and the things they cover.

Since we are working with enriched categories anyway, projective makes sense. The projectives of $\ambient\s$ in this sense and the objects that have a projective resolution permit the extension of $K$.

Projective resolutions of horns: the set of faces of codimension $1$ and a power of those of codimension $2$. Do these help in any way?

In any case, we can do the constructions with these objects,
and since the problem object is in here, we have enough to proof properties of $D$.

\paragraph{density}
Acyclic cofibrations are dense up to homotopy. I now expect no deeper relation between the descend construction of the paper and density or codensity monads than that.

The functor $(K_0,K_1)$ fails to be a monad because of the ordering we force on the supporting points. Without it, the reset of the construction doesn't work. But the ordering arbitrarily chosen to be the lexicographic one prevents a notion of bind.

Moving on: what about $D$? Left Kan extension of $K$ along $D$ anyone?

That makes it clearer why the projective thing would work out.
In that case the elements are 'nice colimits' of simplices, 
that can be replicated on the other side.

\paragraph{new setting}
Coproduct of categories over $\set\leq$. But then, we are considering simplicial object over other simplicial object, so there might be a more direct definition\dots

$D\of \ambient\s/\simplex_{\set\leq} \to \ambient\s/\horn_{\set\leq}$


\paragraph{projectives are cofibrants}
The category of projectives should be equivalent to the category $\cat P$ where objects are pairs $\tuplet{P,p\of P\to\nno}$ of objects and morphisms of $\ambient$ and where a morphism $\tuplet{P,p}\to \tuplet{Q,q}$ is a morphism $f\of P\to \times Q\times \Ar(\simCat)$ such that $f_1(x)\of [p(x)]\to [q(f_0(y))]$, i.e. like a tracked morphism in a sense.
Essentially, families of finite well orderings.

We can cover the family of horn inclusions with these, which is all we need.

Hey, notice something? Our cofibrations are projective morphisms in a suitably modified sense, just as intended. We have described cofibrant objects, which cover everything.

What we need however is the covering by regular epimorphisms, which may differ from that by acyclic fibrations. The 'latching' construction in the factorization proof. I get the feeling that the equivalence relation is already cofibrant. A tuplet $\tuplet{\epsilon_0,y_0,\epsilon_1,y_1}$ where $y_0\cdot\epsilon_0 = y_1\cdot\epsilon_1$, is nondegenerate if $(\epsilon_0,\epsilon_1)\of [a]\to[b]\times[c]$ is monic. Now we have an equivalence relation whose quotient is the original simplex.

I don't trust this. These structures aren't coproducts of simplices, like the projectives I look at before. So something is up.
Coverings with tensors of the family of simplices are everywhere though, so it may not be a great problem.

So $K$ does extends to all of $\ambient\s$. Every object is the quotient of a pseudoequivalence of cofibrant objects. The functor $K$ easily extends to cofibrants and their quotients, hence all of $\ambient$. So $D$ has a proper left adjoint. This left adjoint has to send the family of horn inclusions to cofibrations.



\section{16/6/17}
What is the task that I have been postponing?
\begin{enumerate}
\item update the definition of cofibration once more, to say that the set of complementary faces covers the complement of the image.
\item ensure that every proof of cofibrancy also proves this extra condition.
\item continue the other updates, namely the new family lifting property.
\item prove anew that contractible morphisms are acyclic fibrations.
\item restructure the descend proof to be less hand-wavy as well.
\item epic vs surjective in $\simCat$--make up your mind.
\end{enumerate}

I tend to focus on the link between cofibrations and the saturated class of morphism generated from the family of cycle inclusions.
The recursive lifting constructions are a problem, however.

I keep missing what I really need, but degeneracy should be definite.

Suppose we definite degenerate as follows: $x=y\cdot\epsilon$ for a surjective $\epsilon$ such that $\epsilon\neq\id$.
Can we prove the current positive definition of face?
Suppose $x=x'\cdot\xi$ for some endomorphism $\xi$, but $x$ is nondegenerate. By em-factorization $x = x \cdot m(\xi)\cdot e(\xi)$, but now $\neg\neg(e(\xi)=\id)$, because of nondegeneracy and $e(\xi) = \xi$ because equality between these morphisms is decidable.



\section{11/6/17}
Two approaches make sense. Add the condition that simplices are
generated or define acyclic cofibrations the hard way.
The latter doesn't make much sense.

We can glue in new faces. Therefore the condition that the decided
faces generate everything.

\section{5/6/17}
The lifting operator should be a family of morphism, otherwise
the piece-wise application doesn't make much sense.

Indeed, work with families of morphisms until the last step.

We have filler operators:
\[ f_n\of \hom(K_n,X)\times_{\hom(K_n,Y)}\hom(K_{n+1},Y) \to \hom(K_{n+1},X) \]
We define a new family of fillers using the following equations:
\begin{align*}
g_n &\of \hom(K_0,X)\times_{\hom(K_0,Y)}(\product{m\of\nno}\hom(K_m,Y))\to \hom(K_n,X)\\
g_0(a,b) &= a\\
g_{n+1}(a,b) &= f_n(g_n(a,b),b_{n+1})
\end{align*}
The $b$ must be a family as well and it probably must satisfy certain equations, like $b_0 = p\circ a$ and $b_{n+1}\circ c_n = b_n$.
So that is a factor.
Better yet $b\of K_\infty \to J$, etc.

The last step is a pushout to get to the cofibrations.

Rebuild the contractibles are acyclic proof. In need to reconsider the notation, but that can wait.

\paragraph{confusion}
I took for granted that the set of faces outside of the image of a cofibration is a set of generators, in the sense that each simplex is either part of the domain of the cofibration, or comes form one of the faces. Is it?

If we merely get a decidable subobject of generic simplices, do we get in trouble? Don't we also get the faces then?

Damage assessment:
\begin{enumerate}
\item we prove the decidability of the set of faces in order to show that acyclic fibrations are contractible.
\item the first factorization proof might actually become simpler
with a set of generators
\item the proof in the other direction is our problem now.
\item doesn't seem to come up futher down the road.
\end{enumerate}

So what would be the danger of switching to a decidable subject of generators?
So we loose decidability of genericity\dots do we need that?
Once again the uses are restricted to this section, where we are better of with simple generators!

A decidable set of generators. If we pull back a cofibration with this property, we get a new set of generators, hence no pain at all.

This is good.

I still feel like there is some danger. We cannot simply glue faces in and expect isomorphic results. I am afraid that some cofibrations are not going to be pushouts of powers of the family of cycles.

Why did I define cofibrations differently anyway?

Just adding the assumption that the set of faces outside of the image generates everything else corrects an oversight on my intuitions. It is probably provable that every simplex comes from a face using classical logic, by deriving a contradiction from the assumption that no restriction is nondegenerate.

The problem is equality. In a classical setting $j\cdot \xi = j$ is either true or false. This is a luxury we don't have here, so degeneracy is no decidable. This hurts us more often than expected: when we have a set of generators without the guarantee of non degeneracy, we can never get it back when we need it.

\section{4/6/17}
Let $c\of I\to J$ be a cofibration and let $\phi\of\base J\to\bool$ classify the subject of faces of $J$ that aren't faces of $I$.
Let $K\subseteq \nno\times J$ be the simplicial object that contain $\tuplet{n,j}$ if $\neq\phi(j\cdot\mu)$ for all monic $\mu$ with $\dom(\mu) > n$.
In other words, simplices are only admitted if all of their restrictions are either in $I$, degenerate or of dimension less than $n$.
Let $s\of K\to K$ be the map $\function{\tuplet{n,j}\of \nno\times K}\tuplet{n + 1,j}$ and use $b = \function i\tuplet{0,c(i)}\of I\to K$
The familiar part is proving the left lifting property for $\tuplet{b,s}\of I + K\to K$, as it is a pushout of a power of $\cycle_\nno \to \simplex_\nno$.
It feels stupid to need more than one pushout, but I am unsure what else to do.

The second part involves constructing a filler for $\function{\tuplet{n,i}\of \nno\disc\times I}\tuplet{n,c(i)}$ with induction.
The situation: $c=\tuplet{c_0,c_1}\of I + K\to K$ has the left lifting property. Now define $d\of\nno\disc\times I\to K$ recursively, by $d\tuplet{0,x} = c_0(x)$ and $d\tuplet{n + 1, x} = c_1(d(n,x))$. Then $d$ also has the left lifting property.

Suppose $f\of \hom(I+K,X)\times_{\hom(I+K,Y)}\hom(K,Y) \to \hom(K,X)$ is a filler operator for $c$ against $p$.
Define $g\of\hom(\nno\times I,X)\times_{\hom(\nno \times I,Y)}\hom(K,Y) \to \hom(K,X)$ as follows:
\begin{align*}
g(a,b) &= f(\tuplet{a_0,g(a_s,b)},b)\\
\end{align*}
That looks nice, but does it actually define a total function that satisfies the required equations?
The equation is correct, i.e. a function that satisfies it is a filler for $d$ against $p$. It does not define the function well, however.
This can be proved by induction I guess.

Assuming $\tuplet{n,j}\of\dom(g)$ for $n < m$, $\tuplet{m,j}\of\dom(g)$ because\dots this works out when $K$ is graded.

\section{2/6/17}
The goal is weighted coproducts. Now the discrete object are weighted coproducts of the terminal object, so that is a promising starting point.


The family lifting property is the normal lifting property in an alternative enrichment.

\paragraph{family lifting property}
The lifting property takes the enrichment as implicit parameter, but perhaps this should be an explicit parameter\dots
If there are a bunch of different enrichment, this might be a good idea.


I corrected the definition of fibration now. The next step involved adjusting the proves as well,
Especially 

\begin{itemize}
\item improve the definition of contractible as well.
\item use the new definition of fibrant and contractible in every proof.
\item replace coproducts with subobjects where possible.
\item track down where transfinite composition is used implicitly, make the argument explicit.
  * page 9, lemma 3.6 the end.	
\item try to get rid of transfinite compositions.
\end{itemize}

I updated the definition of lifting property with respect to a family. This permits a concrete way to write down certain proofs, which I am also introducing.
I do find that I remembered some forgotten aspects of earlier structures. As usual, my memory simplifies the proofs by erasing vital details, only hanging on to the general shape. Without these vital details some large scale restructuring becomes easy to imagine, but the chance that the new structure actually work becomes smaller.

I mean, I rediscovered the idea of an object of lifting problems, a vital detail that I didn't manage to put down clearly enough before and gradually removed as I rewrote the paper. The same happened with transfinite compositions. I had them in a way that obscured their role in the central proofs. Now I miss them.

\section{26/5/17}

Transfinite compositions are not used explicitly anywhere and don't seem like much of an addition.

Okay, suppose $f\of X\to X$ is a chain. Feels like the inclusion $X_0 \to X - f(X)$ should be the transfinite composition. Of course, $X - f(X)$ is not a simplicial set, unless we can adjust the restriction operator, but the existence of a transfinite composition suggest than we can.

Important change: rather than defining loose simplicial sets, I define the whole family in one go.
This may have impact on later parts of the paper.

Perhaps we better replace all coproducts with more direct definitions.

So now we have a longer to do list:
\begin{itemize}
\item repair found errors
\item don't use slice categories in the definition of enriched lifting\dots
\item replace coproducts with subobjects where possible.
\item track down where transfinite composition is used implicitly, make the argument explicit.
  * page 9, lemma 3.6 the end.
	
\item try to get rid of transfinite compositions.
\end{itemize}

Important insight: left adjoints preserve left lifting properties and right adjoint preserve right lifting properties. 
Hence the family lifting property reduces to the underlying lifting property!

What we needed comes from the enriched part of the definition! This is now very unclear.
Perhaps we need a lemma for this or something, but let's just see how far we get today.

As it stands, the text suggest that a lot of power comes from defining the lifting property in the slice category. It does not. 
There is an option to pull back morphism with left lifting property along \emph{discrete morphisms}, because of the enrichment. 
That is the power I wanted and should be using explicitly throughout my proofs.

Another insight: the coproducts I seek are \emph{weighted coproducts}.

But something seems to be missing now: how to get weighted colimits of members of the family?

We are looking for a new proof of:
\begin{lemma} Contractible morphisms are acyclic fibrations.\end{lemma}
This seems a construction that actually breaks up the family filler operator internally.
We need to make the case that this is permitted somehow\dots
It doesn't follow from general rules about cofibrations. It must use discreteness somehow.

Actually, we should have argued that the enrichment is over $\ambient/\nno$.
That is where all problems seem to melt away.

Perhaps there is a trick that makes all individual inclusions retracts of the family. 
That might just be the most promising option.
The only trouble is $0\to 1$.


I have been needing a sum of hom objects, but got a product instead.
That is an error. However, when I have repaired the definition, then we have what we need everywhere.

This is applied stack semantics:
The slice $\ambient\s/I\disc$ is enriched over the slice $\ambient/I$: $\nat(X,Y)[i] = \nat(X[i],Y[i])$.

\paragraph{yet another def}

\begin{definition} A morphism $f\of X\to Y$ of $\ambient\s$ is a \keyword{fibration} it is has a \emph{pointwise} right lifting property with respect to the family of horn inclusions.

Let $\set\geq = \set{\tuplet{n,k}\of \nno\times\nno |n\geq k}$ in $\ambient$.
The simplicial set $\simplex_{\set\geq}$ satisfies:
\begin{align*}
\base(\simplex_{\set\geq}) &= \set{\tuplet{\phi,k}\of\Ar(\simCat)\times\nno| k\leq \cod(\phi) } \\
\dim\tuplet{\phi,k} &= \dom(\phi) \\
\tuplet{\phi,k}\cdot \xi &= \tuplet{\phi\circ\xi,k}
\end{align*}
The simplicial set $\horn_{\set\geq}$ satisfies:
\begin{align*}
\base(\horn_{\set\geq}) &= \set{(\phi,k)\of\Ar(\simCat)\times\nno\middle| 
\begin{array}{l}
k\leq \cod(\phi),\\
\exists i\of\nno.\left\{\begin{array}{l}i\leq \cod(\phi), i\neq k,\\ \forall j\of \dom(\phi).\phi(j)\neq i \end{array}\right. 
\end{array}
} \\
\dim\tuplet{\phi,k} &= \dom(\phi) \\
\tuplet{\phi,k}\cdot \xi &= \tuplet{\phi\circ\xi,k}
\end{align*}
The simplicial object $\horn_{\set\geq}$ is subobject of $\simplex_{\set\geq}$ by definition. 
The inclusion $\horn_{\set\geq}\to\simplex_{\set\geq}$ is the family of all horn inclusions.

The formula $\tuplet{\phi,k}\mapsto \tuplet{\dom(\phi),\cod(\phi),k}$ defines morphisms of simplices $\horn_{\set\geq}\to\set\geq\disc$ and $\simplex_{\set\geq}\to\set\geq\disc$ that commute with the inclusion and make it a morphism in $\ambient\s/\set\geq\disc$. This category $\ambient\s/\set\geq\disc$ has an enrichment in $\ambient/\set\geq$, where $\nat(X,Y)$. If $\set\geq\ri(f)$ has the right lifting property with respect to the inclusion $\horn_{\set\geq}\to\set\geq\disc$ relative to the enrichment on $\ambient/\set\geq$.
\end{definition}

Perhaps this requires a new section, even if we use the notion only twice.

I suppose the family thing is quite clear and correct. But this enrichment stuff doesn't clear much up.
closer to the core, we could introduce a parametric variant of the enriched lifting property.

We could introduce the notion of lifting versus a discrete family from the start. 

Lifting discrete families as a core concept, to be introduced right after the enriched factorization system.

I know what I need, but as usual, it is a struggle to write down.

\section{28/4/17}
Dwelling on the contractible-cofibration factorization. The latching an matching elements evidently are part of fibrant and cofibrant replacements and perhaps the proof becomes clearer if we somehow use the replacements first. I don't see it working however.

Plan: print out and check for mistakes; try to publish once again? At the same time, look for computer verification.


\section{24/3/17}
Two parts stay difficult to understand, because they generalize in the internal language.
\begin{itemize}
\item proposition on the factorization of $f$ as a contractible morphism following a cofibration.
\item fibrancy of the universal modest fibration
\end{itemize}

The trouble with the factorization must be that we need to show a filler operator for the family of cycles. Other than a rewording of the current text, I don't see much to improve here.

This whole part is based on Reedy's work and it would be better to reflect that somehow.
I don't know how to do that yet.

\paragraph{Some observations on the relation with Reedy's work}
Reedy shows how a model structure on a small complete category can be lifted to functor categories. My starting point neither has a model structure, nor all colimits.
My construction combines the latching and the matching factorizations of the Reedy categories to yield only one of the factorizations of the model structure.
The latching part seem to ensure cofibrations, while the matching part ensures fillers.
The external induction hurts. Everything should be related to the internal natural number object.
Note that Reedy factorization is quite complicated and the paper tries to skip to the result.

There is a factorization of morphisms in the ambient category based on decidable monomorphism following split epimorphisms.
Reedy's construction lifts this to the category of simplicial objects.
Cofibrations are decidable monomorphism lifted as Reedy defines.
Contractibles are split epi's lifted as Reedy defines.
It stands to reason that his proof could be useful, if it weren't for the external induction in it.

It is good to look up the definitions again, if only for the confirmation that the proof in the paper is not more complicated than necessary.

\section{10/3/17}
We are working out exactly what a \emph{horn or cycle filler} operator is, just like we worked out what a simplicial set is, in hopes of making the proof clearer and more convincing.

The lifting property is more demanding because it has to take all cases into account.
I work in all kinds of slice categories to hide to gory details and keep track of additional requirement:
For a particular $f\of X\to Y$ and the family of horns $h\of D\to C$.
\begin{align*}
P &= \set{ \tuplet{a,b}\of(D\to X)\times(C\to Y)| f\circ a = b \circ h }\\
\dim(a(\tuplet{\phi,k})) &=\max(\cod(\phi))\\
\dim(b(\tuplet{\phi,k})) &= \max(\cod(\phi))\\
a(\tuplet{\phi,k})\cdot\chi &= a(\tuplet{\phi\circ \chi,k}) \\
b(\tuplet{\phi,k})\cdot\chi &= b(\tuplet{\phi\circ \chi,k}) \\
\end{align*}
\begin{itemize}
\item The cycle case is simpler, because we can drop the $k$-index.
\item The filler satisfies the same restrictions on dimensionality and restrictions, plus $c\circ h = a$ and $f\circ c = b$.
\end{itemize}

We now get a simplified notion of what a filler operator for both families are and can try to rewrite the proofs in order to build exactly such an operator.

Suppose we work out an official definition of horn and cycle fillers. What might happen?
The step from the filler to lifting cofibrations may be less obvious, requiring some updates of the proofs and definition.
Not the acyclic though, just the weakly invertible.

\newcommand\HLP{\mathrm{HLP}}
\begin{definition}
Let  Let $f\of X\to Y$ be an arbitrary morphism of $\ambient\s$. The object of horn lifting problems is 
\[\HLP(f) = \set{\tuplet{a,b}\of \base X^D\times \base Y^C \middle|\begin{array}{l}
  f\circ a = b\circ h,\\
  \dim(b\tuplet{\phi,k}) = \max(\dom\phi),\\
  b\tuplet{\phi,k}\cdot\chi = b\tuplet{\phi\circ \chi,k},\\
	a\tuplet{\phi,k}\cdot\chi = a\tuplet{\phi\circ \chi,k}
\end{array}}\]
Here $h\of D\to C$ is the inclusion of the following objects in $\ambient$.
\begin{align*}
C &= \coproduct{\phi\of\Ar(\simCat)}\cod(\phi) \\
D &= \set{\tuplet{\phi,k}\of C \middle| \exists i\of\cod(\phi)-\set k. \forall j\of\dom(\phi).\phi(j)\neq i}
\end{align*}
A \keyword{horn filler} is a morphism $c\of\HLP(f)\to \base X^C$ that satisfies the following equations. 
\begin{align*} c\tuplet{a,b}\circ h &= a & f\circ c\tuplet{a,b} &= b \end{align*}
A \emph{fibration} of $\ambient\s$ is a morphism with a horn filler.
\end{definition}

%Cycle fillers 
\newcommand\CLP{\mathrm{CLP}}
\begin{definition}
Let $f\of X\to Y$ be an arbitrary morphism of $\ambient\s$. The object of cycle lifting problems is 
\[\CLP(f) = \set{\tuplet{a,b}\of \base X^D\times \base Y^C \middle|\begin{array}{l}
  f\circ a = b\circ h,\\
  \dim(b(\phi)) = \max(\dom\phi),\\
  b(\phi)\cdot\chi = b(\phi\circ \chi),\\
  a(\phi)\cdot\chi = a(\phi\circ \chi)
\end{array}}\]
Here $h\of D\to C$ is the inclusion of the following objects in $\ambient$.
\begin{align*}
C &= \Ar(\simCat) \\
D &= \set{\phi\of C \middle| \exists i\of\cod(\phi).\forall j\of\dom(\phi).\phi(j)\neq i}
\end{align*}
A \keyword{cycle filler} is a morphism $c\of\CLP(f)\to \base X^C$ that satisfies the following equations. 
\begin{align*} c\tuplet{a,b}\circ h &= a & f\circ c\tuplet{a,b} &= b \end{align*}
A morphism  of $\ambient\s$ is \emph{contractible} if it has a cycle filler.
\end{definition}

Where do we have problems with generalizations?
\begin{itemize}
\item proposition on the factorization of $f$ as a contractible morphism following a cofibration.
\item the triple lifting property. Improved now.
\item if $f$ and $g\circ f$ are contractible, then so is $g$. Improved now.
\item fibrancy of the universal modest fibration
\end{itemize}

\section{Triple lifting property}
We derive this from the equality of contractible and the acyclic fibrations. The core argument is that $\tuplet{f\to g}$ is a fibration if $f\of A\to B$ is a cofibration and $g\of X\to Y$ is a fibration and contractible if $g$ is contractible or $f$ is acyclic. So how to define the horn and cycle fillers?

\[ \tuplet{f\to g} = \function{x\of X^B}\tuplet{g\circ x,x\circ f}\of X^B \to Y^B\times_{Y^A} X^A \]

Another approach is to take the pushout product of the families and construct the desired fillers there.

Take push out product of the family of horns with the family of cycles, then find a filler.
If $f$ is contractible, take the pushout product of the family of cycles with itself and find a filler for that too.
Then use adjoints etc. to prove the lemma.
We may be able to pull it of without products, however. The triple lift for the families is a special case form which we derive all the special cases.

How far would we get with just the family of cycles along an (acyclic) cofibration?

The ultimate point is that we can fill the pushout product by systematically using fillers for simplices.
That algorithmic reduction of a triple lifting problem to a horn or cycle lifting problem can be done inside $\ambient$ to show that elementary triple lifting problems have a solution if horn or cycle lifting problems have. There rest is the reduction of the general triple lifting problem to the product of the families.

The reduction uses monotone monics $[m + n]\to[m]\times[n]$. 
We start with a collection of $[m+n-1]$-dimensional faces in the pushout product. Unless $m=0$ or $n=0$ we have no $[m+n]$ dimensional faces however. So these need to be glued in, one by one.
These can be lexicographically ordered again, after which we ensure that they get filled.
I.e. we build a sequence $A_i\to A_{i+1}$ of approximations and show that each requires a well defined application of the preexisting filler operator.
Clearly, the result is a proof in the same style as the descent proof, with one important difference: we don't rely on saturation, but an a filler operator to do the job.

\paragraph{set up for triple lift}
We need to fill $\simplex[m]\times \cycle[n]\cup \horn_k[m]\times\simplex[n]$. The first subdivision is along $\set{k}\times \simplex[n]$, whose point we will use as tops of horns to fill. The second subdivision is along $[m]-\set{k}$. We include down sets into each new $m+n$ dimensional face we glue in, until we are completes. The last subdivision is along dimension, as it seems we need face completion to get the required horns.

The main point of course is that we have a construction and therefore a filler operator that works on arbitrary horns.

Can we focus on greater collections than individual simplicies? At least in the intermediate steps we can\dots

\paragraph{considerations}
What matters for the case c-c-af is that the pushout product is a cofibration, which requires no reductions.
The cases c-ac-f and ac-c-f are where the reduction to the family of horns is needed.
Still, we should be comfortable with just the case of a pushout product of the family with an arbitrary cofibrations.

\paragraph{subdivisions}
We want to systematically subdivide the problem of filling
\[ A = \simplex[m]\times \cycle[n]\cup \horn_k[m]\times\simplex[n] \to \simplex[m]\times \simplex[n] \]
Damn this is hard.

Each monic $[m+n]\to [m]\times [n]$ must be glued in at some stage. This gluing in possible if we have a horn.
That is a base point $l$ such that the composition with monics $[m+n-1]\to [m+n]$ that hit $l$ have already been included at an earlier stage.

One thing we know: composition of these monotone monic with the projections $\to[m]$ an $\to[n]$ are surjective. Why?
By induction over $m+n$. Case 0 is trivial. Otherwise the second last element must be lesser in one of the variables,
hence inside the $m+n-1$ dimensional subsquares. The induction hypothesis makes the compositions of the submonic surjective. This forces $f(m+n) = (m,n)$, answering when either of those are hit.

What do we start with?
\begin{itemize}
\item All monics $[m+n-1] \to ([m]-\set{i})\times[n]$, where $i\neq k$.
\item All monics $[m+n-1] \to [m]\times ([n]-\set{j})$
\item No monics $[m+n-1] \to ([m]-\set{k})\times[n]$
\end{itemize}
For each face we glue in, the intersection with the previous complex cannot be a cycle however.
Given a supporting point, there can be no monics that omit it.
This is why the spine $\set{k}\times[n]$ is the unique supply of supporting points.

Monotone monics cannot meander. The set of elements that intersect the spin is always a simple interval.

What worries me is that adding any monic necessarily adds all the monics that miss each point along the spine.

Suppose $M_j$ consists of monics that intersect the $k$-spine in $j+1$ places. Is this the proper selection?
Do we every get any monics for free? I.e. without explicitly gluing them in?

Let's try the most difficult situation and hope for the best.

$M_{i,j}$ where $i\leq j\of[n]$ is the set of monotone monics that hit the points $(k,i)$ to $(k,j)$.
For gluing in $f$ we pick $(k,i)$ as top. Now $f\circ d_l$ for $l\neq k+i$ should already be present, while
$f\circ d_{k+i}$ should not.

We look for the first point where $f(k+j+n)_1 > j$ and swap all those points!?
Nope, we need to subdivide one step further.

Better approach: the 'distance' of two monotone monics is the number of places they don't coincide.
There is a specific monic that we start with and then we progressively add in monics at greater distances.
Note the law $f(k)_0+f(k)_1=k$, which may be even better than out surjectivity claims.

So let's try again: $f_0(l) = \tuplet{l,0}$ if $l\leq k$, $f_0(l) = \tuplet{k,l-k}$ if $l$ is between $k$ and $k+n$ and 
$f_0(l) = \tuplet{l-n,n}$ if $l\geq n+k$. We gluing the faces in order of their distance (a number of steps from the basis figure)
to this monic. That way, we can rely on the overlap to prove required faces are present.

The only problem is choosing the base point is such a way that the opposing face is absent. Can we always do this?

Let $f$ be glued in and $g$ be different from in in point $p\of[m+n]$. For $g\circ \partial_q$ if $q\neq p$ we know those faces are available.
We also need a base point, however. Some place where $f_0$ and $g_0$ are both $k$.
Then we note that all opposites to where $f_0=k$ have been added however\dots
What am I saying? All subfaces of $g$ are different from $f$ except $g\circ \partial_p$!

In general, the surjectivity ensures we can use the $k$-spine to glue in any face. What we need is the opposite:
a proof that the face opposing the chosen base point has not already been glued in!

So for $f$ let the least $p$ such that $f(p)_0=k$ be the base point. We would hate for $f\circ\partial_p$ to be present and there is exactly one face that could case this tragedy: $f + (p \mapsto \tuplet{k-1,f_1(p)+1})$. Its least point is $p+1$, so that gives us a criterion for ordering faces: the least points that hit $k$ 

The existing subfaces seem like causes for $f\circ\partial_p$ existence, but that requires either coordinate of $f(p) = \tuplet{k,x}$ not to occur anymore.
In the first case that forces $f(p-1)_0=k-1$ and $f(p+1)_0=k+1$, which is in the missing $([m]-\set k)\times [n]$ area. In the second, $f(p-1) = \tuplet{k,x-1}$, which means that $p$ is not the least point, contradicting an assumption. We in fact hardly notice the preexisting faces.

The main part is then 'face completion': we have a base point and dimension by dimension glue in the necessary faces, noting that we already have all the $[m+n-2]$ ones already.

\paragraph{Setting up again}
More analysis: every monic can be seen as a sequence of increments in either vertical or horizontal directions. Hence the number of monics is the old familiar:
\[ \left(\begin{array}{c}m+n\\n\end{array}\right) \] 
Everywhere a monic 'turns a corner', we can invert that corner to find another monic. This is an adjacent face. 

The main thing to worry about are the faces of $([m]-\set k)\times [n]$. This makes certain faces $[m+n] \to [m]\times [n]$ dangerous,
precisely the faces that only hit $k$ in one point. Perhaps those are the only ones to look out for, or perhaps we risk chocking of intermediate faces the same way if we don't tread carefully. This is all very unclear, but the reason seems to be that there is no best solution, rather than that it is hard to pick the right ordering.

If we gradually diminish the number of places $p$ where $f_0(p)=k$, we gradually glue in lower dimensional monics of $([m]-\set k)\times [n]$, which makes it more likely that wanted faces are available.

A smarter choice of base point revolves are the inversion of the corner. Now we know that the faces we want are already there\dots
So the base point should move around a lot, rather than stick to the $k$-spine.

There is a clear starting point:
\begin{align*}
f(p) &= \tuplet{p,0} & p&\leq k\\
f(k+p) &= \tuplet{k,p} & p&\leq n\\
f(k+n+p) &= \tuplet{k+p,n} & p&\leq m-k
\end{align*}
Then the ordering depends on how many points a monic has in common with this one. We can always invert the least point of difference, when a monic's turn comes up.

All monics are going to have two points in common: $(0,0)$ and $(m,n)$.
If a monic $g$ has only three point in common with $f$, could the third point be outside of the $k$-spine? 
Nope: $g(p)=\tuplet{k,p-k}$ somewhere and $f(p)=\tuplet{k,p-k}$.

How do we glue in $f$?
There are at most two faces not already present: $f\circ d_k$ and $f\circ d_{k+n}$. If $k=0$ or $k=m$ this reduces to 1, which is ideal.
Otherwise we can first glue in $f\circ d_{k+n}$ and then proceed. I am unsure if this step is unavoidable.

We order the set of monics in such a way that a monic appears earlier in the ordering, if it has more points in common with $f$.
It is more difficult than that though

Inverting a point of difference will not always bring us back all the way to $f$. 
The following measure of distance is probably better:
\[ d(f,g) = \sum_{p\of[m+n]}| f_0(p)-g_0(p) | \]
It has the property that each inversion in the right direction bring a morphism closer to $f$.

In order to glue in a new face, we need a base point and all $(n+m-1)$-dimensional faces not containing that point.

Some of these faces are present in less distant faces\dots
Vertical or horizontal stretches do not present a problem if we pick a base point on the $k$-spine, because they are present in the starting material!
The are only three options. The submonic omits a vertical point, a horizontal point or is part of a face closer to $f$. Distance therefore does the trick.

So the matter of the actual ordering remains.

The choice model makes us think about the places where vertical moves happen: $n$ places to pick out of $m+n$ ones.
We subsequently make these choices, picking one element above the other, in each step leaving enough points to work with.
We could also consider the game of increasing distances. Where do you choose to deviate form $f$.
That way we can create an ordering based on partial distance sums, or the list of pointwise distances.

Subtracting $f_0-g_0$ give a list of number that we can order lexicographically, using an ordering on numbers, e.g. based on $|n+\epsilon|$ where $|\epsilon|<0.5$.
An this gives the ordering which we will use for the faces.


\section{Triple lifting}
The triple lifting lemma is the work horse of constructive homotopy theory. The purpose of this section is to convince you that this lemma is valid in the internal language $\ambient$, because it is constructive and predicative to a sufficient amount.

\begin{lemma}[Triple lifting property] Let $f\of A\to B$ and $g\of C\to D$ be cofibrations and let $h\of X\to Y$ be a fibration. Let $a\of A\times D\to X$, $b\of B\times C\to X$ and $c\of B \times D\to Y$ satisfy $a\circ(\id_A\times g) = b\circ(f\times \id_C)$, $h\circ a=c\circ(f\times \id_D)$ and $h\circ b=c\circ(\id_B\times g)$. If one of $f$, $g$ or $h$ is acyclic, then there is a $d\of B\times D\to X$ such that $d\circ(f\times\id_D)=a$, $d\circ(\id_B\times g)=b$ and $h\circ d = c$.
\[\xy
(0,20)*+{A\times C}="AC",(25,20)*+{B\times C}="BC",(40,20)*+{X}="X",
(0,0)*+{A\times D}="AD",(25,0)*+{B\times D}="BD",(40,0)*+{Y}="Y"
\ar^{f\times\id} "AC";"BC"
\ar_{\id\times g} "AC";"AD"
\ar_{f\times\id} "AD";"BD"
\ar^{a} "AD";"X"
\ar|(.6){\id\times g} "BC";"BD"
\ar^(.6){b} "BC";"X"
\ar@{.>}_{d} "BD";"X"
\ar_(.6){c} "BD";"Y"
\ar^{h} "X";"Y"
\endxy\]
\label{triple lift}
\end{lemma}

\begin{proof} 
Cut down the variety of lifting problems with the following strategies.
\begin{itemize}
\item Using symmetry, derive the cases where $g$ is acyclic from those where $f$ is.
\item By definition, there is an equivalence between lifting acyclic cofibrations and having a filler operator for the family of horns. Use this to reduce the cases where $f$ is acyclic to the case where $f$ is the family of horns.
\item By lemma Reedy, there is an equivalence between lifting cofibrations and having a filler operator for the family of cycles. Use this to reduce the cases where $g$ is an arbitrary cofibration to the case where $g$ is the family of cycles and do the same for $f$.
\end{itemize}
These reductions can be proved with the \emph{pullback power} construction and some diagram chasing.
\[\xy
(34,20)*+{X^C}="top",(0,10)*+{X^D}="left",(24,10)*+{\bullet}="middle",(44,10)*+{Y^C}="right",(34,0)*+{Y^D}="bottom"
\ar^{X^g} "left";"top" \ar@{.>}|(.6){h^g} "left";"middle" \ar_{h^D} "left";"bottom" \ar "middle";"bottom"
\ar "middle";"top" \ar^(.6){h^C} "top";"right" \ar_(.6){Y^g} "bottom";"right"
\endxy\]
The triple lifting problem is equivalent to the simple lifting problem of $f$ against $h^g$.
This leaves two tasks.
\begin{enumerate}
\item Prove that if $h$ has a filler operator for cycles, it has a triple filler operator for the cases where $f$ and $g$ are both the family of cycles.
\item Prove that if $h$ has a filler operator for horn, it can also handle all triple lifting problems involving the family of horns $f$ and the family of cycles $g$.
\end{enumerate}

In both cases there is a subobject of $B\times D$ that is the pushout of $f\times C$ and $A\times g$, because the underlying monomorphisms of $f$ and $g$ are decidable.
\[ \set{\tuplet{x,y}\of B\times D\middle| (x\of f(A)) \vee (y\of g(C)) }\]
Since pushouts preserve left lifting properties, a filler operator for the pushout product is sufficient.

For $m > 0$ and $n > 0$ none of the faces of $\simplex[m]\times \simplex[n]$ belong to either $\simplex[m]\times \cycle[n]$ or $\horn_k[m]\times\simplex[n]$ for any $k\of[m]$, because the faces are $m+n$-dimensional and the faces of either $\simplex[m]$ or $\simplex[n]$ are not. The cases where $m=0$ or $n=0$ are trivial because $\simplex[0] \simeq 1$, $\cycle[0]\simeq 0$ and $\horn_0[0]$ does not exist. Since the pushout product is a countable sum of these inclusions, it is a cofibration. This settles the case where both $f$ and $g$ are the family cycle inclusions, because $h$ is an acyclic fibration.

The case where $f$ is the family of horn inclusions is more complicated. Fortunately, this case is worked out in the proof of lemma A.1 in \citep{DD&DIS11}, where \emph{inner anodyne} is what this paper calls acyclic and \emph{box product} is pushout product. Note that all necessary properties of simplices are decidable. Since the pushout product of $f$ and $g$ is an acyclic cofibration.
\end{proof}
\hide{perhaps we should adopt the same terms as that paper.}


\hide{ 
The case for $f$ acyclic seems simpler, but perhaps pushout products are not as ubiquitous as I thought. I don't see how we can decide if a degenerate simplex belongs to the image of a cofibration. The problem is determining that $x\cdot \phi = x$ for some $\phi\of[\dim x]\to[\dim x]$, since $=$ is not always decidable. This in turn that pushout products may not be available for all cofibrations.

The trick involves regularity: the family of faces exists internally and therefore so does its union.

Not good enough! We would need a union of faces inside. We can create a 'least pseudo-complement'. 
}



\end{document}