Definition of cartesian monoidal structure for categories with finite products.

Cubical/Categories/Limits/BinProduct.agda

@@ -34,9 +34,53 @@ module _ (C : Category ℓ ℓ') where
       binProdPr₂ : Hom[ binProdOb , y ]
       univProp : isBinProduct binProdPr₁ binProdPr₂
 
+    binProdArrow : {z : ob} -> Hom[ z , x ] -> Hom[ z , y ] -> Hom[ z , binProdOb ]
+    binProdArrow f g = univProp f g .fst .fst
+
+    binProdArrowUnique : {z : ob} {f : Hom[ z , x ]} {g : Hom[ z , y ]} {h : Hom[ z , binProdOb ]}
+      -> h ⋆ binProdPr₁ ≡ f -> h ⋆ binProdPr₂ ≡ g -> binProdArrow f g ≡ h
+    binProdArrowUnique {f = f} {g = g} {h = h} p q i = univProp f g .snd (h , p , q) i .fst
+
+    -- Beta rules for products:
+
+    binProdArrowPr₁ : {z : ob} {f : Hom[ z , x ]} {g : Hom[ z , y ]} -> binProdArrow f g ⋆ binProdPr₁ ≡ f
+    binProdArrowPr₁ {f = f} {g = g} = univProp f g .fst .snd .fst
+
+    binProdArrowPr₂ : {z : ob} {f : Hom[ z , x ]} {g : Hom[ z , y ]} -> binProdArrow f g ⋆ binProdPr₂ ≡ g
+    binProdArrowPr₂ {f = f} {g = g} = univProp f g .fst .snd .snd
+
 
   BinProducts : Type (ℓ-max ℓ ℓ')
   BinProducts = (x y : ob) → BinProduct x y
 
   hasBinProducts : Type (ℓ-max ℓ ℓ')
   hasBinProducts = ∥ BinProducts ∥₁
+
+  module BinProducts (prod : BinProducts) where
+    open module AllProductsExpl (x y : ob) = BinProduct (prod x y) public using (binProdOb; univProp)
+    open module AllProductsImpl {x y : ob} = BinProduct (prod x y) public hiding (binProdOb; univProp)
+
+    private
+      variable
+        x y z w x' y' : ob
+        f g h k : Hom[ x , y ]
+
+    binProdMap : Hom[ x , x' ] -> Hom[ y , y' ] -> Hom[ binProdOb x y , binProdOb x' y' ]
+    binProdMap f g = binProdArrow (binProdPr₁ ⋆ f) (binProdPr₂ ⋆ g)
+
+    binProdArrowCompLeft : h ⋆ binProdArrow f g ≡ binProdArrow (h ⋆ f) (h ⋆ g)
+    binProdArrowCompLeft = sym (binProdArrowUnique
+      (⋆Assoc _ _ _ ∙ ⟨ refl ⟩⋆⟨ binProdArrowPr₁ ⟩)
+      (⋆Assoc _ _ _ ∙ ⟨ refl ⟩⋆⟨ binProdArrowPr₂ ⟩))
+
+    binProdArrowCompRight : (binProdArrow f g) ⋆ (binProdMap h k) ≡ binProdArrow (f ⋆ h) (g ⋆ k)
+    binProdArrowCompRight = sym (binProdArrowUnique
+      ( ⋆Assoc _ _ _
+      ∙ cong (_ ⋆_) binProdArrowPr₁
+      ∙ sym (⋆Assoc _ _ _)
+      ∙ cong (_⋆ _) binProdArrowPr₁ )
+
+      ( ⋆Assoc _ _ _
+      ∙ cong (_ ⋆_) binProdArrowPr₂
+      ∙ sym (⋆Assoc _ _ _)
+      ∙ cong (_⋆ _) binProdArrowPr₂ ) )

Cubical/Categories/Monoidal/Cartesian.agda

@@ -0,0 +1,223 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Monoidal.Cartesian where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Limits.BinProduct
+open import Cubical.Categories.Limits.Terminal as Terminal using (Terminal)
+open import Cubical.Categories.Monoidal.Base
+open import Cubical.Categories.NaturalTransformation
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ (C : Category ℓ ℓ') (binProd : BinProducts C) (term : Terminal C) where
+  open Functor
+  open Category C
+
+  open BinProducts C binProd
+    using ()
+    renaming ( binProdOb to _×_
+             ; binProdPr₁ to pr₁
+             ; binProdPr₂ to pr₂
+             ; binProdArrow to ⟨_,_⟩
+             ; binProdMap to _×ₕ_
+             ; binProdArrowUnique to ⟨,⟩unique
+             ; binProdArrowPr₁ to ⟨,⟩pr₁
+             ; binProdArrowPr₂ to ⟨,⟩pr₂
+             ; binProdArrowCompLeft to ⟨,⟩compLeft
+             ; binProdArrowCompRight to ⟨,⟩compRight)
+
+  cartesianTensorStr : TensorStr C
+  TensorStr.─⊗─ cartesianTensorStr .F-ob (x , y) = x × y
+  TensorStr.─⊗─ cartesianTensorStr .F-hom (f , g) = f ×ₕ g
+  TensorStr.─⊗─ cartesianTensorStr .F-id = ⟨,⟩unique (⋆IdL _ ∙ sym (⋆IdR _)) (⋆IdL _ ∙ sym (⋆IdR _))
+  TensorStr.─⊗─ cartesianTensorStr .F-seq (f , f') (g , g') = ⟨,⟩unique lem1 lem2
+    where
+      lem1 : ((f ×ₕ f') ⋆ (g ×ₕ g')) ⋆ pr₁ ≡ pr₁ ⋆ f ⋆ g
+      lem1 = ⋆Assoc _ _ _
+           ∙ ⟨ refl ⟩⋆⟨ ⟨,⟩pr₁ ⟩
+           ∙ sym (⋆Assoc _ _ _)
+           ∙ ⟨ ⟨,⟩pr₁ ⟩⋆⟨ refl ⟩
+           ∙ ⋆Assoc _ _ _
+
+      lem2 : ((f ×ₕ f') ⋆ (g ×ₕ g')) ⋆ pr₂ ≡ pr₂ ⋆ f' ⋆ g'
+      lem2 = ⋆Assoc _ _ _
+           ∙ ⟨ refl ⟩⋆⟨ ⟨,⟩pr₂ ⟩
+           ∙ sym (⋆Assoc _ _ _)
+           ∙ ⟨ ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+           ∙ ⋆Assoc _ _ _
+
+  TensorStr.unit cartesianTensorStr = fst term
+
+  open TensorStr cartesianTensorStr
+
+  private
+    terminalArrow : ∀ {x} -> Hom[ x , unit ]
+    terminalArrow {x} = Terminal.terminalArrow C term x
+
+    terminalArrowUnique : ∀ {x} {f g : Hom[ x , unit ]} -> f ≡ g
+    terminalArrowUnique {f = f} {g = g} = sym (Terminal.terminalArrowUnique C {term} f) ∙ Terminal.terminalArrowUnique C {term} g
+
+    1×─ : Functor C C
+    1×─ = ─⊗─ ∘F rinj _ _ unit
+
+    ─×1 : Functor C C
+    ─×1 = ─⊗─ ∘F linj _ _ unit
+
+    prodAssocRight : Functor (C ×C C ×C C) C
+    prodAssocRight = ─⊗─ ∘F (Id ×F ─⊗─)
+
+    prodAssocLeft : Functor (C ×C C ×C C) C
+    prodAssocLeft = ─⊗─ ∘F (─⊗─ ×F Id) ∘F (×C-assoc C C C)
+
+    open NatIso
+    open NatTrans
+    open isIso
+
+    leftUnitor : NatIso 1×─ Id
+    leftUnitor .trans .N-ob _ = pr₂
+    leftUnitor .trans .N-hom _ = ⟨,⟩pr₂
+    leftUnitor .nIso x .inv = ⟨ terminalArrow , id ⟩
+    leftUnitor .nIso x .sec = ⟨,⟩pr₂
+    leftUnitor .nIso x .ret = ⟨,⟩compLeft ∙ ⟨,⟩unique terminalArrowUnique ((⋆IdL _) ∙ sym (⋆IdR _))
+
+    rightUnitor : NatIso ─×1 Id
+    rightUnitor .trans .N-ob _ = pr₁
+    rightUnitor .trans .N-hom _ = ⟨,⟩pr₁
+    rightUnitor .nIso x .inv = ⟨ id , terminalArrow ⟩
+    rightUnitor .nIso x .sec = ⟨,⟩pr₁
+    rightUnitor .nIso x .ret = ⟨,⟩compLeft ∙ ⟨,⟩unique (⋆IdL _ ∙ sym (⋆IdR _)) terminalArrowUnique
+
+    associator : NatIso prodAssocRight prodAssocLeft
+
+    associator .trans .N-ob _ = ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩
+
+    associator .trans .N-hom (f , g , h) = ⟨,⟩compLeft
+                                         ∙ cong₂ ⟨_,_⟩ prodAssocRight-pr₁2 prodAssocRight-pr3
+                                         ∙ sym ⟨,⟩compRight
+      where
+        prodAssocRight-pr₁ : prodAssocRight .F-hom (f , g , h) ⋆ pr₁ ≡ pr₁ ⋆ f
+        prodAssocRight-pr₁ = ⟨,⟩pr₁
+
+        prodAssocRight-pr₂ : prodAssocRight .F-hom (f , g , h) ⋆ pr₂ ⋆ pr₁ ≡ (pr₂ ⋆ pr₁) ⋆ g
+        prodAssocRight-pr₂ = sym (⋆Assoc _ _ _)
+                           ∙ ⟨ ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+                           ∙ ⋆Assoc _ _ _
+                           ∙ ⟨ refl ⟩⋆⟨ ⟨,⟩pr₁ ⟩
+                           ∙ sym (⋆Assoc _ _ _)
+
+        prodAssocRight-pr₁2 : prodAssocRight .F-hom (f , g , h) ⋆ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ ≡ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ ⋆ (f ×ₕ g)
+        prodAssocRight-pr₁2 = ⟨,⟩compLeft
+                            ∙ cong₂ ⟨_,_⟩ prodAssocRight-pr₁ prodAssocRight-pr₂
+                            ∙ sym ⟨,⟩compRight
+
+        prodAssocRight-pr3 : prodAssocRight .F-hom (f , g , h) ⋆ pr₂ ⋆ pr₂ ≡ (pr₂ ⋆ pr₂) ⋆ h
+        prodAssocRight-pr3 = sym (⋆Assoc _ _ _)
+                           ∙ cong (_⋆ pr₂) ⟨,⟩pr₂
+                           ∙ ⋆Assoc _ _ _
+                           ∙ cong (pr₂ ⋆_) ⟨,⟩pr₂
+                           ∙ sym (⋆Assoc _ _ _)
+
+    associator .nIso x .inv = ⟨ pr₁ ⋆ pr₁ , ⟨ pr₁ ⋆ pr₂ , pr₂ ⟩ ⟩
+    associator .nIso x .sec = ⟨,⟩compLeft
+                            ∙ cong₂ ⟨_,_⟩
+                                ( ⟨,⟩compLeft
+                                ∙ cong₂ ⟨_,_⟩
+                                    ⟨,⟩pr₁
+                                    (sym (⋆Assoc _ _ _) ∙ ⟨ ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩ ∙ ⟨,⟩pr₁ ) )
+
+                                ( sym (⋆Assoc _ _ _)
+                                ∙ ⟨ ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+                                ∙ ⟨,⟩pr₂ )
+
+                            ∙ ⟨,⟩unique (sym (⟨,⟩unique ⟨ ⋆IdL _ ⟩⋆⟨ refl ⟩ ⟨ ⋆IdL _ ⟩⋆⟨ refl ⟩)) (⋆IdL _)
+
+    associator .nIso x .ret = ⟨,⟩compLeft
+                            ∙ ⟨,⟩unique
+                                ( ⋆IdL _
+                                ∙ sym ⟨,⟩pr₁
+                                ∙ ⟨ sym ⟨,⟩pr₁ ⟩⋆⟨ refl ⟩
+                                ∙ ⋆Assoc _ _ _ )
+
+                                ( ⋆IdL _
+                                ∙ sym (⟨,⟩unique refl refl)
+                                ∙ cong₂ ⟨_,_⟩
+                                    ( sym ⟨,⟩pr₂
+                                    ∙ ⟨ sym ⟨,⟩pr₁ ⟩⋆⟨ refl ⟩
+                                    ∙ ⋆Assoc _ _ _ )
+                                    ( sym ⟨,⟩pr₂ )
+                                ∙ sym ⟨,⟩compLeft )
+
+
+  cartesianMonoidalStr : MonoidalStr C
+  MonoidalStr.tenstr cartesianMonoidalStr = cartesianTensorStr
+  MonoidalStr.α cartesianMonoidalStr = associator
+  MonoidalStr.η cartesianMonoidalStr = leftUnitor
+  MonoidalStr.ρ cartesianMonoidalStr = rightUnitor
+  MonoidalStr.pentagon cartesianMonoidalStr x y z w = ⟨ refl ⟩⋆⟨ ⟨,⟩compRight ⟩
+                                           ∙ ⟨,⟩compLeft
+                                           ∙ ⟨,⟩unique lem1 lem2
+                                           ∙ sym ⟨,⟩compLeft
+    where
+      lem1 : ⟨ ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ ,  pr₂ ⋆ pr₂ ⟩ ⋆ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩
+             , ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩ ⋆ pr₂ ⋆ pr₂
+             ⟩ ⋆ pr₁
+           ≡ (id ×ₕ ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩) ⋆ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ ⋆ ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩
+      lem1 = ⟨,⟩pr₁
+           ∙ ⟨,⟩compLeft
+
+           ∙ (cong₂ ⟨_,_⟩
+                ( ⟨,⟩pr₁
+                ∙ cong₂ ⟨_,_⟩
+                    (sym ⟨,⟩pr₁)
+                    ( sym ⟨,⟩pr₁
+                    ∙ ⟨ sym ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+                    ∙ ⋆Assoc _ _ _ )
+                ∙ sym ⟨,⟩compLeft )
+
+                ( sym (⋆Assoc _ _ _)
+                ∙ ⟨ ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+                ∙ ⋆Assoc _ _ _
+                ∙ sym ⟨,⟩pr₂
+                ∙ ⟨ sym ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+                ∙ ⋆Assoc _ _ _ ))
+
+           ∙ sym ⟨,⟩compLeft
+           ∙ ⟨ cong₂ ⟨_,_⟩
+                 (sym (⋆IdR _) ∙ sym ⟨,⟩pr₁)
+                 ( sym ⟨,⟩pr₁
+                 ∙ ⟨ cong₂ ⟨_,_⟩ (sym ⟨,⟩compLeft) refl
+                   ∙ sym ⟨,⟩compLeft
+                   ∙ sym ⟨,⟩pr₂
+                   ⟩⋆⟨ refl ⟩
+                 ∙ ⋆Assoc _ _ _ )
+             ∙ sym ⟨,⟩compLeft
+             ⟩⋆⟨ refl ⟩
+           ∙ ⋆Assoc _ _ _
+
+      lem2 : ⟨ ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩ ⋆ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩
+             , ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩ ⋆ pr₂ ⋆ pr₂
+             ⟩ ⋆ pr₂
+          ≡ (id ×ₕ ⟨ ⟨ pr₁ , pr₂ ⋆ pr₁ ⟩ , pr₂ ⋆ pr₂ ⟩) ⋆ (pr₂ ⋆ pr₂) ⋆ id
+      lem2 = ⟨,⟩pr₂
+           ∙ sym (⋆Assoc _ _ _)
+           ∙ ⟨ ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+           ∙ ⋆Assoc _ _ _
+           ∙ ⟨ refl ⟩⋆⟨ sym ⟨,⟩pr₂ ⟩
+           ∙ sym (⋆Assoc _ _ _)
+           ∙ ⟨ sym ⟨,⟩pr₂ ⟩⋆⟨ refl ⟩
+           ∙ ⋆Assoc _ _ _
+           ∙ sym (⋆IdR _)
+           ∙ ⋆Assoc _ _ _
+
+  MonoidalStr.triangle cartesianMonoidalStr x y
+    = ⟨,⟩compRight
+    ∙ ⟨,⟩unique
+        (⟨,⟩pr₁ ∙ ⋆IdR _ ∙ sym ⟨,⟩pr₁)
+        (⟨,⟩pr₂ ∙ sym (⋆IdR _))