5 files changed, 438 insertions, 16 deletions
diff --git a/Category/Cocomplete/Bundle.agda b/Category/Cocomplete/Bundle.agda
deleted file mode 100644
index 3ab3cac..0000000
--- a/Category/Cocomplete/Bundle.agda
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-module Category.Cocomplete.Bundle where
-
-open import Level
-
-open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
-open import Categories.Category.Core using (Category)
-
-
-record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
-  field
-    U     : Category o ℓ e
-    finCo : FinitelyCocomplete U
-
-  open Category U public
-  open FinitelyCocomplete finCo public
diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda
new file mode 100644
index 0000000..af40895
--- /dev/null
+++ b/Category/Cocomplete/Finitely/Bundle.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+module Category.Cocomplete.Finitely.Bundle where
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+
+
+record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  field
+    U     : Category o ℓ e
+    finCo : FinitelyCocomplete U
+
+  open Category U public
+  open FinitelyCocomplete finCo public
+
+  open FinitelyCocompleteSymmetricMonoidal finCo using (+-monoidal; +-symmetric)
+
+  symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
+  symmetricMonoidalCategory = record
+      { U = U
+      ; monoidal = +-monoidal
+      ; symmetric = +-symmetric
+      }
diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
new file mode 100644
index 0000000..26813eb
--- /dev/null
+++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+
+module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where
+
+open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
+open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+
+
+module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete 𝒞) where
+
+  open FinitelyCocomplete finCo using (cocartesian)
+  open CocartesianMonoidal cocartesian using (+-monoidal) public
+  open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) public
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
new file mode 100644
index 0000000..a3f8fb0
--- /dev/null
+++ b/Category/Instance/Cospans.agda
@@ -0,0 +1,363 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Function using (flip)
+open import Level using (_⊔_)
+
+module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
+
+open FinitelyCocompleteCategory 𝒞
+
+open import Categories.Diagram.Duality U using (Pushout⇒coPullback)
+open import Categories.Diagram.Pushout U using (Pushout)
+open import Categories.Diagram.Pushout.Properties U using (glue; swap; pushout-resp-≈)
+open import Categories.Morphism U using (_≅_; module ≅)
+open import Categories.Morphism.Duality U using (op-≅⇒≅)
+open import Categories.Morphism.Reasoning U using
+    ( switch-fromtoˡ
+    ; glueTrianglesˡ
+    ; id-comm
+    ; id-comm-sym
+    ; pullˡ
+    ; pullʳ
+    ; assoc²''
+    ; assoc²'
+    )
+
+import Categories.Diagram.Pullback op as Pb using (up-to-iso)
+
+
+private
+
+  variable
+    A B C D X Y Z : Obj
+    f g h : A ⇒ B
+
+record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
+
+  field
+    {N} : Obj
+    f₁  : A ⇒ N
+    f₂  : B ⇒ N
+
+compose : Cospan A B → Cospan B C → Cospan A C
+compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ }
+  where
+    module C₁ = Cospan c₁
+    module C₂ = Cospan c₂
+    module p = pushout C₁.f₂ C₂.f₁
+
+identity : Cospan A A
+identity = record { f₁ = id ; f₂ = id }
+
+compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
+compose-3 c₁ c₂ c₃ = record { f₁ = P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ ; f₂ = P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ }
+  where
+    module C₁ = Cospan c₁
+    module C₂ = Cospan c₂
+    module C₃ = Cospan c₃
+    module P₁ = pushout C₁.f₂ C₂.f₁
+    module P₂ = pushout C₂.f₂ C₃.f₁
+    module P₃ = pushout P₁.i₂ P₂.i₁
+
+record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where
+
+  module C = Cospan C
+  module C′ = Cospan C′
+
+  field
+    ≅N : C.N ≅ C′.N
+
+  open _≅_ ≅N public
+
+  field
+    from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁
+    from∘f₂≈f₂′ : from ∘ C.f₂ ≈ C′.f₂
+
+same-refl : {C : Cospan A B} → Same C C
+same-refl = record
+    { ≅N = ≅.refl
+    ; from∘f₁≈f₁′ = identityˡ
+    ; from∘f₂≈f₂′ = identityˡ
+    }
+
+same-sym : {C C′ : Cospan A B} → Same C C′ → Same C′ C
+same-sym C≅C′ = record
+    { ≅N = ≅.sym ≅N
+    ; from∘f₁≈f₁′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁′)
+    ; from∘f₂≈f₂′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂′)
+    }
+  where
+    open Same C≅C′
+
+same-trans : {C C′ C″ : Cospan A B} → Same C C′ → Same C′ C″ → Same C C″
+same-trans C≈C′ C′≈C″ = record
+    { ≅N = ≅.trans C≈C′.≅N C′≈C″.≅N
+    ; from∘f₁≈f₁′ = glueTrianglesˡ C′≈C″.from∘f₁≈f₁′ C≈C′.from∘f₁≈f₁′
+    ; from∘f₂≈f₂′ = glueTrianglesˡ C′≈C″.from∘f₂≈f₂′ C≈C′.from∘f₂≈f₂′
+    }
+  where
+    module C≈C′ = Same C≈C′
+    module C′≈C″ = Same C′≈C″
+
+glue-i₁ : (p : Pushout f g) → Pushout h (Pushout.i₁ p) → Pushout (h ∘ f) g
+glue-i₁ p = glue p
+
+glue-i₂ : (p₁ : Pushout f g) → Pushout (Pushout.i₂ p₁) h → Pushout f (h ∘ g)
+glue-i₂ p₁ p₂ = swap (glue (swap p₁) (swap p₂))
+
+up-to-iso : (p p′ : Pushout f g) → Pushout.Q p ≅ Pushout.Q p′
+up-to-iso p p′ = op-≅⇒≅ (Pb.up-to-iso (Pushout⇒coPullback p) (Pushout⇒coPullback p′))
+
+pushout-f-id : Pushout f id
+pushout-f-id {_} {_} {f} = record
+    { i₁ = id
+    ; i₂ = f
+    ; commute = id-comm-sym
+    ; universal = λ {B} {h₁} {h₂} eq → h₁
+    ; unique = λ {E} {h₁} {h₂} {eq} {j} j∘i₁≈h₁ j∘i₂≈h₂ → Equiv.sym identityʳ ○ j∘i₁≈h₁
+    ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → identityʳ
+    ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → eq ○ identityʳ
+    }
+  where
+    open HomReasoning
+
+pushout-id-g : Pushout id g
+pushout-id-g {_} {_} {g} = record
+    { i₁ = g
+    ; i₂ = id
+    ; commute = id-comm
+    ; universal = λ {B} {h₁} {h₂} eq → h₂
+    ; unique = λ {E} {h₁} {h₂} {eq} {j} j∘i₁≈h₁ j∘i₂≈h₂ → Equiv.sym identityʳ ○ j∘i₂≈h₂
+    ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → Equiv.sym eq ○ identityʳ
+    ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → identityʳ
+    }
+  where
+    open HomReasoning
+
+extend-i₁-iso
+    : {f : A ⇒ B}
+      {g : A ⇒ C}
+      (p : Pushout f g)
+      (B≅D : B ≅ D)
+    → Pushout (_≅_.from B≅D ∘ f) g
+extend-i₁-iso {_} {_} {_} {_} {f} {g} p B≅D = record
+    { i₁ = P.i₁ ∘ B≅D.to
+    ; i₂ = P.i₂
+    ; commute = begin
+          (P.i₁ ∘ B≅D.to) ∘ B≅D.from ∘ f  ≈⟨ assoc²'' ⟨
+          P.i₁ ∘ (B≅D.to ∘ B≅D.from) ∘ f  ≈⟨ refl⟩∘⟨ B≅D.isoˡ ⟩∘⟨refl ⟩
+          P.i₁ ∘ id ∘ f                   ≈⟨ refl⟩∘⟨ identityˡ ⟩
+          P.i₁ ∘ f                        ≈⟨ P.commute ⟩
+          P.i₂ ∘ g                        ∎
+    ; universal = λ { eq → P.universal (assoc ○ eq) }
+    ; unique = λ {_} {h₁} {_} {j} ≈₁ ≈₂ →
+          let
+            ≈₁′ = begin
+                j ∘ P.i₁                        ≈⟨ refl⟩∘⟨ identityʳ ⟨
+                j ∘ P.i₁ ∘ id                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ B≅D.isoˡ ⟨
+                j ∘ P.i₁ ∘ B≅D.to ∘ B≅D.from    ≈⟨ assoc²' ⟨
+                (j ∘ P.i₁ ∘ B≅D.to) ∘ B≅D.from  ≈⟨ ≈₁ ⟩∘⟨refl ⟩
+                h₁ ∘ B≅D.from                   ∎
+          in P.unique ≈₁′ ≈₂
+    ; universal∘i₁≈h₁ = λ {E} {h₁} {_} {eq} →
+        begin
+            P.universal (assoc ○ eq) ∘ P.i₁ ∘ B≅D.to    ≈⟨ sym-assoc ⟩
+            (P.universal (assoc ○ eq) ∘ P.i₁) ∘ B≅D.to  ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
+            (h₁ ∘ B≅D.from) ∘ B≅D.to                    ≈⟨ assoc ⟩
+            h₁ ∘ B≅D.from ∘ B≅D.to                      ≈⟨ refl⟩∘⟨ B≅D.isoʳ ⟩
+            h₁ ∘ id                                     ≈⟨ identityʳ ⟩
+            h₁                                          ∎
+    ; universal∘i₂≈h₂ = P.universal∘i₂≈h₂
+    }
+  where
+    module P = Pushout p
+    module B≅D = _≅_ B≅D
+    open HomReasoning
+
+extend-i₂-iso
+    : {f : A ⇒ B}
+      {g : A ⇒ C}
+      (p : Pushout f g)
+      (C≅D : C ≅ D)
+    → Pushout f (_≅_.from C≅D ∘ g)
+extend-i₂-iso {_} {_} {_} {_} {f} {g} p C≅D = swap (extend-i₁-iso (swap p) C≅D)
+
+compose-idˡ : {C : Cospan A B} → Same (compose C identity) C
+compose-idˡ {_} {_} {C} = record
+    { ≅N = ≅P
+    ; from∘f₁≈f₁′ = begin
+          ≅P.from ∘ P.i₁ ∘ C.f₁     ≈⟨ assoc ⟨
+          (≅P.from ∘ P.i₁) ∘ C.f₁   ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
+          id ∘ C.f₁                 ≈⟨ identityˡ ⟩
+          C.f₁                      ∎
+    ; from∘f₂≈f₂′ = begin
+          ≅P.from ∘ P.i₂ ∘ id       ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          ≅P.from ∘ P.i₂            ≈⟨ P.universal∘i₂≈h₂ ⟩
+          C.f₂                      ∎
+    }
+  where
+    open HomReasoning
+    module C = Cospan C
+    P = pushout C.f₂ id
+    module P = Pushout P
+    P′ = pushout-f-id {f = C.f₂}
+    ≅P = up-to-iso P P′
+    module ≅P = _≅_ ≅P
+
+compose-idʳ : {C : Cospan A B} → Same (compose identity C) C
+compose-idʳ {_} {_} {C} = record
+    { ≅N = ≅P
+    ; from∘f₁≈f₁′ = begin
+          ≅P.from ∘ P.i₁ ∘ id       ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          ≅P.from ∘ P.i₁            ≈⟨ P.universal∘i₁≈h₁ ⟩
+          C.f₁                      ∎
+    ; from∘f₂≈f₂′ = begin
+          ≅P.from ∘ P.i₂ ∘ C.f₂     ≈⟨ assoc ⟨
+          (≅P.from ∘ P.i₂) ∘ C.f₂   ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩
+          id ∘ C.f₂                 ≈⟨ identityˡ ⟩
+          C.f₂                      ∎
+    }
+  where
+    open HomReasoning
+    module C = Cospan C
+    P = pushout id C.f₁
+    module P = Pushout P
+    P′ = pushout-id-g {g = C.f₁}
+    ≅P = up-to-iso P P′
+    module ≅P = _≅_ ≅P
+
+compose-id² : Same {A} (compose identity identity) identity
+compose-id² = compose-idˡ
+
+compose-3-right
+    : {c₁ : Cospan A B}
+      {c₂ : Cospan B C}
+      {c₃ : Cospan C D}
+    → Same (compose c₁ (compose c₂ c₃)) (compose-3 c₁ c₂ c₃)
+compose-3-right {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
+    { ≅N = up-to-iso P₄′ P₄
+    ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc
+    ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl
+    }
+  where
+    open HomReasoning
+    module C₁ = Cospan c₁
+    module C₂ = Cospan c₂
+    module C₃ = Cospan c₃
+    P₁ = pushout C₁.f₂ C₂.f₁
+    P₂ = pushout C₂.f₂ C₃.f₁
+    module P₁ = Pushout P₁
+    module P₂ = Pushout P₂
+    P₃ = pushout P₁.i₂ P₂.i₁
+    module P₃ = Pushout P₃
+    P₄ = glue-i₂ P₁ P₃
+    module P₄ = Pushout P₄
+    P₄′ = pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
+    module P₄′ = Pushout P₄′
+
+compose-3-left
+    : {c₁ : Cospan A B}
+      {c₂ : Cospan B C}
+      {c₃ : Cospan C D}
+    → Same (compose (compose c₁ c₂) c₃) (compose-3 c₁ c₂ c₃)
+compose-3-left {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
+    { ≅N = up-to-iso P₄′ P₄
+    ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl
+    ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc
+    }
+  where
+    open HomReasoning
+    module C₁ = Cospan c₁
+    module C₂ = Cospan c₂
+    module C₃ = Cospan c₃
+    P₁ = pushout C₁.f₂ C₂.f₁
+    P₂ = pushout C₂.f₂ C₃.f₁
+    module P₁ = Pushout P₁
+    module P₂ = Pushout P₂
+    P₃ = pushout P₁.i₂ P₂.i₁
+    module P₃ = Pushout P₃
+    P₄ = glue-i₁ P₂ P₃
+    module P₄ = Pushout P₄
+    P₄′ = pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
+    module P₄′ = Pushout P₄′
+
+compose-assoc
+    : {c₁ : Cospan A B}
+      {c₂ : Cospan B C}
+      {c₃ : Cospan C D}
+    → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃)
+compose-assoc = same-trans compose-3-right (same-sym compose-3-left)
+
+compose-sym-assoc
+    : {c₁ : Cospan A B}
+      {c₂ : Cospan B C}
+      {c₃ : Cospan C D}
+    → Same (compose (compose c₁ c₂) c₃) (compose c₁ (compose c₂ c₃))
+compose-sym-assoc = same-trans compose-3-left (same-sym compose-3-right)
+
+compose-equiv
+    : {c₂ c₂′ : Cospan B C}
+      {c₁ c₁′ : Cospan A B}
+    → Same c₂ c₂′
+    → Same c₁ c₁′
+    → Same (compose c₁ c₂) (compose c₁′ c₂′)
+compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≈C₂ ≈C₁ = record
+    { ≅N = up-to-iso P P″
+    ; from∘f₁≈f₁′ = begin
+          ≅P.from ∘ P.i₁ ∘ C₁.f₁      ≈⟨ assoc ⟨
+          (≅P.from ∘ P.i₁) ∘ C₁.f₁    ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
+          (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁  ≈⟨ assoc ⟩
+          P′.i₁ ∘ ≈C₁.from ∘ C₁.f₁    ≈⟨ refl⟩∘⟨ ≈C₁.from∘f₁≈f₁′ ⟩
+          P′.i₁ ∘ C₁′.f₁              ∎
+    ; from∘f₂≈f₂′ = begin
+          ≅P.from ∘ P.i₂ ∘ C₂.f₂      ≈⟨ assoc ⟨
+          (≅P.from ∘ P.i₂) ∘ C₂.f₂    ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩
+          (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂  ≈⟨ assoc ⟩
+          P′.i₂ ∘ ≈C₂.from ∘ C₂.f₂    ≈⟨ refl⟩∘⟨ ≈C₂.from∘f₂≈f₂′ ⟩
+          P′.i₂ ∘ C₂′.f₂              ∎
+    }
+  where
+    module C₁ = Cospan c₁
+    module C₁′ = Cospan c₁′
+    module C₂ = Cospan c₂
+    module C₂′ = Cospan c₂′
+    P = pushout C₁.f₂ C₂.f₁
+    P′ = pushout C₁′.f₂ C₂′.f₁
+    module ≈C₁ = Same ≈C₁
+    module ≈C₂ = Same ≈C₂
+    P′′ : Pushout (≈C₁.to ∘ C₁′.f₂) (≈C₂.to ∘ C₂′.f₁)
+    P′′ = extend-i₂-iso (extend-i₁-iso P′ (≅.sym ≈C₁.≅N)) (≅.sym ≈C₂.≅N)
+    P″ : Pushout C₁.f₂ C₂.f₁
+    P″ =
+        pushout-resp-≈
+            P′′
+            (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂′))
+            (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁′))
+    module P = Pushout P
+    module P′ = Pushout P′
+    ≅P : P.Q ≅ P′.Q
+    ≅P = up-to-iso P P″
+    module ≅P = _≅_ ≅P
+    open HomReasoning
+
+Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e)
+Cospans = record
+    { Obj = Obj
+    ; _⇒_ = Cospan
+    ; _≈_ = Same
+    ; id = identity
+    ; _∘_ = flip compose
+    ; assoc = compose-assoc
+    ; sym-assoc = compose-sym-assoc
+    ; identityˡ = compose-idˡ
+    ; identityʳ = compose-idʳ
+    ; identity² = compose-id²
+    ; equiv = record
+        { refl = same-refl
+        ; sym = same-sym
+        ; trans = same-trans
+        }
+    ; ∘-resp-≈ = compose-equiv
+    }
diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
new file mode 100644
index 0000000..fa4d903
--- /dev/null
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Setoids.SymmetricMonoidal {ℓ} where
+
+open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Monoidal.Instance.Setoids
+    using (Setoids-Cartesian; Setoids-Cocartesian)
+    renaming (Setoids-Monoidal to ×-monoidal)
+open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids ℓ ℓ) Setoids-Cartesian
+    using ()
+    renaming (symmetric to ×-symmetric)
+open import Level using (suc)
+open import Categories.Category.Cocartesian (Setoids ℓ ℓ)
+    using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal)
+open CocartesianMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-monoidal)
+open CocartesianSymmetricMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-symmetric)
+
+
+Setoids-× : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ
+Setoids-× = record
+    { U = Setoids ℓ ℓ
+    ; monoidal = ×-monoidal
+    ; symmetric = ×-symmetric
+    }
+
+Setoids-+ : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ
+Setoids-+ = record
+    { U = Setoids ℓ ℓ
+    ; monoidal = +-monoidal
+    ; symmetric = +-symmetric
+    }