module Cat.Displayed.Instances.TotalProduct
  {o₁ ℓ₁ oβ‚‚ β„“β‚‚ o₃ ℓ₃ oβ‚„ β„“β‚„}
  (C : Precategory o₁ ℓ₁)
  (D : Precategory oβ‚‚ β„“β‚‚)
  (EC : Displayed C o₃ ℓ₃) (ED : Displayed D oβ‚„ β„“β‚„) where
  private module EC = Displayed EC
  private module ED = Displayed ED

The total product of displayed categoriesπŸ”—

If E→B\mathcal{E}\to \mathcal{B} and q:D→Cq :\mathcal{D} \to \mathcal{C} are displayed categories, then we can define their total product E×D→B×C\mathcal{E}\times \mathcal{D}\to \mathcal{B}\times \mathcal{C}, which is again a displayed category.

  _Γ—α΅€α΄°_ : Displayed (C Γ—αΆœ D) (o₃ βŠ” oβ‚„) (ℓ₃ βŠ” β„“β‚„)
If displayed categories are regarded as functors, then the product of displayed categories can be regarded as the usual product of functors.
  _Γ—α΅€α΄°_ .Displayed.Ob[_] (p₁ , pβ‚‚) =
   EC.Ob[ p₁ ]  Γ— ED.Ob[ pβ‚‚ ] 
  _Γ—α΅€α΄°_ .Displayed.Hom[_] (f₁ , fβ‚‚) (c₁ , cβ‚‚) (d₁ , dβ‚‚) =
    EC.Hom[ f₁ ] c₁ d₁ Γ—
    ED.Hom[ fβ‚‚ ] cβ‚‚ dβ‚‚
  _Γ—α΅€α΄°_ .Displayed.id' = (EC.id' , ED.id')

We establish that the hom sets of the product fibration are actually sets.

If x,y:Ob⁑[CΓ—D]x, y : \operatorname{Ob}[C \times D] (so x=(xC,xD),y=(yC,yD)x = (x_C, x_D), y = (y_C, y_D)) and f:xβ†’yf : x \to y (so ff is (fC,fD)(f_C, f_D)) then for any two morphisms f1,f2f_1,f_2 lying over ff, and any p,q:f1=f2p, q : f_1 = f_2, p=qp=q.

  _Γ—α΅€α΄°_ .Displayed.Hom[_]-set (f₁ , fβ‚‚) (x'₁ , x'β‚‚) (y'₁ , y'β‚‚) =
    Γ—-is-hlevel 2
    (EC.Hom[ f₁ ]-set x'₁ y'₁) (ED.Hom[ fβ‚‚ ]-set x'β‚‚ y'β‚‚)
Composition is pairwise.
  _Γ—α΅€α΄°_ .Displayed._∘'_ (f₁ , fβ‚‚) (g₁ , gβ‚‚) =
    EC._∘'_ f₁ g₁ , ED._∘'_ fβ‚‚ gβ‚‚

Associativity and left/right identity laws hold because they hold for the components of the ordered pairs.

  _Γ—α΅€α΄°_ .Displayed.idr' (f₁ , fβ‚‚) = EC.idr' f₁ ,β‚š ED.idr' fβ‚‚
  _Γ—α΅€α΄°_ .Displayed.idl' (f₁ , fβ‚‚) = EC.idl' f₁ ,β‚š ED.idl' fβ‚‚
  _Γ—α΅€α΄°_ .Displayed.assoc' (f₁ , fβ‚‚) (g₁ , gβ‚‚) (h₁ , hβ‚‚) =
    EC.assoc' f₁ g₁ h₁ ,β‚š ED.assoc' fβ‚‚ gβ‚‚ hβ‚‚