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 _))