Update to latest agda-categories

5 files changed, 63 insertions, 23 deletions

diff --git a/Category/Cartesian/Instance/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda
index 5425233..8c779d5 100644
--- a/Category/Cartesian/Instance/FinitelyCocompletes.agda
+++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda
@@ -16,8 +16,8 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; ni
 open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso)
 open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct)
 open import Categories.Object.Initial using (IsInitial)
-open import Data.Product.Base using (_,_) renaming (_×_ to _×′_)
-
+open import Data.Product using (_,_; swap) renaming (_×_ to _×′_)
+open import Function using () renaming (_∘_ to _∘′_)
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
 open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_)
 open import Functor.Exact using (IsRightExact; RightExactFunctor)
@@ -44,13 +44,48 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where
   private
     module -+- = Functor -+-
 
+  flip-IsInitial
+      : {(A , B) : 𝒞×𝒞.Obj}
+      → IsInitial 𝒞×𝒞.U (A , B)
+      → IsInitial 𝒞×𝒞.U (B , A)
+  flip-IsInitial isInitial = let open IsInitial isInitial in record
+      { ! = swap !
+      ; !-unique = swap ∘′ !-unique ∘′ swap
+      }
+
+  flip-IsCoproduct
+      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
+        {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)}
+        {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
+      → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂)
+      → IsCoproduct 𝒞×𝒞.U (i₁-₂ , i₁-₁) (i₂-₂ , i₂-₁)
+  flip-IsCoproduct isCoproduct = let module + = IsCoproduct isCoproduct in record
+      { [_,_] = λ x y → swap (+.[ swap x , swap y ])
+      ; inject₁ = swap +.inject₁
+      ; inject₂ = swap +.inject₂
+      ; unique = λ x y → swap (+.unique (swap x) (swap y))
+      }
+
+  flip-IsCoequalizer
+      : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj}
+        {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)}
+        {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)}
+      → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂)
+      → IsCoequalizer 𝒞×𝒞.U (f₂ , f₁) (g₂ , g₁) (h₂ , h₁)
+  flip-IsCoequalizer isCoeq = let open IsCoequalizer isCoeq in record
+      { equality = swap equality
+      ; coequalize = swap ∘′ coequalize ∘′ swap
+      ; universal = swap universal
+      ; unique = swap ∘′ unique ∘′ swap
+      }
+
   +-resp-⊥
       : {(A , B) : 𝒞×𝒞.Obj}
       → IsInitial 𝒞×𝒞.U (A , B)
       → IsInitial 𝒞.U (A + B)
   +-resp-⊥ {A , B} A,B-isInitial = record
       { ! = [ A-isInitial.! , B-isInitial.! ]
-      ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) }
+      ; !-unique = λ f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂)))
       }
     where
       open IsRightExact
@@ -209,7 +244,14 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
   module x+y = RightExactFunctor -+-
 
   ↔-+- : 𝒞 × 𝒞 ⇒ 𝒞
-  ↔-+- = -+- ∘ Swap 𝒞 𝒞
+  ↔-+- = record
+      { F = flip-bifunctor 𝒞.-+-
+      ; isRightExact = record
+          { F-resp-⊥ = λ x → +-resp-⊥ 𝒞 (flip-IsInitial 𝒞 x)
+          ; F-resp-+ = λ x → +-resp-+ 𝒞 (flip-IsCoproduct 𝒞 x)
+          ; F-resp-coeq = λ x → (+-resp-coeq 𝒞 (flip-IsCoequalizer 𝒞 x))
+          }
+      }
   module y+x = RightExactFunctor ↔-+-
 
   [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞
@@ -227,7 +269,6 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where
       module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞)
       open Morphism U using (_≅_; module ≅)
       module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z}))
-      open import Categories.Category.BinaryProducts using (BinaryProducts)
       open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct)
       op-binaryProducts : BinaryProducts op
       op-binaryProducts = record { product = Coproduct⇒coProduct coproduct }
diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda
index fa15295..3b49b26 100644
--- a/Category/Instance/Properties/SymMonCat.agda
+++ b/Category/Instance/Properties/SymMonCat.agda
@@ -18,7 +18,6 @@ open import Categories.Category.Instance.One using (One)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
 open import Categories.Category.Cartesian SymMonCat using (Cartesian)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
-open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
 open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts)
 open import Categories.Functor.Monoidal.Construction.Product
   using ()
diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda
index e4b136c..814abeb 100644
--- a/Category/Instance/SymMonCat.agda
+++ b/Category/Instance/SymMonCat.agda
@@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel)
 open import Categories.Category using (Category; _[_,_]; _[_∘_])
 open import Categories.Category.Helper using (categoryHelper)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
+open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
 
 open SMF.Lax using (SymmetricMonoidalFunctor)
 open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda
index 3df57ee..b0625ab 100644
--- a/Category/Monoidal/Instance/DecoratedCospans.agda
+++ b/Category/Monoidal/Instance/DecoratedCospans.agda
@@ -257,21 +257,21 @@ module LiftAssociator where
     open NaturalIsomorphism using (F⇐G)
     ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ assoc-≃))) ∘ᵥ ≃₂ ≋ ≃₁
     ≃₂≋≃₁ {(X , Y) , Z} {(f , g) , h} = begin
-        F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ _) ∘ ρ⇐) ∘ id                                               ≈⟨ refl⟩∘⟨ identityʳ ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym-assoc ⟩∘⟨refl ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ ((F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ ρ⇐) ∘ ρ⇐                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟨
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ λ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-to ⟨
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ λ⇐ ∘ ρ⇐                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (switch-tofromˡ α coherence-inv₁) ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩∘⟨refl ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g) ⊗₁ h ∘ ρ⇐ ⊗₁ id ∘ ρ⇐      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym split₁ʳ) ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
-        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ (id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐          ≈⟨ refl⟩∘⟨ sym-assoc ⟩
-        F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐          ≈⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α′) F.associativity) ⟨
-        F.⊗-homo.η (X + Y , Z) ∘ F.⊗-homo.η (X , Y) ⊗₁ id ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐                           ≈⟨ refl⟩∘⟨ pullˡ (sym split₁ˡ) ⟩
-        F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ (f ⊗₁ g) ∘ ρ⇐) ⊗₁ h ∘ ρ⇐                               ∎
+        F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ _) ∘ ρ⇐) ∘ id                                           ≈⟨ refl⟩∘⟨ identityʳ ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym-assoc ⟩∘⟨refl ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ ((F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ ρ⇐) ∘ ρ⇐                 ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ ρ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟨
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ λ⇐             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-to ⟨
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ λ⇐ ∘ ρ⇐                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (switch-tofromˡ α coherence-inv₁) ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g) ⊗₁ h ∘ ρ⇐ ⊗₁ id ∘ ρ⇐  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym split₁ʳ) ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩
+        F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ (id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐      ≈⟨ refl⟩∘⟨ sym-assoc ⟩
+        F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐      ≈⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α′) F.associativity) ⟨
+        F.⊗-homo.η (X + Y , Z) ∘ F.⊗-homo.η (X , Y) ⊗₁ id ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐                       ≈⟨ refl⟩∘⟨ pullˡ (sym split₁ˡ) ⟩
+        F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ (f ⊗₁ g) ∘ ρ⇐) ⊗₁ h ∘ ρ⇐                           ∎
       where
         open Shorthands 𝒞.monoidal using () renaming (α⇐ to α⇐′)
         open Shorthands 𝒟.monoidal using (α⇒; λ⇐)
diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda
index f8ef542..647f887 100644
--- a/Category/Monoidal/Instance/DecoratedCospans/Products.agda
+++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda
@@ -25,7 +25,7 @@ open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
-open import Categories.Functor.Monoidal.Properties using (∘-SymmetricMonoidal)
+open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-SymmetricMonoidal)
 open import Categories.Functor.Monoidal.Construction.Product using (⁂-SymmetricMonoidalFunctor)
 open import Categories.NaturalTransformation.Core using (NaturalTransformation; _∘ᵥ_; ntHelper)
 open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian)