open import Cat.Displayed.Comprehension.Coproduct.Strong
open import Cat.Displayed.Comprehension.Coproduct
open import Cat.Displayed.Cartesian.Indexing
open import Cat.Displayed.Comprehension
open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
open import Cat.Morphism.Orthogonal
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

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

π_{E}, ⟨ x, a ⟩ : Γ,_{E} X,_{D} A \to Γ,_{D} ∐_{X} A

is an isomorphism.

module _
  {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
  {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
  {D-fib : Cartesian-fibration D} {E-fib : Cartesian-fibration E}
  (P : Comprehension-structure D) {Q : Comprehension-structure E}
  (coprods : has-comprehension-coproducts D-fib E-fib Q)
  where
  private
    open Cat.Reasoning B
    module E = Displayed E
    module D = Displayed D
    module P = Comprehension D D-fib P
    module Q = Comprehension E E-fib Q
    open has-comprehension-coproducts coprods

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

module very-strong-comprehension-coproducts
  {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
  {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
  {D-fib : Cartesian-fibration D} {E-fib : Cartesian-fibration E}
  (P : Comprehension-structure D) {Q : Comprehension-structure E}
  (coprods : has-comprehension-coproducts D-fib E-fib Q)
  (vstrong : very-strong-comprehension-coproducts P coprods)
  where
  private
    open Cat.Reasoning B
    module E = Displayed E
    module D = Displayed D
    module P = Comprehension D D-fib P
    module Q = Comprehension E E-fib Q
    open has-comprehension-coproducts coprods
    module vstrong {Γ} (x : E.Ob[ Γ ]) (a : D.Ob[ Γ Q.⨾ x ]) =
      is-invertible (vstrong 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 $β$ 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 $η$ 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$ be a comprehension category over $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-structure E}
  (coprods : has-comprehension-coproducts E-fib E-fib P)
  where

  private
    open Cat.Reasoning B

    module E where
      open Displayed E public
      open Cartesian-fibration E E-fib public

    module E* {Γ Δ : Ob} (σ : Hom Γ Δ) = Functor (base-change E E-fib σ)

    open Comprehension E E-fib P
    open has-comprehension-coproducts coprods

  self-strong-comprehension-coproducts→very-strong
    : strong-comprehension-coproducts P coprods
    → very-strong-comprehension-coproducts P coprods

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

The $β$ and $η$ 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