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

import Cat.Reasoning

module Cat.Displayed.Diagram.Total.Product where

open Total-hom

Total Products🔗

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

  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 $E B$ be a displayed category, and $P, π_{1} : P \to X, π_{2} : P \to Y$ be a product diagram in $B .$ A diagram $P^{'}, π_{1}^{'}, π_{2}^{'}$ of the shape

is a total product diagram if it satisfies a displayed version of the universal property of the product.

  record is-total-product
      {π₁ : 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^{'}, f^{'}, g^{'})$ displayed over $(A, f, g),$ as in the following diagram.

$P$ is a product, so there exists a unique $⟨ f, g ⟩ : A \to P$ that commutes with $π_{1}$ and $π_{2} .$

This leaves a conspicuous gap in the upstairs portion of the diagram between $A^{'}$ and $P^{'};$ $(P^{'}, π_{1}^{'}, π_{2}^{'})$ is a total product precisely when we have a unique lift of $⟨ f, g ⟩$ that commutes with $π_{1}^{'}$ and $π_{2}^{'} .$

      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' ⟩'

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

  record Total-product
    {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-total-product : is-total-product has-is-product π₁' π₂'

    open is-total-product has-is-total-product

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 $E$ induces to a product diagram in the total category of $E .$

  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 (π₁ .hom) (π₂ .hom)}
    → is-total-product E prod (π₁ .preserves) (π₂ .preserves)
    → is-product (∫ E) π₁ π₂

The proof is largely shuffling data about, so we elide the details.

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

    ∫prod : is-product (∫ E) π₁ π₂
    ∫prod .is-product.⟨_,_⟩ f g =
      total-hom ⟨ f .hom , g .hom ⟩ ⟨ f .preserves , g .preserves ⟩'
    ∫prod .is-product.π₁∘⟨⟩ =
      total-hom-path E π₁∘⟨⟩ π₁∘⟨⟩'
    ∫prod .is-product.π₂∘⟨⟩ =
      total-hom-path E π₂∘⟨⟩ π₂∘⟨⟩'
    ∫prod .is-product.unique p1 p2 =
      total-hom-path E
        (unique (ap hom p1) (ap hom p2))
        (unique' (ap preserves p1) (ap preserves 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!