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 and are displayed categories, then we can define their total product 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β‚‚
  _Γ—α΅€α΄°_' = (' ,')

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

If (so and (so is then for any two morphisms lying over and any

  _Γ—α΅€α΄°_ .Displayed.Hom[_]-set _ _ _ = hlevel 2
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β‚‚