open import Cat.Displayed.Cartesian.Indexing
open import Cat.Displayed.Comprehension
open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
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
{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 E)
where

private
open Cat.Reasoning B
module E = Displayed E
module D = Displayed D
module Dβ {Ξ} = Cat.Reasoning (Fibre D Ξ)
module Dr = Cat.Displayed.Reasoning D
module D-fib {x y} (f : Hom x y) (yβ² : D.Ob[ y ]) =
Cartesian-lift (Cartesian-fibration.has-lift D-fib f yβ²)
open Comprehension E E-fib P
module D* {Ξ Ξ : Ob} (Ο : Hom Ξ Ξ) = Functor (base-change D D-fib Ο)
module Ο* {Ξ : Ob} (x : E.Ob[ Ξ ]) = Functor (base-change D D-fib (ΟαΆ {x = x}))
open Functor
open _=>_


# Coproducts in comprehension categoriesπ

Let $\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}$ be a comprehension category and $\mathcal{D} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}$ a fibration over the same base. We say that $\mathcal{D}$ has $\mathcal{E}$-coproducts when:

• For every $\Gamma : \mathcal{B}$, $X : \mathcal{E}_{\Gamma}$, and $A : \mathcal{D}_{\Gamma, X}$, there exists an object $\coprod_{X} A : \mathcal{D}_{\Gamma}$;

• Every projection $\pi : \Gamma, X \to X$ induces a cocartesian map $\langle\rangle : A \to_{\pi} \coprod_{X} A$;

• For every cubical diagram as below, if $f : X \to Y$ is cartesian in $\mathcal{E}$, $g$ and $h$ are cartesian in $\mathcal{D}$, and $s$ is cocartesian in $\mathcal{D}$, then $r$ is cocartesian in $\mathcal{D}$.

From a type-theoretic perspective, the first two conditions are rather straightforward. The first condition establishes that we have a type former $\coprod$ that can quantify over objects of $\mathcal{E}$. The second condition defines an introduction rule of the following form: $\frac{\Gamma, x : X \vdash a : A}{\Gamma \vdash \langle x, a \rangle : \coprod (x : X) A}$

The elimination rule comes from each $\langle\rangle$ being cocartesian, as cocartesian maps satisfy a mapping-out universal property, exactly like a coproduct should!

However, at a glance, the last condition is somewhat mysterious. It says that cocartesian maps over projections are stable: but what does that have to do with coproducts? This, like many other questions in category theory, is elucidated by thinking type-theoretically: A cartesian map in a comprehension category is essentially a substitution: the stability condition says that the introduction rule for coproducts is actually type-theoretic: stable under substitution.

