open import Cat.Displayed.Diagram.Total.Terminal
open import Cat.Diagram.Product
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Cartesian
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Reasoning

module Cat.Displayed.Diagram.Total.Product where

open ∫Hom

Total products🔗

module _ {ob ℓb oe ℓe} {B : Precategory ob ℓb} (E : Displayed B oe ℓe) where
  open Cat.Displayed.Reasoning E
  open Cat.Reasoning B

  private variable
    a x y p     : Ob
    a' x' y' p' : Ob[ a ]
    f g other   : Hom a x
    f' g'       : Hom[ f ] a' x'

Let $\mathcal{E}\mathcal{B}$ be a displayed category, and $X\stackrel{{\pi }_1}{\leftarrow }P\stackrel{{\pi }_2}{\to }Y$ be a product diagram in $\mathcal{B}\text{.}$ A total diagram in $\mathcal{E}$ is a diagram

satisfying a displayed version of the universal property of products.

  record is-product-over
      {π₁ : Hom p x} {π₂ : Hom p y} (prod : is-product B π₁ π₂)
      (π₁' : Hom[ π₁ ] p' x') (π₂' : Hom[ π₂ ] p' y') : Type (ob ⊔ ℓb ⊔ oe ⊔ ℓe)
    where

    no-eta-equality
    open is-product prod

More explicitly, suppose that we had a triple $(A^{\prime },f^{\prime },g^{\prime })$ displayed over $(A,f,g)\text{,}$ as in the following diagram.

$P$ is a product, so there exists a unique $⟨f,g⟩:A\to P$ that commutes with ${\pi }_1$ and ${\pi }_2\text{.}$

