module Cat.Displayed.Comprehension.Coproduct.VeryStrong where

Very Strong Comprehension Coproducts🔗

As noted in strong comprehension coproducts, the elimination principle for comprehension coproducts is quite weak, being more of a recursion principle. Strong coproducts model coproducts with a proper elimination, but as also noted there, we’re lacking large elimination. If we want that, we have to find very strong comprehension coproducts.

Let D\mathcal{D} and E\mathcal{E} be comprehension categories over B\mathcal{B}. We say that D\mathcal{D} has very strong E\mathcal{E}-comprehension coproducts if the canonical substitution

πE,⟹x,a⟩:Γ,EX,DA→Γ,D∐XA \pi_{\mathcal{E}}, \langle x , a \rangle : \Gamma,_{\mathcal{E}}X,_{\mathcal{D}}A \to \Gamma,_{\mathcal{D}}\textstyle\coprod_X A

is an isomorphism.

  very-strong-comprehension-coproducts : Type _
  very-strong-comprehension-coproducts =
    ∀ {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⚟ x ])
    → is-invertible (Q.πᶜ P.⚟ˢ ⟹ x , a ⟩)

This gives us the familiar first and second projections out of the coproduct.

  opaque
    ∐-fst
      : ∀ {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⚟ x ])
      → Hom (Γ P.⚟ ∐ x a) (Γ Q.⚟ x)
    ∐-fst x a = P.πᶜ ∘ vstrong.inv x a

  opaque
    ∐-snd
      : ∀ {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⚟ x ])
      → Hom (Γ P.⚟ ∐ x a) (Γ Q.⚟ x P.⚟ a)
    ∐-snd x a = vstrong.inv x a

These come with their respective β\beta rules, but they are slightly obfuscated due to having to work with substitutions rather than terms.

  opaque
    unfolding ∐-fst
    ∐-fst-β
      : ∀ {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⚟ x ])
      → ∐-fst x a ∘ (Q.πᶜ P.⚟ˢ ⟹ x , a ⟩) ≡ P.πᶜ
    ∐-fst-β x a = cancelr (vstrong.invr x a)

  opaque
    unfolding ∐-snd
    ∐-snd-β
      : ∀ {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⚟ x ])
      → ∐-snd x a ∘ (Q.πᶜ P.⚟ˢ ⟹ x , a ⟩) ≡ id
    ∐-snd-β x a = vstrong.invr x a

We also have an η\eta law, though this too is still a bit obfuscated.

  opaque
    unfolding ∐-fst ∐-snd
    ∐-very-strong-η
      : ∀ {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⚟ x ])
      → (Q.πᶜ P.⚟ˢ ⟹ x , a ⟩) ∘ ∐-snd x a ≡ id
    ∐-very-strong-η x a = vstrong.invl x a

Note that very strong coproducts are always strong.

  strong : strong-comprehension-coproducts P coprods
  strong = to-strong-comprehension-coproducts P coprods mkstrong where
    open make-strong-comprehension-coproducts

    mkstrong : make-strong-comprehension-coproducts P coprods
    mkstrong .∐-strong-elim σ Îœ p = Îœ ∘ ∐-snd _ _
    mkstrong .∐-strong-β p = cancelr (∐-snd-β _ _)
    mkstrong .∐-strong-sub p = pulll (sym p) ∙ cancelr (∐-very-strong-η _ _)
    mkstrong .∐-strong-η p other β η = intror (∐-very-strong-η _ _) ∙ pulll β

Strong coproducts over the same category are very strong🔗

Let E\mathcal{E} be a comprehension category over B\mathcal{B} having comprehension coproducts over itself. If these coproducts are strong, then they are automatically very strong. That should make sense: we have have been motivating strong comprehension coproducts as having elimination but no large elimination, but if we only have one “size” going around, then elimination is large elimination!

module _
  {ob ℓb oe ℓe} {B : Precategory ob ℓb}
  {E : Displayed B oe ℓe}
  {E-fib : Cartesian-fibration E}
  {P : Comprehension E}
  (coprods : has-comprehension-coproducts E-fib E-fib P)
  where
  self-strong-comprehension-coproducts→very-strong
    : strong-comprehension-coproducts P coprods
    → very-strong-comprehension-coproducts P coprods

We begin by defining a first projection Γ,∐XA→Γ,X\Gamma, \coprod X A \to \Gamma, X by factorizing the following square. This really is special: in the case of strong comprehension coproducts, Γ,X\Gamma, X and Γ,X,D\Gamma, X, D correspond to different context extensions (analogy: the first extends the context by a kind, the second by a type). But since we’re dealing with very strong coproducts, they’re the same extension.

We can then define the second projection Γ,∐XA→Γ,X,A\Gamma, \coprod X A \to \Gamma, X, A using the first.

The β\beta and η\eta laws follow from some short calculations.

  self-strong-comprehension-coproducts→very-strong strong {Γ = Γ} x a =
    make-invertible
      ∐-strong-snd
      ∐-strong-snd-η
      (∐-strong-β ∐-strong-fst-β)
    where
      open strong-comprehension-coproducts P coprods strong

      ∐-strong-fst : Hom (Γ ⚟ ∐ x a) (Γ ⚟ x)
      ∐-strong-fst = ∐-strong-elim πᶜ πᶜ (sub-proj ⟹ x , a ⟩)

      ∐-strong-fst-β : ∐-strong-fst ∘ (πᶜ ⚟ˢ ⟹ x , a ⟩) ≡ πᶜ ∘ id
      ∐-strong-fst-β = ∐-strong-β _ ∙ sym (idr _)

      ∐-strong-snd : Hom (Γ ⚟ ∐ x a) (Γ ⚟ x ⚟ a)
      ∐-strong-snd = ∐-strong-elim ∐-strong-fst id ∐-strong-fst-β

      ∐-strong-snd-forget : πᶜ ∘ (πᶜ ⚟ˢ ⟹ x , a ⟩) ∘ ∐-strong-snd ≡ πᶜ
      ∐-strong-snd-forget =
        πᶜ ∘ (πᶜ ⚟ˢ ⟹ x , a ⟩) ∘ ∐-strong-snd ≡⟚ pulll (sub-proj ⟹ x , a ⟩) ⟩≡
        (πᶜ ∘ πᶜ) ∘ ∐-strong-snd              ≡⟚ pullr (∐-strong-sub ∐-strong-fst-β) ⟩≡
        (πᶜ ∘ ∐-strong-fst)                   ≡⟚ ∐-strong-sub (sub-proj ⟹ x , a ⟩) ⟩≡
        πᶜ                                    ∎

      ∐-strong-snd-η : (πᶜ ⚟ˢ ⟹ x , a ⟩) ∘ ∐-strong-snd ≡ id
      ∐-strong-snd-η =
        ∐-strong-η refl _ (cancelr (∐-strong-β ∐-strong-fst-β)) ∐-strong-snd-forget
        ∙ ∐-strong-id