open import Cat.Displayed.Comprehension.Coproduct
open import Cat.Displayed.Comprehension
open import Cat.Displayed.Cartesian
open import Cat.Morphism.Orthogonal
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Displayed.Comprehension.Coproduct.Strong where

Strong comprehension coproducts🔗

Let $\mathcal{D}$ and $\mathcal{E}$ be a pair of comprehension categories over the same base category $\mathcal{B}$, such that $\mathcal{D}$ has coproducts over $\mathcal{E}$. Type theoretically, this (roughly) corresponds to a type theory with a pair of syntactic categories (for instance, types and kinds), along with mixed-mode $\Sigma$ types.

We can model this using coproducts over a comprehension category, but the elimination principle we get from this setup is pretty weak: we really only have a recursion principle, not an elimination principle. That has to be be captured through an extra condition.

We say that a comprehension category has strong comprehension coproducts if (it has comprehension coproducts, and) the canonical substitution $\pi_{\mathcal{E}}, \langle x , a \rangle$ forms an orthogonal factorisation system with the weakening maps $\pi_{\mathcal{D}}$. In more elementary terms, this means that any square diagram, as below, has a unique diagonal filler.

That's a very concise definition: too concise. Let's dig a bit deeper.



In the diagram, $B$ is a type in some context $\Delta$, and we have a
substitution $\sigma : \Gamma , \coprod_X A \to \Delta$ --- but, for
intuition, we might as well zap $\sigma$ to the identity: $B$ is a type
in context $\Gamma, \coprod_X A$.
In this simplified setting, the top morphism $\nu : \Gamma, X, A \to
\Gamma, B$ must be entirely determined by a "term" $\Gamma, x : X, a : A
\vdash \nu : B\langle x, a \rangle$, for the outer square to commute.
Then, we see that the diagonal filler is exactly an elimination
principle: since it too commutes with weakening, it must be determined
by a "term" $\Gamma, v : \coprod_X A \vdash B(v)$!

However, note that this elimination principle does **not** allow us to
eliminate an arbitrary object from $\cE$, which corresponds
type-theoretically having _no_ $\cE$-large elimination. This large
elimination is captured by [[very strong comprehension coproducts]],
which are extremely rare.

The upper-left triangle of the diagram gives us our $\beta$ law;
eliminating out of a substitution extended with an introduction form
gives us the original substitution.

The lower-right triangle describes how substitution interacts with
eliminators; if we forget the thing we just eliminated into, then
we recover the substitution from $\Gamma, \coprod X A \to \Delta$.

<a id="strong-comprehension-coproducts.∐-strong-sub"></a><a id="6937" href="Cat.Displayed.Comprehension.Coproduct.Strong.html#6937" data-type="(P₂ : Comprehension D)

Finally, uniqueness gives us an $\eta$; any other substitution that
walks like the eliminator and quacks like the eliminator is the
eliminator.

<a id="strong-comprehension-coproducts.∐-strong-η"></a><a id="7396" href="Cat.Displayed.Comprehension.Coproduct.Strong.html#7396" data-type="(P₂ : Comprehension D)

Now, for some useful lemmas. If we eliminate by simply packaging up
the data into a pair, then we've done nothing. Categorically, this
means the unique filler of the following diagram is the identity
morphism.

~~~{.quiver}
\begin{tikzcd}
  {\Gamma,_{\cE}X,_{\cD}A} && {\Gamma,_{\cD}\coprod X A} \\
  \\
  {\Gamma,_{\cD}\coprod X A} && \Gamma
  \arrow["{\pi_{\cE},\langle X, A\rangle}"', from=1-1, to=3-1]
  \arrow["{\pi_{\cD}}", from=1-3, to=3-3]
  \arrow["{\pi_{\cD}}"', from=3-1, to=3-3]
  \arrow["{\pi_{\cE},\langle X, A\rangle}", from=1-1, to=1-3]
  \arrow["id", from=3-1, to=1-3]
\end{tikzcd}
~~~

<a id="strong-comprehension-coproducts.∐-strong-id"></a><a id="8460" href="Cat.Displayed.Comprehension.Coproduct.Strong.html#8460" data-type="(P₂ : Comprehension D)