This leaves a conspicuous gap in the upstairs portion of the diagram between $A^{\prime }$ and $P^{\prime }\text{;}$ $(P^{\prime },{\pi }_1^{\prime },{\pi }_2^{\prime })$ is a total product precisely when we have a unique lift of $⟨f,g⟩$ that commutes with ${\pi }_1^{\prime }$ and ${\pi }_2^{\prime }\text{.}$

    field
      ⟨_,_⟩'
        : (f' : Hom[ f ] a' x') (g' : Hom[ g ] a' y')
        → Hom[ ⟨ f , g ⟩ ] a' p'

      π₁∘⟨⟩' : π₁' ∘' ⟨ f' , g' ⟩' ≡[ π₁∘⟨⟩ ] f'
      π₂∘⟨⟩' : π₂' ∘' ⟨ f' , g' ⟩' ≡[ π₂∘⟨⟩ ] g'

      unique'
        : {p1 : π₁ ∘ other ≡ f} {p2 : π₂ ∘ other ≡ g}
        → {other' : Hom[ other ] a' p'}
        → (p1' : (π₁' ∘' other') ≡[ p1 ] f')
        → (p2' : (π₂' ∘' other') ≡[ p2 ] g')
        → other' ≡[ unique p1 p2 ] ⟨ f' , g' ⟩'

    opaque
      ⟨_,_⟩ₚ
        : (f' : Hom[ π₁ ∘ f ] a' x') (g' : Hom[ π₂ ∘ f ] a' y')
        → Hom[ f ] a' p'
      ⟨ f' , g' ⟩ₚ = hom[ sym (unique refl refl) ] ⟨ f' , g' ⟩'

      abstract
        π₁∘⟨⟩ₚ : π₁' ∘' ⟨ f' , g' ⟩ₚ ≡ f'
        π₁∘⟨⟩ₚ = whisker-r _ ∙ reindex _ _ ∙ from-pathp π₁∘⟨⟩'

        π₂∘⟨⟩ₚ : π₂' ∘' ⟨ f' , g' ⟩ₚ ≡ g'
        π₂∘⟨⟩ₚ = whisker-r _ ∙ reindex _ _ ∙ from-pathp π₂∘⟨⟩'

A total product of $A^{\prime }$ and $B^{\prime }$ in $\mathcal{E}$ consists of a choice of a total product diagram.

  record
    ProductP {x y} (prod : Product B x y) (x' : Ob[ x ]) (y' : Ob[ y ])
      : Type (ob ⊔ ℓb ⊔ oe ⊔ ℓe) where

    no-eta-equality
    open Product prod

    field
      apex' : Ob[ apex ]
      π₁'   : Hom[ π₁ ] apex' x'
      π₂'   : Hom[ π₂ ] apex' y'
      has-is-product'
        : is-product-over has-is-product π₁' π₂'

    open is-product-over has-is-product' public

has-products-over
  : ∀ {o ℓ o' ℓ'} {B : Precategory o ℓ}
  → Displayed B o' ℓ'
  → has-products B
  → Type _
has-products-over {B = B} E prod = ∀ {a b : ⌞ B ⌟} (x : E ʻ a) (y : E ʻ b) → ProductP E (prod a b) x y

Total products and total categories🔗

module _ {ob ℓb oe ℓe} {B : Precategory ob ℓb} {E : Displayed B oe ℓe} where
  open Cat.Reasoning B
  open Displayed E

  private module ∫E = Cat.Reasoning (∫ E)

As the name suggests, a total product diagram in $\mathcal{E}$ induces to a product diagram in the total category of $\mathcal{E}\text{.}$

  is-total-product→total-is-product
    : ∀ {x y p} {x' : Ob[ x ]} {y' : Ob[ y ]} {p' : Ob[ p ]}
    → {π₁ : ∫E.Hom (p , p') (x , x')} {π₂ : ∫E.Hom (p , p') (y , y')}
    → {prod : is-product B (π₁ .fst) (π₂ .fst)}
    → is-product-over E prod (π₁ .snd) (π₂ .snd)
    → is-product (∫ E) π₁ π₂

  is-total-product→total-is-product {π₁ = π₁} {π₂ = π₂} {prod = prod} total-prod = ∫prod where
    open is-product-over total-prod
    open is-product prod

    ∫prod : is-product (∫ E) π₁ π₂
    ∫prod .is-product.⟨_,_⟩ f g =
      ∫hom ⟨ f .fst , g .fst ⟩ ⟨ f .snd , g .snd ⟩'
    ∫prod .is-product.π₁∘⟨⟩ =
      ∫Hom-path E π₁∘⟨⟩ π₁∘⟨⟩'
    ∫prod .is-product.π₂∘⟨⟩ =
      ∫Hom-path E π₂∘⟨⟩ π₂∘⟨⟩'
    ∫prod .is-product.unique p1 p2 =
      ∫Hom-path E
        (unique (ap fst p1) (ap fst p2))
        (unique' (ap snd p1) (ap snd p2))

Warning

Note that a product diagram in a total category does not necessarily yield a product diagram in the base category. For a counterexample, consider the following displayed category:

The total category is equivalent to the terminal category, and thus has products. However, the base category does not have products, as the uniqueness condition fails!

module
  Binary-products'
    {o ℓ o' ℓ'} {B : Precategory o ℓ} {E : Displayed B o' ℓ'} {fp : has-products B}
    (fp' : has-products-over E fp)
  where

  open Precategory B

  module _ {a b : Ob} (a' : E ʻ a) (b' : E ʻ b) where open ProductP (fp' a' b') renaming (apex' to _⊗₀'_) using () public
  module _ {a b : Ob} {a' : E ʻ a} {b' : E ʻ b} where open ProductP (fp' a' b') renaming (unique' to ⟨⟩'-unique) hiding (apex') public

record
  Cartesian-over
    {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') (cart : Cartesian-category B)
    : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ')
  where

  private module cart = Cartesian-category cart

  field
    terminal' : TerminalP E cart.terminal
    products' : has-products-over E cart.products

  open TerminalP terminal' hiding (has⊤') public
  open Binary-products' products' public