record has-comprehension-coproducts : Type (ob β βb β od β βd β oe β βe) where
no-eta-equality
field
β : β {Ξ} β (x : E.Ob[ Ξ ]) (a : D.Ob[ Ξ β¨Ύ x ]) β D.Ob[ Ξ ]
: β {Ξ} β (x : E.Ob[ Ξ ]) (a : D.Ob[ Ξ β¨Ύ x ])
β D.Hom[ ΟαΆ ] a (β x a)
: β {Ξ} β (x : E.Ob[ Ξ ]) (a : D.Ob[ Ξ β¨Ύ x ])
β is-cocartesian D ΟαΆ β¨ x , a β©
cocartesian-stable
: β {Ξ Ξ x y a a' b b'} {Ο : Hom Ξ Ξ} {f : E.Hom[ Ο ] x y}
β {r : D.Hom[ ΟαΆ ] a a'} {h : D.Hom[ Ο ] a' b'}
β {g : D.Hom[ Ο β¨ΎΛ’ f ] a b} {s : D.Hom[ ΟαΆ ] b b'}
β is-cartesian E Ο f
β s D.ββ² g D.β‘[ sub-proj f ] h D.ββ² r
β is-cocartesian D ΟαΆ s
β is-cartesian D (Ο β¨ΎΛ’ f) g
β is-cartesian D Ο h
β is-cocartesian D ΟαΆ r

module β¨β©-cocartesian {Ξ} (x : E.Ob[ Ξ ]) (a : D.Ob[ Ξ β¨Ύ x ]) =
is-cocartesian (β¨β©-cocartesian x a)


Now, some general facts about coproducts. To start, note that forming coproducts is a functorial operation. The proof is very routine β if youβve seen one functoriality argument, youβve seen them all β so weβve hidden it from the page.1

  opaque
β[_]
: β {Ξ} {x : E.Ob[ Ξ ]} {a b : D.Ob[ Ξ β¨Ύ x ]}
β D.Hom[ id ] a b β D.Hom[ id ] (β x a) (β x b)
β[_] {Ξ} {x} {a} {b} f =
β¨β©-cocartesian.universalβ² x a id-comm-sym (β¨ x , b β© D.ββ² f)

β[]-id : β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} β β[ D.idβ² {x = a} ] β‘ D.idβ²
β[]-β
: β {Ξ} {x : E.Ob[ Ξ ]} {a b c : D.Ob[ Ξ β¨Ύ x ]}
β (f : D.Hom[ id ] b c) (g : D.Hom[ id ] a b)
β β[ f Dβ.β g ] D.β‘[ sym (idl _) ] β[ f ] D.ββ² β[ g ]

    β[]-natural
: β {Ξ} {x : E.Ob[ Ξ ]} {a b : D.Ob[ Ξ β¨Ύ x ]}
β (f : D.Hom[ id ] a b)
β β[ f ] D.ββ² β¨ x , a β© D.β‘[ id-comm-sym ] β¨ x , b β© D.ββ² f
β[]-natural {x = x} {a} {b} f =
β¨β©-cocartesian.commutesp x a _ _

β[]-id {x = x} {a = a} =
sym $β¨β©-cocartesian.unique _ _ _$ from-pathpβ» $Dr.cast[]$
D.idβ² D.ββ² β¨ x , a β© D.β‘[]β¨ D.idlβ² _ β©D.β‘[]
β¨ x , a β©            D.β‘[]β¨ symP (D.idrβ² _ ) β©D.β‘[]
β¨ x , a β© D.ββ² D.idβ² β

β[]-β {x = x} {a = a} {b = b} {c = c} f g =
symP $β¨β©-cocartesian.uniquep x a _ _ _ _$
(β[ f ] D.ββ² β[ g ]) D.ββ² β¨ x , a β©          D.β‘[]β¨ Dr.pullr[] _ (β[]-natural g) β©D.β‘[]
β[ f ] D.ββ² β¨ x , b β© D.ββ² g                 D.β‘[]β¨ Dr.extendl[] _ (β[]-natural f) β©D.β‘[]
β¨ x , c β© D.ββ² f D.ββ² g                      D.β‘[]β¨ to-pathp (Dr.unwhisker-r (ap (ΟαΆ β_) (idl _)) (idl _)) β©D.β‘[]
β¨ x , c β© D.ββ² (f Dβ.β g) β


We can also re-package the cocartesianness of $\langle\rangle$ to give a method for constructing morphisms $\coprod_{X} A \to B$ given morphisms $A \to \pi^{*}(B)$. Type theoretically, this gives a much more familiar presentation of the elimination rule.

  opaque
β-elim
: β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β D.Hom[ id ] a (Ο*.Fβ x b)
β D.Hom[ id ] (β x a) b
β-elim {x = x} {a = a} {b = b} f =
β¨β©-cocartesian.universalβ² x a id-comm-sym (D-fib.lifting ΟαΆ b D.ββ² f)

β-elim-Ξ²
: β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β (f : D.Hom[ id ] a (Ο*.Fβ x b))
β β-elim f D.ββ² β¨ x , a β© D.β‘[ id-comm-sym ] D-fib.lifting ΟαΆ b D.ββ² f
β-elim-Ξ² f = β¨β©-cocartesian.commutesp _ _ _ _


Putting on our type-theorist goggles, weβre still missing one thing to call this a proper elimination rule: stability under substitution. In the categorical world, thatβs satisfied by the proof that the operation we just constructed is natural, given below.

    β-elim-natural
: β {Ξ} {x : E.Ob[ Ξ ]} {a b : D.Ob[ Ξ β¨Ύ x ]} {c : D.Ob[ Ξ ]}
β (f : D.Hom[ id ] b (Ο*.β x c)) (g : D.Hom[ id ] a b)
β β-elim f D.ββ² β[ g ] D.β‘[ idl _ ] β-elim (f Dβ.β g)
β-elim-natural {x = x} {a = a} {b = b} {c = c} f g =
β¨β©-cocartesian.uniquep x a _ _ _ (β-elim f D.ββ² β[ g ]) $((β-elim f) D.ββ² β[ g ]) D.ββ² β¨ x , a β© D.β‘[]β¨ Dr.pullr[] _ (β[]-natural g) β©D.β‘[] β-elim f D.ββ² β¨ x , b β© D.ββ² g D.β‘[]β¨ Dr.extendl[] id-comm-sym (β¨β©-cocartesian.commutesp x b _ _) β©D.β‘[] D-fib.lifting ΟαΆ c D.ββ² f D.ββ² g D.β‘[]β¨ to-pathp (Dr.unwhisker-r (ap (ΟαΆ β_) (idl _)) (idl _)) β©D.β‘[] D-fib.lifting ΟαΆ c D.ββ² Dr.hom[] (f D.ββ² g) β  Conversely, we can make maps $A \to \pi^{*}(B)$ given maps $\coprod_{X} A \to B$. This isnβt quite, type-theoretically, as the elimination principle: itβs a weird mash-up of the introduction rule for coproducts, followed by substitution.  opaque β-transpose : β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]} β D.Hom[ id ] (β x a) b β D.Hom[ id ] a (Ο*.β x b) β-transpose {x = x} {a = a} {b = b} f = D-fib.universalβ² ΟαΆ b id-comm (f D.ββ² β¨ x , a β©)   opaque unfolding β-transpose β-transpose-weaken : β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]} β (f : D.Hom[ id ] (β x a) b) β D-fib.lifting ΟαΆ b D.ββ² β-transpose f D.β‘[ id-comm ] f D.ββ² β¨ x , a β© β-transpose-weaken f = D-fib.commutesp ΟαΆ _ id-comm _  While β-transpose may not play an obvious type-theoretic role, it is extremely important categorically, since it is an inverse of β-elim! Moreover, itβs also natural, but that proof is also hidden from the page for brevity.  opaque unfolding β-elim β-transpose β-elim-transpose : β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]} β (f : D.Hom[ id ] (β x a) b) β β-elim (β-transpose f) β‘ f β-elim-transpose {x = x} {a = a} {b = b} f = sym$
β¨β©-cocartesian.uniquep x a _ _ _ f $symP$
D-fib.commutesp ΟαΆ b id-comm (f D.ββ² β¨ x , a β©)

