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

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 D) {Q : Comprehension 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 D) {Q : Comprehension 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 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)
where

  private
open Cat.Reasoning B
module E = Displayed E
module E* {Ξ Ξ : Ob} (Ο : Hom Ξ Ξ) = Functor (base-change E E-fib Ο)
module E-fib {x y} (f : Hom x y) (y' : E.Ob[ y ]) =
Cartesian-lift (Cartesian-fibration.has-lift E-fib f y')
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 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 =
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