module Cubical.Categories.LocallySmall.Instances.BinProduct.Properties where


open import Cubical.Data.Sigma
open import Cubical.Data.Sigma.More

open import Cubical.Categories.LocallySmall.Category.Base
open import Cubical.Categories.LocallySmall.Variables
open import Cubical.Categories.LocallySmall.Functor
open import Cubical.Categories.LocallySmall.Instances.BinProduct.Base

open Category
open Σω
open Functor

module _
  {C : Category Cob CHom-ℓ}
  {D : Category Dob DHom-ℓ}
  {E : Category Eob EHom-ℓ}
  where
  _,F_ : Functor C D → Functor C E → Functor C (D ×C E)
  (F ,F G) .F-ob = λ z → F-ob F z , F-ob G z
  (F ,F G) .F-hom = λ z → F-hom F z , F-hom G z
  (F ,F G) .F-id = ≡-× (F-id F) (F-id G)
  (F ,F G) .F-seq _ _ = ≡-× (F-seq F _ _) (F-seq G _ _)

module _
  {Bob BHom-ℓ}
  {B : Category Bob BHom-ℓ}
  {C : Category Cob CHom-ℓ}
  {D : Category Dob DHom-ℓ}
  {E : Category Eob EHom-ℓ}
  where
  _×F_ : Functor B D → Functor C E → Functor (B ×C C) (D ×C E)
  F ×F G = (F ∘F π₁ _ _) ,F (G ∘F π₂ _ _)