β-transpose-elim
: β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β (f : D.Hom[ id ] a (Ο*.Fβ x b))
β β-transpose (β-elim f) β‘ f
β-transpose-elim {x = x} {a = a} {b = b} f = sym $D-fib.uniquep ΟαΆ b _ _ _ f$ symP $β¨β©-cocartesian.commutesp x a id-comm-sym (D-fib.lifting ΟαΆ b D.ββ² f)   β-transpose-equiv : β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b : D.Ob[ Ξ ]} β is-equiv (β-transpose {a = a} {b = b}) β-transpose-equiv = is-isoβis-equiv$
iso β-elim β-transpose-elim β-elim-transpose

opaque
unfolding β-transpose
β-transpose-naturall
: β {Ξ} {x : E.Ob[ Ξ ]} {a b : D.Ob[ Ξ β¨Ύ x ]} {c : D.Ob[ Ξ ]}
β (f : D.Hom[ id ] (β x b) c) (g : D.Hom[ id ] a b)
β β-transpose f D.ββ² g D.β‘[ idl _ ] β-transpose (f Dβ.β β[ g ])
β-transpose-naturall {x = x} {a = a} {b = b} {c = c} f g =
D-fib.uniquep ΟαΆ c _ _ _ (β-transpose f D.ββ² g) $D-fib.lifting ΟαΆ c D.ββ² β-transpose f D.ββ² g D.β‘[]β¨ Dr.pulll[] id-comm (D-fib.commutesp ΟαΆ c _ _) β©D.β‘[] (f D.ββ² β¨ x , b β©) D.ββ² g D.β‘[]β¨ Dr.extendr[] _ (symP (β[]-natural g)) β©D.β‘[] (f D.ββ² β[ g ]) D.ββ² β¨ x , a β© D.β‘[ ap (_β ΟαΆ) (idl _) ]β¨ to-pathp (Dr.unwhisker-l (ap (_β ΟαΆ) (idl _)) (idl _)) β©] (f Dβ.β β[ g ]) D.ββ² β¨ x , a β© β β-transpose-naturalr : β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ β¨Ύ x ]} {b c : D.Ob[ Ξ ]} β (f : D.Hom[ id ] b c) (g : D.Hom[ id ] (β x a) b) β Ο*.β x f D.ββ² β-transpose g D.β‘[ idl _ ] β-transpose (f Dβ.β g) β-transpose-naturalr {x = x} {a = a} {b = b} {c = c} f g = D-fib.uniquep ΟαΆ c _ _ _ (Ο*.Fβ x f D.ββ² β-transpose g)$
D-fib.lifting ΟαΆ c D.ββ² Ο*.β x f D.ββ² β-transpose g     D.β‘[]β¨ Dr.pulll[] _ (D-fib.commutesp ΟαΆ c id-comm _) β©D.β‘[]
(f D.ββ² D-fib.lifting ΟαΆ b) D.ββ² β-transpose g          D.β‘[]β¨ Dr.extendr[] id-comm (D-fib.commutesp ΟαΆ b _ _) β©D.β‘[]
(f D.ββ² g) D.ββ² β¨ x , a β©                               D.β‘[ ap (_β ΟαΆ) (idl _) ]β¨ to-pathp (Dr.unwhisker-l (ap (_β ΟαΆ) (idl _)) (idl _)) β©]
Dr.hom[ idl id ] (f D.ββ² g) D.ββ² β¨ x , a β©              β


