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 and be comprehension categories over We say that has very strong coproducts if the canonical substitution

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.

      : βˆ€ {Ξ“} (x : E.Ob[ Ξ“ ]) (a : D.Ob[ Ξ“ Q.β¨Ύ x ])
      β†’ Hom (Ξ“ P.β¨Ύ ∐ x a) (Ξ“ Q.β¨Ύ x)
    ∐-fst x a = P.Ο€αΆœ ∘ vstrong.inv x a

      : βˆ€ {Ξ“} (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 rules, but they are slightly obfuscated due to having to work with substitutions rather than terms.

    unfolding ∐-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)

    unfolding ∐-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 law, though this too is still a bit obfuscated.

    unfolding ∐-fst ∐-snd
      : βˆ€ {Ξ“} (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 be a comprehension category over 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)
    : strong-comprehension-coproducts P coprods
    β†’ very-strong-comprehension-coproducts P coprods

We begin by defining a first projection by factorizing the following square. This really is special: in the case of strong comprehension coproducts, and 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 using the first.

The and laws follow from some short calculations.

  self-strong-comprehension-coproducts→very-strong strong {Γ = Γ} x a =
      (∐-strong-β ∐-strong-fst-β)
      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