open import Cat.Displayed.Comprehension.Coproduct
open import Cat.Displayed.Comprehension
open import Cat.Displayed.Cartesian
open import Cat.Morphism.Orthogonal
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Displayed.Comprehension.Coproduct.Strong where


# Strong comprehension coproductsπ

Let and be a pair of comprehension categories over the same base category such that has coproducts over Type theoretically, this (roughly) corresponds to a type theory with a pair of syntactic categories (for instance, types and kinds), along with mixed-mode types.

We can model this using coproducts over a comprehension category, but the elimination principle we get from this setup is pretty weak: we really only have a recursion principle, not an elimination principle. That has to be be captured through an extra condition.

We say that a comprehension category has strong comprehension coproducts if (it has comprehension coproducts, and) the canonical substitution forms an orthogonal factorisation system with the weakening maps In more elementary terms, this means that any square diagram, as below, has a unique diagonal filler.

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

  strong-comprehension-coproducts : Type _
strong-comprehension-coproducts =
β {Ξ Ξ} (x : E.Ob[ Ξ ]) (a : D.Ob[ Ξ Q.β¨Ύ x ]) (b : D.Ob[ Ξ ])
β mβ₯m B (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) (P.ΟαΆ {x = b})

  record make-strong-comprehension-coproducts : Type (ob β βb β od β oe) where
no-eta-equality
field
β-strong-elim
: β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β (Ο : Hom (Ξ P.β¨Ύ β x a) Ξ) (Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b))
β Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½
β Hom (Ξ P.β¨Ύ β x a) (Ξ P.β¨Ύ b)
β-strong-Ξ²
: β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β {Ο : Hom (Ξ P.β¨Ύ β x a) Ξ} {Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)}
β (p : Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½)
β β-strong-elim Ο Ξ½ p β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ Ξ½
β-strong-sub
: β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β {Ο : Hom (Ξ P.β¨Ύ β x a) Ξ} {Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)}
β (p : Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½)
β P.ΟαΆ β β-strong-elim Ο Ξ½ p β‘ Ο
β-strong-Ξ·
: β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]}
β {Ο : Hom (Ξ P.β¨Ύ β x a) Ξ} {Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)}
β (p : Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½)
β (other : Hom (Ξ P.β¨Ύ β x a) (Ξ P.β¨Ύ b))
β other β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ Ξ½
β P.ΟαΆ β other β‘ Ο
β other β‘ β-strong-elim Ο Ξ½ p

to-strong-comprehension-coproducts
: make-strong-comprehension-coproducts
β strong-comprehension-coproducts
to-strong-comprehension-coproducts mk x a b {u = u} {v = v} p =
contr (β-strong-elim _ _ p , β-strong-Ξ² p , β-strong-sub p) Ξ» w β
Ξ£-prop-path! $sym (β-strong-Ξ· p (w .fst) (w .snd .fst) (w .snd .snd)) where open make-strong-comprehension-coproducts mk  Thatβs a very concise definition: too concise. Letβs dig a bit deeper. module 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) (strong : 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  In the diagram, is a type in some context and we have a substitution β but, for intuition, we might as well zap to the identity: is a type in context In this simplified setting, the top morphism must be entirely determined by a βtermβ for the outer square to commute. Then, we see that the diagonal filler is exactly an elimination principle: since it too commutes with weakening, it must be determined by a βtermβ However, note that this elimination principle does not allow us to eliminate an arbitrary object from which corresponds type-theoretically having no elimination. This large elimination is captured by very strong comprehension coproducts, which are extremely rare.  opaque β-strong-elim : β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]} β (Ο : Hom (Ξ P.β¨Ύ β x a) Ξ) (Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)) β Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½ β Hom (Ξ P.β¨Ύ β x a) (Ξ P.β¨Ύ b) β-strong-elim {x = x} {a = a} {b = b} Ο Ξ½ p = strong x a b p .centre .fst  The upper-left triangle of the diagram gives us our law; eliminating out of a substitution extended with an introduction form gives us the original substitution.  opaque unfolding β-strong-elim β-strong-Ξ² : β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]} β {Ο : Hom (Ξ P.β¨Ύ β x a) Ξ} {Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)} β (p : Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½) β β-strong-elim Ο Ξ½ p β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ Ξ½ β-strong-Ξ² p = strong _ _ _ p .centre .snd .fst  The lower-right triangle describes how substitution interacts with eliminators; if we forget the thing we just eliminated into, then we recover the substitution from  β-strong-sub : β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]} β {Ο : Hom (Ξ P.β¨Ύ β x a) Ξ} {Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)} β (p : Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½) β P.ΟαΆ β β-strong-elim Ο Ξ½ p β‘ Ο β-strong-sub p = strong _ _ _ p .centre .snd .snd  Finally, uniqueness gives us an any other substitution that walks like the eliminator and quacks like the eliminator is the eliminator.  β-strong-Ξ· : β {Ξ Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]} {b : D.Ob[ Ξ ]} β {Ο : Hom (Ξ P.β¨Ύ β x a) Ξ} {Ξ½ : Hom (Ξ Q.β¨Ύ x P.β¨Ύ a) (Ξ P.β¨Ύ b)} β (p : Ο β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ P.ΟαΆ β Ξ½) β (other : Hom (Ξ P.β¨Ύ β x a) (Ξ P.β¨Ύ b)) β other β (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) β‘ Ξ½ β P.ΟαΆ β other β‘ Ο β other β‘ β-strong-elim Ο Ξ½ p β-strong-Ξ· p other Ξ² sub = ap fst (sym$ strong _ _ _ p .paths (other , Ξ² , sub))


Now, for some useful lemmas. If we eliminate by simply packaging up the data into a pair, then weβve done nothing. Categorically, this means the unique filler of the following diagram is the identity morphism.

    β-strong-id
: β {Ξ} {x : E.Ob[ Ξ ]} {a : D.Ob[ Ξ Q.β¨Ύ x ]}
β β-strong-elim P.ΟαΆ (Q.ΟαΆ P.β¨ΎΛ’ β¨ x , a β©) refl β‘ id
β-strong-id = sym (β-strong-Ξ· refl id (idl _) (idr _))