Next, we define an introduction rule for coproducts that also lets us apply a mediating substitution:

  opaque
: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ}
β (f : E.Hom[ Ο ] x y) (a : D.Ob[ Ξ β¨Ύ y ])
β D.Hom[ ΟαΆ ] (D*.β (Ο β¨ΎΛ’ f) a) (D*.β Ο (β y a))

β¨_β¨Ύ_β© {x = x} {y = y} {Ο = Ο} f a =
D-fib.universalβ² Ο (β y a) (sym (sub-proj f)) \$
β¨ y , a β© D.ββ² D-fib.lifting (Ο β¨ΎΛ’ f) a

: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ}
β (f : E.Hom[ Ο ] x y) (a : D.Ob[ Ξ β¨Ύ y ])
β D-fib.lifting Ο (β y a) D.ββ² β¨ f β¨Ύ a β©
D.β‘[ sym (sub-proj f) ] β¨ y , a β© D.ββ² D-fib.lifting (Ο β¨ΎΛ’ f) a

β¨β¨Ύβ©-weaken {y = y} {Ο = Ο} f a =
D-fib.commutesp Ο (β y a) (symP (sub-proj f)) _


Because we have assumed that cocartesian maps are stable when pulled back along cartesian maps over projections2, this map is also cocartesian β and, you guessed it β the spiced-up introduction rule is also natural.

  opaque
: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ} β {f : E.Hom[ Ο ] x y}
β is-cartesian E Ο f β (a : D.Ob[ Ξ β¨Ύ y ])
β is-cocartesian D ΟαΆ β¨ f β¨Ύ a β©
β¨β¨Ύβ©-cocartesian {x = x} {y = y} {Ο = Ο} {f = f} cart a =
cocartesian-stable cart
(symP (β¨β¨Ύβ©-weaken f a))
(D-fib.cartesian (Ο β¨ΎΛ’ f) a)
(D-fib.cartesian Ο (β y a))

