Show category of maps is monoidal

2 files changed, 263 insertions, 39 deletions

diff --git a/Category/Dagger/2-Poset.agda b/Category/Dagger/2-Poset.agda
index 27c01af..fcd7e4a 100644
--- a/Category/Dagger/2-Poset.agda
+++ b/Category/Dagger/2-Poset.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category using (Category)
-open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
 open import Level using (Level; suc; _⊔_)
 
 module Category.Dagger.2-Poset {o ℓ e : Level} where
@@ -17,7 +16,7 @@ open import Categories.Enriched.Category Posets-Monoidal using () renaming (Cate
 open import Data.Product using (_,_)
 open import Data.Unit.Polymorphic using (tt)
 open import Relation.Binary using (Poset)
-open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
+open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism)
 
 open PosetHomomorphism using (⟦_⟧; cong; mono)
 
@@ -51,49 +50,13 @@ record Dagger-2-Poset : Set (suc (o ⊔ ℓ ⊔ e)) where
   private
     module P {A B : Obj} = Poset (hom A B)
 
-  open P using (_≤_) public
+  open P using (_≤_; reflexive) public
   open Category category hiding (Obj) public
   open HasDagger hasDagger public
 
   field
     †-resp-≤ : {A B : Obj} {f g : A ⇒ B} → f ≤ g → f † ≤ g †
 
-dagger-2-poset : {𝒞 : Category o ℓ e} (ISA† : IdempotentSemiadditiveDagger 𝒞) → Dagger-2-Poset
-dagger-2-poset {𝒞} ISA† = record
-    { 2-poset = record
-        { Obj = Obj
-        ; hom = λ A B → record
-            { Carrier = A ⇒ B
-            ; _≈_ = _≈_
-            ; _≤_ = ISA†._≤_
-            ; isPartialOrder = record
-                { isPreorder = record
-                    { isEquivalence = equiv
-                    ; reflexive = λ x≈y → Equiv.trans (ISA†.+-congʳ x≈y) ISA†.≤-refl
-                    ; trans = ISA†.≤-trans
-                    }
-                ; antisym = ISA†.≤-antisym
-                }
-            }
-        ; id = mkPosetHomo _ _ (λ _ → id) (λ _ → ISA†.≤-refl)
-        ; ⊚ = mkPosetHomo _ _ (λ (f , g) → f ∘ g) (λ (≤₁ , ≤₂) → ISA†.≤-resp-∘ ≤₁ ≤₂)
-        ; ⊚-assoc = assoc
-        ; unitˡ = identityˡ
-        ; unitʳ = identityʳ
-        }
-    ; hasDagger = record
-        { _† = ISA†._†
-        ; †-identity = ISA†.†-identity
-        ; †-homomorphism = ISA†.†-homomorphism
-        ; †-resp-≈ = ISA†.⟨_⟩†
-        ; †-involutive = ISA†.†-involutive
-        }
-    ; †-resp-≤ = ISA†.†-resp-≤
-    }
-  where
-    module ISA† = IdempotentSemiadditiveDagger ISA†
-    open Category 𝒞
-
 module _ (S : Dagger-2-Poset) where
 
   open Dagger-2-Poset S
@@ -104,6 +67,14 @@ module _ (S : Dagger-2-Poset) where
       functional : f ∘ f † ≤ id
       entire : id ≤ f † ∘ f
 
+  open import Categories.Morphism category using (Iso)
+
+  unitary-isMap : {A B : Obj} {f : A ⇒ B} → Iso f (f †) → IsMap f
+  unitary-isMap iso = let open Iso iso in record
+      { functional = reflexive isoʳ
+      ; entire = reflexive (Equiv.sym isoˡ)
+      }
+
   record Map (A B : Obj) : Set (ℓ ⊔ e) where
 
     field
diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda
index a5b03ab..424f8df 100644
--- a/Category/Dagger/Semiadditive.agda
+++ b/Category/Dagger/Semiadditive.agda
@@ -5,11 +5,21 @@ open import Categories.Category using (Category)
 
 module Category.Dagger.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where
 
+import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Category.Semiadditive.Monoidal as SemiadditiveMonoidal
 
 open import Categories.Category.Dagger using (HasDagger)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.Morphism using (Iso)
+open import Categories.Morphism.Properties 𝒞 using (Iso-resp-≈; Iso-swap)
+open import Category.Dagger.2-Poset using (Dagger-2-Poset; Map; Maps; unitary-isMap)
 open import Category.Semiadditive using (Semiadditive)
+open import Data.Product using (_,_)
 open import Relation.Binary using (Rel)
+open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
 
 record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
 
@@ -41,6 +51,42 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       Δ † † ≈⟨ †-involutive Δ ⟩
       Δ     ∎
 
+  i₁† : {A B : Obj} → i₁ {A} {B} † ≈ π₁
+  i₁† = begin
+      i₁ †    ≈⟨ ⟨ π₁† ⟩† ⟨
+      π₁ † †  ≈⟨ †-involutive π₁ ⟩
+      π₁      ∎
+
+  i₂† : {A B : Obj} → i₂ {A} {B} † ≈ π₂
+  i₂† = begin
+      i₂ †    ≈⟨ ⟨ π₂† ⟩† ⟨
+      π₂ † †  ≈⟨ †-involutive π₂ ⟩
+      π₂      ∎
+
+  module _ {A B C : Obj} where
+
+    α⇒† : assocˡ {A} {B} {C} † ≈ assocʳ
+    α⇒† = begin
+        ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ †          ≈⟨ ⟨⟩-† ⟩
+        [ (π₁ ∘ π₁) † , ⟨ π₂ ∘ π₁ , π₂ ⟩ † ]      ≈⟨ []-cong₂ †-homomorphism ⟨⟩-† ⟩
+        [ π₁ † ∘ π₁ † , [ (π₂ ∘ π₁) † , π₂ † ] ]  ≈⟨ []-congˡ ([]-congʳ †-homomorphism) ⟩
+        [ π₁ † ∘ π₁ † , [ π₁ † ∘ π₂ † , π₂ † ] ]  ≈⟨ []-cong₂ (π₁† ⟩∘⟨ π₁†) ([]-cong₂ (π₁† ⟩∘⟨ π₂†) π₂†) ⟩
+        [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ]            ≈⟨ assocʳ≈+-assocʳ ⟨
+        assocʳ                                    ∎
+
+    α⇐† : assocʳ {A} {B} {C} † ≈ assocˡ
+    α⇐† = begin
+        assocʳ †    ≈⟨ ⟨ α⇒† ⟩† ⟨
+        assocˡ † †  ≈⟨ †-involutive assocˡ ⟩
+        assocˡ      ∎
+
+  swap† : {A B : Obj} → swap {A} {B} † ≈ swap {B} {A}
+  swap† {A} {B} = begin
+      ⟨ π₂ , π₁ ⟩ †   ≈⟨ ⟨⟩-† ⟩
+      [ π₂ † , π₁ † ] ≈⟨ []-cong₂ π₂† π₁† ⟩
+      [ i₂ , i₁ ]     ≈⟨ swap≈+-swap ⟨
+      ⟨ π₂ , π₁ ⟩     ∎
+
   †-resp-×₁ : {A B C D : Obj} {f : A ⇒ B} {g : C ⇒ D} → (f ×₁ g) † ≈ (f †) ×₁ (g †)
   †-resp-×₁ {f = f} {g} = begin
       ⟨ f ∘ π₁ , g ∘ π₂ ⟩ †       ≈⟨ ⟨⟩-† ⟩
@@ -77,6 +123,21 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       id ∘ f ∘ h + id ∘ g ∘ h ≈⟨ +-cong (pullˡ identityˡ) (pullˡ identityˡ) ⟩
       f ∘ h + g ∘ h           ∎
 
+  open SemiadditiveMonoidal semiadditive using (monoidal; symmetric)
+
+  monoidalCategory : MonoidalCategory o ℓ e
+  monoidalCategory = record
+      { U = 𝒞
+      ; monoidal = monoidal
+      }
+
+  symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
+  symmetricMonoidalCategory = record
+      { U = 𝒞
+      ; monoidal = monoidal
+      ; symmetric = symmetric
+      }
+
 record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
 
   field
@@ -127,6 +188,41 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       (f + h) + (g + i) ≈⟨ +-cong f≤h g≤i ⟩
       h + i             ∎
 
+  Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ
+  Δ-⊕ {X} {Y} = begin
+      ⟨ id , id ⟩                                     ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨
+      ⟨ id ×₁ id , id ×₁ id ⟩                         ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ project₁ project₁) (×₁-cong₂ project₂ project₂) ⟨
+      ⟨ (π₁ ∘ Δ) ×₁ (π₁ ∘ Δ) , (π₂ ∘ Δ) ×₁ (π₂ ∘ Δ) ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨
+      ⟨ π₁ ×₁ π₁ ∘ Δ ×₁ Δ , π₂ ×₁ π₂ ∘ Δ ×₁ Δ ⟩       ≈⟨ ⟨⟩∘ ⟨
+      σ₂₃ ∘ Δ ×₁ Δ                                    ∎
+
+  ∇-⊕ : {X Y : Obj} → ∇ {X ⊕ Y} ≈ ∇ ×₁ ∇ ∘ σ₂₃
+  ∇-⊕ {X} {Y} = begin
+      [ id , id ]                                       ≈⟨ []-cong₂ id×₁id id×₁id ⟨
+      [ id ×₁ id , id ×₁ id ]                           ≈⟨ []-cong₂ (×₁-cong₂ inject₁ inject₁) (×₁-cong₂ inject₂ inject₂) ⟨
+      [ (∇ ∘ i₁) ×₁ (∇ ∘ i₁) , (∇ ∘ i₂) ×₁ (∇ ∘ i₂) ]   ≈⟨ []-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨
+      [ ∇ ×₁ ∇ ∘ i₁ ×₁ i₁ , ∇ ×₁ ∇ ∘ i₂ ×₁ i₂ ]         ≈⟨ ∘[] ⟨
+      ∇ ×₁ ∇ ∘ [ i₁ ×₁ i₁ , i₂ ×₁ i₂ ]                  ≈⟨ refl⟩∘⟨ ⟨⟩-unique (∘[] ○ []-cong₂ π₁∘×₁ π₁∘×₁) (∘[] ○ []-cong₂ π₂∘×₁ π₂∘×₁) ⟨
+      ∇ ×₁ ∇ ∘ ⟨ π₁ +₁ π₁ , π₂ +₁ π₂ ⟩                  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (×₁-+₁ π₁ π₁) (×₁-+₁ π₂ π₂) ⟨
+      ∇ ×₁ ∇ ∘ σ₂₃                                      ∎
+
+  ≤-resp-×₁
+      : {A B C D : Obj}
+        {f h : A ⇒ B}
+        {g i : C ⇒ D}
+      → f ≤ h
+      → g ≤ i
+      → (f ×₁ g) ≤ (h ×₁ i)
+  ≤-resp-×₁ {f = f} {h} {g} {i} f≤h g≤i = begin
+      ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ Δ                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-⊕ ⟩
+      ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ∘ Δ ×₁ Δ             ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-×₁ ⟩
+      ∇ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ             ≈⟨ pushˡ ∇-⊕ ⟩
+      ∇ ×₁ ∇ ∘ σ₂₃ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ  ≈⟨ refl⟩∘⟨ cancelˡ σ₂₃-σ₂₃ ⟩
+      ∇ ×₁ ∇ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ              ≈⟨ refl⟩∘⟨ ×₁∘×₁ ⟩
+      ∇ ×₁ ∇ ∘ (f ×₁ h ∘ Δ) ×₁ (g ×₁ i ∘ Δ)               ≈⟨ ×₁∘×₁ ⟩
+      (∇ ∘ f ×₁ h ∘ Δ) ×₁ (∇ ∘ g ×₁ i ∘ Δ)                ≈⟨ ×₁-cong₂ f≤h g≤i ⟩
+      h ×₁ i                                              ∎
+
   ≤-resp-∘
       : {A B C : Obj}
         {f h : B ⇒ C}
@@ -156,3 +252,160 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where
       ∇ ∘ Δ             ≈⟨ refl⟩∘⟨ introˡ id×₁id ⟩
       ∇ ∘ id ×₁ id ∘ Δ  ≈⟨ idempotent ⟩
       id                ∎
+
+  dagger-2-poset : Dagger-2-Poset
+  dagger-2-poset = record
+      { 2-poset = record
+          { Obj = Obj
+          ; hom = λ A B → record
+              { Carrier = A ⇒ B
+              ; _≈_ = _≈_
+              ; _≤_ = _≤_
+              ; isPartialOrder = record
+                  { isPreorder = record
+                      { isEquivalence = equiv
+                      ; reflexive = λ x≈y → Equiv.trans (+-congʳ x≈y) ≤-refl
+                      ; trans = ≤-trans
+                      }
+                  ; antisym = ≤-antisym
+                  }
+              }
+          ; id = mkPosetHomo _ _ (λ _ → id) (λ _ → ≤-refl)
+          ; ⊚ = mkPosetHomo _ _ (λ (f , g) → f ∘ g) (λ (≤₁ , ≤₂) → ≤-resp-∘ ≤₁ ≤₂)
+          ; ⊚-assoc = assoc
+          ; unitˡ = identityˡ
+          ; unitʳ = identityʳ
+          }
+      ; hasDagger = record
+          { _† = _†
+          ; †-identity = †-identity
+          ; †-homomorphism = †-homomorphism
+          ; †-resp-≈ = ⟨_⟩†
+          ; †-involutive = †-involutive
+          }
+      ; †-resp-≤ = †-resp-≤
+      }
+
+  maps : Category o (ℓ ⊔ e) e
+  maps = Maps dagger-2-poset
+
+  open Dagger-2-Poset dagger-2-poset using (category)
+  open SemiadditiveMonoidal semiadditive using (monoidal)
+
+  module M = Monoidal monoidal
+
+  ×₁-functional
+      : {A B C D : Obj}
+        {f : A ⇒ B}
+        {g : C ⇒ D}
+      → (f ∘ f †) ≤ id
+      → (g ∘ g †) ≤ id
+      → (f ×₁ g ∘ (f ×₁ g) †) ≤ id
+  ×₁-functional {f = f} {g} f∘f†≤id g∘g†≤id = begin
+      f ×₁ g ∘ (f ×₁ g) † + id          ≈⟨ +-congʳ (refl⟩∘⟨ †-resp-×₁) ⟩
+      f ×₁ g ∘ (f †) ×₁ (g †) + id      ≈⟨ +-cong ×₁∘×₁ (Equiv.sym id×₁id) ⟩
+      (f ∘ f †) ×₁ (g ∘ g †) + id ×₁ id ≈⟨ ≤-resp-×₁ f∘f†≤id g∘g†≤id ⟩
+      id ×₁ id                          ≈⟨ id×₁id ⟩
+      id                                ∎
+
+  ×₁-entire
+      : {A B C D : Obj}
+        {f : A ⇒ B}
+        {g : C ⇒ D}
+      → id ≤ (f † ∘ f)
+      → id ≤ (g † ∘ g)
+      → id ≤ ((f ×₁ g) † ∘ f ×₁ g)
+  ×₁-entire {f = f} {g} id≤f†∘f id≤g†∘g = begin
+      id + (f ×₁ g) † ∘ (f ×₁ g)        ≈⟨ +-congˡ (†-resp-×₁ ⟩∘⟨refl) ⟩
+      id + (f †) ×₁ (g †) ∘ f ×₁ g      ≈⟨ +-cong (Equiv.sym id×₁id) ×₁∘×₁ ⟩
+      id ×₁ id + (f † ∘ f) ×₁ (g † ∘ g) ≈⟨ ≤-resp-×₁ id≤f†∘f id≤g†∘g ⟩
+      (f † ∘ f) ×₁ (g † ∘ g)            ≈⟨ ×₁∘×₁ ⟨
+      (f †) ×₁ (g †) ∘ f ×₁ g           ≈⟨ †-resp-×₁ ⟩∘⟨refl ⟨
+      (f ×₁ g) † ∘ f ×₁ g               ∎
+
+  open Map
+
+  ⊗ : Bifunctor maps maps maps
+  ⊗ = record
+      { F₀ = M.⊗.₀
+      ; F₁ = λ (f , g) → record
+          { map = map f M.⊗₁ map g
+          ; isMap = record
+              { functional = ×₁-functional (functional f) (functional g)
+              ; entire = ×₁-entire (entire f) (entire g)
+              }
+          }
+      ; identity = M.⊗.identity
+      ; homomorphism = M.⊗.homomorphism
+      ; F-resp-≈ = M.⊗.F-resp-≈
+      }
+
+  open Morphism maps using (_≅_)
+  open Equiv
+
+  λ⇒-unitary : {X : Obj} → Iso category (π₂ {𝟘} {X}) (π₂ †)
+  λ⇒-unitary = record { Iso (Iso-resp-≈ M.unitorˡ.iso refl (sym π₂†)) }
+
+  λ⇐-unitary : {X : Obj} → Iso category (i₂ {𝟘} {X}) (i₂ †)
+  λ⇐-unitary = record { Iso (Iso-swap (Iso-resp-≈ M.unitorˡ.iso (sym i₂†) refl)) }
+
+  ρ⇒-unitary : {X : Obj} → Iso category (π₁ {X} {𝟘}) (π₁ †)
+  ρ⇒-unitary = record { Iso (Iso-resp-≈ M.unitorʳ.iso refl (sym π₁†)) }
+
+  ρ⇐-unitary : {X : Obj} → Iso category (i₁ {X} {𝟘}) (i₁ †)
+  ρ⇐-unitary = record { Iso (Iso-swap (Iso-resp-≈ M.unitorʳ.iso (sym i₁†) refl)) }
+
+  α⇒-unitary : {X Y Z : Obj} → Iso category (assocˡ {X} {Y} {Z}) (assocˡ †)
+  α⇒-unitary = record { Iso (Iso-resp-≈ M.associator.iso refl (sym α⇒†)) }
+
+  α⇐-unitary : {X Y Z : Obj} → Iso category (assocʳ {X} {Y} {Z}) (assocʳ †)
+  α⇐-unitary = record { Iso (Iso-swap (Iso-resp-≈ M.associator.iso (sym α⇐†) refl)) }
+
+  unitorˡ : {X : Obj} → 𝟘 M.⊗₀ X ≅ X
+  unitorˡ = record
+      { from = record
+          { map = M.unitorˡ.from
+          ; isMap = unitary-isMap dagger-2-poset λ⇒-unitary
+          }
+      ; to = record
+          { map = M.unitorˡ.to
+          ; isMap = unitary-isMap dagger-2-poset λ⇐-unitary
+          }
+      ; iso = record { M.unitorˡ }
+      }
+
+  unitorʳ : {X : Obj} → X M.⊗₀ 𝟘 ≅ X
+  unitorʳ = record
+      { from = record
+          { map = M.unitorʳ.from
+          ; isMap = unitary-isMap dagger-2-poset ρ⇒-unitary
+          }
+      ; to = record
+          { map = M.unitorʳ.to
+          ; isMap = unitary-isMap dagger-2-poset ρ⇐-unitary
+          }
+      ; iso = record { M.unitorʳ }
+      }
+
+  associator : {X Y Z : Obj} → (X M.⊗₀ Y) M.⊗₀ Z ≅ X M.⊗₀ (Y M.⊗₀ Z)
+  associator = record
+      { from = record
+          { map = M.associator.from
+          ; isMap = unitary-isMap dagger-2-poset α⇒-unitary
+          }
+      ; to = record
+          { map = M.associator.to
+          ; isMap = unitary-isMap dagger-2-poset α⇐-unitary
+          }
+      ; iso = record { M.associator }
+      }
+
+  maps-monoidal : Monoidal maps
+  maps-monoidal = record
+      { ⊗ = ⊗
+      ; unit = 𝟘
+      ; unitorˡ = unitorˡ
+      ; unitorʳ = unitorʳ
+      ; associator = associator
+      ; M
+      }