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.  strong-comprehension-coproducts : Type _ strong-comprehension-coproducts = {Γ Δ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⨾ x ]) (b : D.Ob[ Δ ]) m⊥m B (Q.πᶜ P.⨾ˢ x , a ) (P.πᶜ {x = b})


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.


opaque ∐-strong-elim : {Γ Δ} {x : E.Ob[ Γ ]} {a : D.Ob[ Γ Q.⨾ x ]} {b : D.Ob[ Δ ]} (σ : Hom (Γ P.⨾ x a) Δ) (ν : Hom (Γ Q.⨾ x P.⨾ a) (Δ P.⨾ b)) σ (Q.πᶜ P.⨾ˢ x , a ) P.πᶜ ν Hom (Γ P.⨾ x a) (Δ P.⨾ b) ∐-strong-elim {x = x} {a = a} {b = b} σ ν p = strong x a b p .centre .fst
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.


opaque unfolding ∐-strong-elim ∐-strong-β : {Γ Δ} {x : E.Ob[ Γ ]} {a : D.Ob[ Γ Q.⨾ x ]} {b : D.Ob[ Δ ]} {σ : Hom (Γ P.⨾ x a) Δ} {ν : Hom (Γ Q.⨾ x P.⨾ a) (Δ P.⨾ b)} (p : σ (Q.πᶜ P.⨾ˢ x , a ) P.πᶜ ν) ∐-strong-elim σ ν p (Q.πᶜ P.⨾ˢ x , a ) ν ∐-strong-β p = strong _ p .centre .snd .fst
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)
(coprods : has-comprehension-coproducts D-fib E-fib Q) (strong : strong-comprehension-coproducts P₂ coprods) (p : B₁ .Precategory._∘_ σ ((D Comprehension.⨾ˢ D-fib) P₂ (Comprehension.πᶜ E E-fib Q) (coprods .has-comprehension-coproducts.⟨,⟩ x a)) ≡ B₁ .Precategory._∘_ (Comprehension.πᶜ D D-fib P₂) ν) → B₁ .Precategory._∘_ (Comprehension.πᶜ D D-fib P₂) (strong-comprehension-coproducts.∐-strong-elim P₂ coprods strong σ ν p) ≡ σ” class=“Function”>∐-strong-sub : {Γ Δ} {x : E.Ob[ Γ ]} {a : D.Ob[ Γ Q.⨾ x ]} {b : D.Ob[ Δ ]} {σ : Hom (Γ P.⨾ x a) Δ} {ν : Hom (Γ Q.⨾ x P.⨾ a) (Δ P.⨾ b)} (p : σ (Q.πᶜ P.⨾ˢ x , a ) P.πᶜ ν) P.πᶜ ∐-strong-elim σ ν p σ ∐-strong-sub p = strong _ p .centre .snd .snd
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)
(coprods : has-comprehension-coproducts D-fib E-fib Q) (strong : strong-comprehension-coproducts P₂ coprods) (p : B₁ .Precategory._∘_ σ ((D Comprehension.⨾ˢ D-fib) P₂ (Comprehension.πᶜ E E-fib Q) (coprods .has-comprehension-coproducts.⟨,⟩ x a)) ≡ B₁ .Precategory._∘_ (Comprehension.πᶜ D D-fib P₂) ν) (other : B₁ .Precategory.Hom ((D Comprehension.⨾ D-fib) P₂ Γ₁ (coprods .has-comprehension-coproducts.∐ x a)) ((D Comprehension.⨾ D-fib) P₂ Δ₁ b)) → B₁ .Precategory._∘_ other ((D Comprehension.⨾ˢ D-fib) P₂ (Comprehension.πᶜ E E-fib Q) (coprods .has-comprehension-coproducts.⟨,⟩ x a)) ≡ ν → B₁ .Precategory._∘_ (Comprehension.πᶜ D D-fib P₂) other ≡ σ → other ≡ strong-comprehension-coproducts.∐-strong-elim P₂ coprods strong σ ν p” class=“Function”>∐-strong-η : {Γ Δ} {x : E.Ob[ Γ ]} {a : D.Ob[ Γ Q.⨾ x ]} {b : D.Ob[ Δ ]} {σ : Hom (Γ P.⨾ x a) Δ} {ν : Hom (Γ Q.⨾ x P.⨾ a) (Δ P.⨾ b)} (p : σ (Q.πᶜ P.⨾ˢ x , a ) P.πᶜ ν) (other : Hom (Γ P.⨾ x a) (Δ P.⨾ b)) other (Q.πᶜ P.⨾ˢ x , a ) ν P.πᶜ other σ other ∐-strong-elim σ ν p ∐-strong-η p other β sub = ap fst (sym \$ strong _ p .paths (other , β , sub))
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)
(coprods : has-comprehension-coproducts D-fib E-fib Q) (strong : strong-comprehension-coproducts P₂ coprods) → strong-comprehension-coproducts.∐-strong-elim P₂ coprods strong (Comprehension.πᶜ D D-fib P₂) ((D Comprehension.⨾ˢ D-fib) P₂ (Comprehension.πᶜ E E-fib Q) (coprods .has-comprehension-coproducts.⟨,⟩ x a)) refl ≡ B₁ .Precategory.id” class=“Function”>∐-strong-id : {Γ} {x : E.Ob[ Γ ]} {a : D.Ob[ Γ Q.⨾ x ]} ∐-strong-elim P.πᶜ (Q.πᶜ P.⨾ˢ x , a ) refl id ∐-strong-id = sym (∐-strong-η refl id (idl ) (idr ))