{Ξ Ξ x y} {Ο : Hom Ξ Ξ} {f : E.Hom[ Ο ] x y}
(cart : is-cartesian E Ο f) (a : D.Ob[ Ξ β¨Ύ y ])
= is-cocartesian (β¨β¨Ύβ©-cocartesian cart a)

  opaque
: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ}
β {a b : D.Ob[ Ξ β¨Ύ y ]}
β (f : D.Hom[ id ] a b) (g : E.Hom[ Ο ] x y)
β β¨ g β¨Ύ b β© D.ββ² D*.β (Ο β¨ΎΛ’ g) f D.β‘[ id-comm ] D*.β Ο β[ f ] D.ββ² β¨ g β¨Ύ a β©
β¨β¨Ύβ©-natural {x = x} {y = y} {Ο = Ο} {a = a} {b = b} f g =
D-fib.uniquepβ Ο (β y b) _ _ _ _ _
(Dr.pulll[] _ (D-fib.commutesp Ο (β y b) (sym (sub-proj g)) _)
D.β[] Dr.pullr[] _ (D-fib.commutesp (Ο β¨ΎΛ’ g) b id-comm _))
(Dr.pulll[] _ (D-fib.commutesp Ο (β y b) id-comm _)
D.β[] Dr.pullr[] _ (β¨β¨Ύβ©-weaken g a)
D.β[] Dr.extendl[] _ (β[]-natural f))


This lets us extend a substitution $\Gamma, X \to \Delta, Y$ into a substitution

$\sigma^*(\textstyle\coprod_{Y}A) \to \textstyle\coprod_{(\sigma, f)^{*}(X)} A\text{.}$

  opaque
β-sub
: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ} {f : E.Hom[ Ο ] x y}
β is-cartesian E Ο f β (a : D.Ob[ Ξ β¨Ύ y ])
β D.Hom[ id ] (D*.β Ο (β y a)) (β x (D*.β (Ο β¨ΎΛ’ f) a))
β-sub {x = x} {Ο = Ο} {f = f} cart a =
β¨β¨Ύβ©-cocartesian.universalv cart a β¨ x , (D*.β (Ο β¨ΎΛ’ f) a) β©

: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ} {f : E.Hom[ Ο ] x y}
β (cart : is-cartesian E Ο f) β (a : D.Ob[ Ξ β¨Ύ y ])
β β-sub cart a D.ββ² β¨ f β¨Ύ a β© D.β‘[ idl _ ] β¨ x , (D*.β (Ο β¨ΎΛ’ f) a) β©
β-sub-β¨β¨Ύβ© cart a =
β¨β¨Ύβ©-cocartesian.commutesv cart a _

β-sub-natural
: β {Ξ Ξ x y} {Ο : Hom Ξ Ξ} {f : E.Hom[ Ο ] x y}
β {a b : D.Ob[ Ξ β¨Ύ y ]}
β (cart : is-cartesian E Ο f)
β (g : D.Hom[ id ] a b)
β β-sub cart b D.ββ² D*.β Ο β[ g ] β‘ β[ D*.β (Ο β¨ΎΛ’ f) g ] D.ββ² β-sub cart a
β-sub-natural {x = x} {y = y} {Ο = Ο} {f = f} {a = a} {b = b} cart g =
β¨β¨Ύβ©-cocartesian.uniquepβ cart a _ _ _ _ _
(Dr.pullr[] _ (symP (β¨β¨Ύβ©-natural g f))
D.β[] Dr.pulll[] _ (β¨β¨Ύβ©-cocartesian.commutesv cart b _))
(Dr.pullr[] _ (β¨β¨Ύβ©-cocartesian.commutesv cart a _)
D.β[] β[]-natural (D*.β (Ο β¨ΎΛ’ f) g))


1. As a reminder, you can choose to toggle hidden code on the sidebar.β©οΈ

2. what a mouthful!β©οΈ