Coherence theorem for monoidal categories (#112)

* displayed monoidal categories
* free monoidal category on a type of objects with its universal property
* strong and lax monoidal functors
* Displayed Arrow category and Iso category and their reflection principles
* helper for making displayed monoidal cats with prop homs
* a more convenient version of isSetHom\^D
* product of monoidal cats, prove Graph is a 2-sided fib (also define 2-sided fib)
* Monoidal structure on displayed cat of Isos of Monoidal Cat
* arrow cat is 2-sided fib, iso cat is 2-sided isofib
* reindexing displayed monoidal cat along strong monoidal functor
* prove displayed Iso cat is isofibration, product of strong monoidal functors
* IsoFiber displayed category, whose GlobalSections are sections up to Iso
* Lists as monoidal category, weak universal property
* displayed monoidal total category
* prove hasPropHoms is closed under IsoRetraction
* dual of a monoidal category

Cubical/Categories/Constructions/BinProduct/Monoidal.agda

@@ -0,0 +1,173 @@
+-- Product of two categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.BinProduct.Monoidal where
+
+import Cubical.Categories.Constructions.BinProduct as BP
+
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functors.Constant
+open import Cubical.Categories.Monoidal
+open import Cubical.Categories.Monoidal.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Instances.Functors.More
+
+private
+  variable
+    ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+
+open NatTrans
+open NatIso
+open isIso
+module _ (M : MonoidalCategory ℓC ℓC') (N : MonoidalCategory ℓD ℓD') where
+  private
+    module M = MonoidalCategory M
+    module N = MonoidalCategory N
+  _×M_ : MonoidalCategory (ℓ-max ℓC ℓD) (ℓ-max ℓC' ℓD')
+  _×M_ .MonoidalCategory.C = M.C BP.×C N.C
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.tenstr .TensorStr.─⊗─ =
+    (M.─⊗─ ∘F (BP.Fst M.C N.C BP.×F BP.Fst M.C N.C))
+    BP.,F (N.─⊗─ ∘F (BP.Snd M.C N.C BP.×F BP.Snd M.C N.C))
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.tenstr .TensorStr.unit =
+    M.unit , N.unit
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.α .trans .N-ob x =
+    M.α .trans ⟦ _ ⟧ , N.α .trans ⟦ _ ⟧
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.α .trans .N-hom f =
+    ΣPathP ((M.α .trans .N-hom _) , (N.α .trans .N-hom _))
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.α .nIso x .inv =
+    M.α⁻¹⟨ _ , _ , _ ⟩ , N.α⁻¹⟨ _ , _ , _ ⟩
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.α .nIso x .sec =
+    ΣPathP ((M.α .nIso _ .sec) , (N.α .nIso _ .sec))
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.α .nIso x .ret =
+    ΣPathP ((M.α .nIso _ .ret) , (N.α .nIso _ .ret))
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.η .trans .N-ob x =
+    M.η⟨ _ ⟩ , N.η⟨ _ ⟩
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.η .trans .N-hom x =
+    ΣPathP (M.η .trans .N-hom _ , N.η .trans .N-hom _)
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.η .nIso x .inv =
+    M.η⁻¹⟨ _ ⟩ , N.η⁻¹⟨ _ ⟩
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.η .nIso x .sec =
+    ΣPathP (M.η .nIso _ .sec , N.η .nIso _ .sec)
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.η .nIso x .ret =
+    ΣPathP (M.η .nIso _ .ret , N.η .nIso _ .ret)
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.ρ .trans .N-ob x =
+    M.ρ⟨ _ ⟩ , N.ρ⟨ _ ⟩
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.ρ .trans .N-hom x =
+    ΣPathP (M.ρ .trans .N-hom _ , N.ρ .trans .N-hom _)
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.ρ .nIso x .inv =
+    M.ρ⁻¹⟨ _ ⟩ , N.ρ⁻¹⟨ _ ⟩
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.ρ .nIso x .sec =
+    ΣPathP (M.ρ .nIso _ .sec , N.ρ .nIso _ .sec)
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.ρ .nIso x .ret =
+    ΣPathP (M.ρ .nIso _ .ret , N.ρ .nIso _ .ret)
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.pentagon _ _ _ _ =
+    ΣPathP ((M.pentagon _ _ _ _ ) , (N.pentagon _ _ _ _))
+  _×M_ .MonoidalCategory.monstr .MonoidalStr.triangle _ _ =
+    ΣPathP (M.triangle _ _ , N.triangle _ _)
+
+  open Functor
+  open StrongMonoidalFunctor
+  open StrongMonoidalStr
+  open LaxMonoidalStr
+  -- Probably should be able to do this with a transport but I'll just
+  -- do it manually
+  Fst : StrongMonoidalFunctor _×M_ M
+  Fst .F .F-ob = fst
+  Fst .F .F-hom = fst
+  Fst .F .F-id = refl
+  Fst .F .F-seq _ _ = refl
+  Fst .strmonstr .laxmonstr .ε = M.id
+  Fst .strmonstr .laxmonstr .μ .N-ob = λ _ → M.id
+  Fst .strmonstr .laxmonstr .μ .N-hom = λ _ → M.⋆IdR _ ∙ sym (M.⋆IdL _)
+  Fst .strmonstr .laxmonstr .αμ-law _ _ _ =
+    M.⋆IdR _ ∙ cong₂ M._⋆_ refl (M.─⊗─ .F-id) ∙ M.⋆IdR _
+    ∙ sym (M.⋆IdL _)
+    ∙ cong₂ M._⋆_ (sym (M.⋆IdR _ ∙ M.─⊗─ .F-id)) refl
+  Fst .strmonstr .laxmonstr .ηε-law _ =
+    cong₂ M._⋆_ (M.⋆IdR _ ∙ M.─⊗─ .F-id) refl ∙ M.⋆IdL _
+  Fst .strmonstr .laxmonstr .ρε-law _ =
+    cong₂ M._⋆_ ((M.⋆IdR _ ∙ M.─⊗─ .F-id)) refl ∙ M.⋆IdL _
+  Fst .strmonstr .ε-isIso = idCatIso .snd
+  Fst .strmonstr .μ-isIso = λ _ → idCatIso .snd
+
+  Snd : StrongMonoidalFunctor _×M_ N
+  Snd .F .F-ob = snd
+  Snd .F .F-hom = snd
+  Snd .F .F-id = refl
+  Snd .F .F-seq _ _ = refl
+  Snd .strmonstr .laxmonstr .ε = N.id
+  Snd .strmonstr .laxmonstr .μ .N-ob = λ _ → N.id
+  Snd .strmonstr .laxmonstr .μ .N-hom = λ _ → N.⋆IdR _ ∙ sym (N.⋆IdL _)
+  Snd .strmonstr .laxmonstr .αμ-law _ _ _ =
+    N.⋆IdR _ ∙ cong₂ N._⋆_ refl (N.─⊗─ .F-id) ∙ N.⋆IdR _
+    ∙ sym (N.⋆IdL _)
+    ∙ cong₂ N._⋆_ (sym (N.⋆IdR _ ∙ N.─⊗─ .F-id)) refl
+  Snd .strmonstr .laxmonstr .ηε-law _ =
+    cong₂ N._⋆_ (N.⋆IdR _ ∙ N.─⊗─ .F-id) refl ∙ N.⋆IdL _
+  Snd .strmonstr .laxmonstr .ρε-law _ =
+    cong₂ N._⋆_ ((N.⋆IdR _ ∙ N.─⊗─ .F-id)) refl ∙ N.⋆IdL _
+  Snd .strmonstr .ε-isIso = idCatIso .snd
+  Snd .strmonstr .μ-isIso = λ _ → idCatIso .snd
+
+module _ {M : MonoidalCategory ℓC ℓC'} {N : MonoidalCategory ℓD ℓD'}
+         {O : MonoidalCategory ℓE ℓE'}
+         (G : StrongMonoidalFunctor M N)(H : StrongMonoidalFunctor M O)
+  where
+  private
+    module G = StrongMonoidalFunctor G
+    module H = StrongMonoidalFunctor H
+  open StrongMonoidalFunctor
+  open StrongMonoidalStr
+  open LaxMonoidalStr
+  _,F_ : StrongMonoidalFunctor M (N ×M O)
+  _,F_ .F = G.F BP.,F H.F
+  _,F_ .strmonstr .laxmonstr .ε = G.ε , H.ε
+  _,F_ .strmonstr .laxmonstr .μ .N-ob x = (N-ob G.μ x) , (N-ob H.μ x)
+  _,F_ .strmonstr .laxmonstr .μ .N-hom f =
+    ΣPathP ((N-hom G.μ f) , (N-hom H.μ f))
+  _,F_ .strmonstr .laxmonstr .αμ-law x y z =
+    ΣPathP ((G.αμ-law x y z) , (H.αμ-law x y z))
+  _,F_ .strmonstr .laxmonstr .ηε-law x = ΣPathP (G.ηε-law x , H.ηε-law x)
+  _,F_ .strmonstr .laxmonstr .ρε-law x = ΣPathP (G.ρε-law x , H.ρε-law x)
+  _,F_ .strmonstr .ε-isIso .inv = (G.ε-isIso .inv) , (H.ε-isIso .inv)
+  _,F_ .strmonstr .ε-isIso .sec = ΣPathP ((G.ε-isIso .sec) , (H.ε-isIso .sec))
+  _,F_ .strmonstr .ε-isIso .ret = ΣPathP ((G.ε-isIso .ret) , (H.ε-isIso .ret))
+  _,F_ .strmonstr .μ-isIso x .inv = (G.μ-isIso x .inv) , (H.μ-isIso x .inv)
+  _,F_ .strmonstr .μ-isIso x .sec =
+    ΣPathP ((G.μ-isIso x .sec) , (H.μ-isIso x .sec))
+  _,F_ .strmonstr .μ-isIso x .ret =
+    ΣPathP (G.μ-isIso x .ret , H.μ-isIso x .ret)
+
+module _ {M : MonoidalCategory ℓC ℓC'} {N : MonoidalCategory ℓD ℓD'}
+         {O : MonoidalCategory ℓE ℓE'}{P : MonoidalCategory ℓB ℓB'}
+         (G : StrongMonoidalFunctor M N)(H : StrongMonoidalFunctor O P)
+  where
+  open StrongMonoidalFunctor
+  open LaxMonoidalStr
+  open StrongMonoidalStr
+  private
+    module G = StrongMonoidalFunctor G
+    module H = StrongMonoidalFunctor H
+
+  -- would be definable using composition of strongmonoidal functors,
+  -- but that's not done yet
+  _×F_ : StrongMonoidalFunctor (M ×M O) (N ×M P)
+  _×F_ .F = G .F BP.×F H .F
+  _×F_ .strmonstr .laxmonstr .ε = G.ε , H.ε
+  _×F_ .strmonstr .laxmonstr .μ .N-ob _ = (G.μ ⟦ _ ⟧) , H.μ ⟦ _ ⟧
+  _×F_ .strmonstr .laxmonstr .μ .N-hom _ =
+    ΣPathP ((G.μ .N-hom _) , (H.μ .N-hom _))
+  _×F_ .strmonstr .laxmonstr .αμ-law _ _ _ =
+    ΣPathP (G.αμ-law _ _ _ , H.αμ-law _ _ _ )
+  _×F_ .strmonstr .laxmonstr .ηε-law _ = ΣPathP (G.ηε-law _ , H.ηε-law _ )
+  _×F_ .strmonstr .laxmonstr .ρε-law _ = ΣPathP (G.ρε-law _ , H.ρε-law _ )
+  _×F_ .strmonstr .ε-isIso .inv = G.ε-isIso .inv , H.ε-isIso .inv
+  _×F_ .strmonstr .ε-isIso .sec = ΣPathP (G.ε-isIso .sec , H.ε-isIso .sec)
+  _×F_ .strmonstr .ε-isIso .ret = ΣPathP (G.ε-isIso .ret , H.ε-isIso .ret)
+  _×F_ .strmonstr .μ-isIso _ .inv = G.μ-isIso _ .inv , H.μ-isIso _ .inv
+  _×F_ .strmonstr .μ-isIso _ .sec = ΣPathP (G.μ-isIso _ .sec , H.μ-isIso _ .sec)
+  _×F_ .strmonstr .μ-isIso _ .ret = ΣPathP (G.μ-isIso _ .ret , H.μ-isIso _ .ret)

Cubical/Categories/Constructions/BinProduct/More.agda

@@ -97,3 +97,18 @@ module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{E : Category ℓE 
       ≡⟨ (λ i → (β≡ (c₁ , d₁) (~ i)) ⋆⟨ E ⟩ (G ⟪ fc , fd ⟫)) ⟩
     (((βc c₁) .trans .N-ob d₁) ⋆⟨ E ⟩ (G ⟪ fc , fd ⟫)) ∎
   binaryNatIso F G βc βd β≡ .nIso (c , d)  = (βc c) .nIso d
+
+module _ (C : Category ℓC ℓC')
+         (D : Category ℓD ℓD') where
+  open Functor
+  SplitCatIso× : {x y : C .ob}{z w : D .ob}
+    → CatIso (C ×C D) (x , z) (y , w)
+    → CatIso C x y × CatIso D z w
+  SplitCatIso× f .fst .fst = f .fst .fst
+  SplitCatIso× f .fst .snd .isIso.inv = f .snd .isIso.inv .fst
+  SplitCatIso× f .fst .snd .isIso.sec = cong fst (f .snd .isIso.sec)
+  SplitCatIso× f .fst .snd .isIso.ret = cong fst (f .snd .isIso.ret)
+  SplitCatIso× f .snd .fst = f .fst .snd
+  SplitCatIso× f .snd .snd .isIso.inv = f .snd .isIso.inv .snd
+  SplitCatIso× f .snd .snd .isIso.sec = cong snd (f .snd .isIso.sec)
+  SplitCatIso× f .snd .snd .isIso.ret = cong snd (f .snd .isIso.ret)

Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda

@@ -18,6 +18,7 @@ open import Cubical.Categories.Limits.BinProduct
 open import Cubical.Categories.Limits.BinProduct.More
 
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.More
 open import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Displayed.Limits.Cartesian
 open import Cubical.Categories.Displayed.Limits.Terminal
@@ -112,10 +113,9 @@ module _ (Q : ×Quiver ℓQ ℓQ') where
         elim-F-hom (⋆ₑAssoc f g h i) =
           Cᴰ.⋆Assocᴰ (elim-F-hom f) (elim-F-hom g) (elim-F-hom h) i
         elim-F-hom (isSetExp f g p q i j) =
-          isOfHLevel→isOfHLevelDep 2 (λ _ → Cᴰ.isSetHomᴰ)
+          isSetHomᴰ' Cᴰ
           (elim-F-hom f) (elim-F-hom g)
           (cong elim-F-hom p) (cong elim-F-hom q)
-          (isSetExp f g p q)
           i j
         elim-F-hom !ₑ = !tᴰ _
         -- TODO: Why does this need rectify?

Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda

@@ -12,6 +12,7 @@ open import Cubical.Data.Quiver.Base
 open import Cubical.Data.Sum.Base as Sum hiding (elim; rec)
 open import Cubical.Data.Unit
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.More
 open import Cubical.Categories.Presheaf
 open import Cubical.Categories.Displayed.Presheaf
 open import Cubical.Categories.Displayed.Limits.Terminal
@@ -109,11 +110,9 @@ module _ (Ob : Type ℓg) where
           elim-F-homᴰ (⋆ₑAssoc f g h i) = Cᴰ.⋆Assocᴰ
             (elim-F-homᴰ f) (elim-F-homᴰ g) (elim-F-homᴰ h) i
           elim-F-homᴰ (isSetExp f g p q i j) =
-            isOfHLevel→isOfHLevelDep 2
-            ((λ x → Cᴰ.isSetHomᴰ))
-            ((elim-F-homᴰ f)) ((elim-F-homᴰ g))
-            ((cong elim-F-homᴰ p)) ((cong elim-F-homᴰ q))
-            ((isSetExp f g p q))
+            isSetHomᴰ' Cᴰ
+            (elim-F-homᴰ f) (elim-F-homᴰ g)
+            (cong elim-F-homᴰ p) (cong elim-F-homᴰ q)
             i j
           elim-F-homᴰ {d = d} !ₑ = !tᴰ (ϕ* d)
           elim-F-homᴰ {d = d} (isProp!ₑ f g i) = goal i