Mercurial > hg > Members > kono > Proof > category

changeset 72:cbc30519e961

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack overflow solved by moving implicit parameters to module parameters
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jul 2013 12:38:54 +0900
parents 709c1bde54dc
children b75b5792bd81
files adj-monad.agda nat.agda
diffstat 2 files changed, 147 insertions(+), 170 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/adj-monad.agda	Fri Jul 26 12:38:54 2013 +0900
@@ -0,0 +1,95 @@
+-- Monad
+-- Category A
+-- A = Category
+-- Functor T : A → A
+--T(a) = t(a)
+--T(f) = tf(f)
+
+open import Category -- https://github.com/konn/category-agda
+open import Level
+--open import Category.HomReasoning
+open import HomReasoning
+open import cat-utility
+open import Category.Cat
+
+module adj-monad where
+
+----
+--
+-- Adjunction to Monad
+--
+----
+
+open Adjunction
+open NTrans
+open Functor
+
+UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 ( U : Functor B A )
+                 ( F : Functor A B )
+                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) → NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
+UεF A B U F ε =  lemma11  (
+     Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○  U} {identityFunctor} ε F)  ) where
+         lemma11 :   NTrans A A   ( U ○ ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) ) 
+                  →  NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
+         lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
+
+Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 { U : Functor B A }
+                 { F : Functor A B }
+                 { η : NTrans A A identityFunctor ( U ○  F ) }
+                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
+      Adjunction A B U F η ε  → Monad A (U ○  F) η (UεF A B U F ε)
+Adj2Monad A B {U} {F} {η} {ε} adj = record {
+         isMonad = record {
+                    assoc = assoc1;
+                    unity1 = unity1;
+                    unity2 = unity2
+              }
+      }  where
+           T : Functor A A
+           T = U  ○ F
+           μ : NTrans A A ( T ○ T ) T
+           μ = UεF A B U F ε
+           lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → 
+                 B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ] 
+           lemma-assoc1 f =  IsNTrans.naturality ( isNTrans ε )
+           assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
+           assoc1 {a} = let open ≈-Reasoning (A) in
+             begin
+                TMap μ a o TMap μ ( FObj T a )
+             ≈⟨⟩
+                (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F  a )))))
+             ≈⟨ sym (distr U) ⟩
+                FMap U (B [ TMap ε ( FObj F a )  o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
+             ≈⟨  (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
+                FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
+             ≈⟨ distr U ⟩
+                (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
+             ≈⟨⟩
+                TMap μ a o FMap T (TMap μ a) 
+             ∎
+           unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+           unity1 {a} = let open ≈-Reasoning (A) in
+             begin
+               TMap μ a o TMap η ( FObj T a )
+             ≈⟨⟩
+               (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F  a ))
+             ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
+               id (FObj U ( FObj F a ))
+             ≈⟨⟩
+               id (FObj T a)
+             ∎
+           unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+           unity2 {a} = let open ≈-Reasoning (A) in
+             begin
+                TMap μ a o (FMap T (TMap η a ))
+             ≈⟨⟩
+                (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
+             ≈⟨ sym (distr U ) ⟩
+                FMap U ( B [  (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
+             ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
+                FMap U ( id1 B (FObj F a) )
+             ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
+                id (FObj T a)
+             ∎
--- a/nat.agda	Fri Jul 26 11:42:57 2013 +0900
+++ b/nat.agda	Fri Jul 26 12:38:54 2013 +0900
@@ -1,4 +1,4 @@
-module nat  where 
+
 
 -- Monad
 -- Category A
@@ -12,6 +12,15 @@
 --open import Category.HomReasoning
 open import HomReasoning
 open import cat-utility
+open import Category.Cat
+
+module nat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { M : Monad A T η μ } 
+                 { K : Kleisli A T η μ M } where
+
 
 --T(g f) = T(g) T(f)
 
@@ -27,8 +36,6 @@
       → A [ A [  FMap G f o TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
 Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )
 
-open import Category.Cat
-
 -- η :   1_A → T
 -- μ :   TT → T
 -- μ(a)η(T(a)) = a
@@ -111,49 +118,36 @@
      ∎
 
 -- f ○ η(a) = f
-Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 { μ : NTrans A A (T ○ T) T }
-                 ( a  : Obj A )  ( b : Obj A )
+Lemma8 : ( a  : Obj A )  ( b : Obj A )
                  ( f : Hom A a ( FObj T b) )
-                 ( m : Monad A T η μ )
-                 ( k : Kleisli A T η μ m) 
-                      → A  [ join k f (TMap η a)  ≈ f ]
-Lemma8 c T η a b f m k = 
+                      → A  [ join K f (TMap η a)  ≈ f ]
+Lemma8 a b f = 
   begin
-     join k f (TMap η a) 
+     join K f (TMap η a) 
   ≈⟨ refl-hom ⟩
-     c [ TMap μ b  o c [  FMap T f o (TMap η a) ] ]  
+     A [ TMap μ b  o A [  FMap T f o (TMap η a) ] ]  
   ≈⟨ cdr  ( nat η ) ⟩
-     c [ TMap μ b  o c [ (TMap η ( FObj T b)) o f ] ] 
-  ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
-     c [ c [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
-  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩
-     c [ id (FObj T b)  o f ]
-  ≈⟨  IsCategory.identityL (Category.isCategory c)  ⟩
+     A [ TMap μ b  o A [ (TMap η ( FObj T b)) o f ] ] 
+  ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
+     A [ A [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
+  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad K )) ) ⟩
+     A [ id (FObj T b)  o f ]
+  ≈⟨  IsCategory.identityL (Category.isCategory A)  ⟩
      f
   ∎  where 
-      open ≈-Reasoning (c) 
-      μ = mu ( monad k )
+      open ≈-Reasoning (A) 
 
 -- h ○ (g ○ f) = (h ○ g) ○ f
-Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-                 { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
-                 { a b c d : Obj A }
+Lemma9 : { a b c d : Obj A }
                  ( f : Hom A a ( FObj T b) )
                  ( g : Hom A b ( FObj T c) ) 
                  ( h : Hom A c ( FObj T d) )
-                 ( m : Monad A T η μ )
-                 { k : Kleisli A T η μ m}
-                      → A  [ join k h (join k g f)  ≈ join k ( join k h g) f ]
-Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = 
+                      → A  [ join K h (join K g f)  ≈ join K ( join K h g) f ]
+Lemma9 {a} {b} {c} {d} f g h = 
   begin 
-     join k h (join k g f)  
+     join K h (join K g f)  
    ≈⟨⟩
-     join k h (                  ( TMap μ c o ( FMap T g o f ) ) )
+     join K h (                  ( TMap μ c o ( FMap T g o f ) ) )
    ≈⟨ refl-hom ⟩
      ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
    ≈⟨ cdr ( cdr ( assoc )) ⟩
@@ -186,7 +180,7 @@
    ≈⟨ car ( car (
       begin
          ( TMap μ d o TMap μ (FObj T d) )
-      ≈⟨ IsMonad.assoc ( isMonad m) ⟩
+      ≈⟨ IsMonad.assoc ( isMonad M) ⟩
          ( TMap μ d o FMap T (TMap μ d) )
       ∎
    )) ⟩
@@ -198,176 +192,64 @@
    ≈⟨ cdr ( car ( sym ( distr T )))   ⟩
      ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
    ≈⟨ refl-hom ⟩
-     join k ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
+     join K ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
    ≈⟨ refl-hom ⟩
-     join k ( join k h g) f 
+     join K ( join K h g) f 
   ∎ where open ≈-Reasoning (A) 
 
-KHom1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A )  (a : Obj A) → (b : Obj A)  -> Set (c₂ ⊔ c₁)
+KHom1 :  (a : Obj A) → (b : Obj A)  -> Set (c₂ ⊔ c₁)
 KHom1 = {!!}
 
-record KHom  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( T : Functor A A )  (a : Obj A)  (b : Obj A)
+record KHom (a : Obj A)  (b : Obj A)
      : Set (suc (c₂ ⊔ c₁)) where
    field
        KMap :  Hom A a ( FObj T b )
 
-K-id : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } {η : NTrans A A identityFunctor T} {a : Obj A} → KHom A T a a
-K-id {_} {_} {_} {A} {T} {η} {a = a} = record { KMap =  TMap η a } 
+K-id :  {a : Obj A} → KHom a a
+K-id {a = a} = record { KMap =  TMap η a } 
 
 open import Relation.Binary.Core
 
-_⋍_ :  ∀{c₁ c₂ ℓ} {A : Category c₁ c₂ ℓ} { T : Functor A A }
-    { a : Obj A } { b : Obj A } (f g  : KHom A T a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ))
+_⋍_ : 
+    { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ))
 _⋍_ = {!!}
 
+open KHom
 
-_*_ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
-                 { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ } →
-                 { K : Kleisli A T η μ M } →
-       { a b : Obj A } → { c : Obj A } →
-                      ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
-_*_ {_} {_} {_} {_} {_} {_} {_} {_} {K} {a} {b} {c} g f = join K {a} {b} {c} g f
+_*_ : { a b : Obj A } → { c : Obj A } →
+                      ( KHom b c) → (  KHom a b) → KHom a c 
+_*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }
 
-isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-                 { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
-                 ( m : Monad A T η μ )
-                 { k : Kleisli A T η μ m} →
-         IsCategory ( Obj A ) ( KHom A T ) _⋍_ _*_ K-id 
-isKleisliCategory A {T} {η} m = record  { isEquivalence =  isEquivalence A T
+isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id 
+isKleisliCategory  = record  { isEquivalence =  isEquivalence 
                     ; identityL =   KidL
                     ; identityR =   KidR
                     ; o-resp-≈ =    Ko-resp
                     ; associative = Kassoc
                     }
      where
-         isEquivalence : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A ) -> { a b : Obj A } ->
-               IsEquivalence {_} {_} {KHom A T a b} _⋍_
-         isEquivalence A T {C} {D} =
+         isEquivalence :  { a b : Obj A } ->
+               IsEquivalence {_} {_} {KHom a b} _⋍_
+         isEquivalence {C} {D} =
            record { refl  = λ {F} → ⋍-refl {F}
              ; sym   = λ {F} {G} → ⋍-sym {F} {G}
              ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H}
              } where
-                  ⋍-refl : {F : KHom A T C D} → F ⋍ F
+                  ⋍-refl : {F : KHom C D} → F ⋍ F
                   ⋍-refl = {!!}
-                  ⋍-sym : {F G : KHom A T C D} → F ⋍ G → G ⋍ F
+                  ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F
                   ⋍-sym = {!!}
-                  ⋍-trans : {F G H : KHom A T C D} → F ⋍ G → G ⋍ H → F ⋍ H
+                  ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H
                   ⋍-trans = {!!}
-         KidL : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {C D : Obj A} -> {f : KHom A T C D} → (K-id * f) ⋍ f
+         KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
          KidL = {!!}
-         KidR : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {C D : Obj A} -> {f : KHom A T C D} → (f * K-id) ⋍ f
+         KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
          KidR = {!!}
-         Ko-resp : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {a b c : Obj A} -> {f g : KHom A T a b } → {h i : KHom A T b c } → 
+         Ko-resp :  {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom  b c } → 
                           f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
          Ko-resp = {!!}
-         Kassoc :  {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {a b c : Obj A} -> {f g : KHom A T a b } → {h i : KHom A T b c } →
+         Kassoc :   {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
                           (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc = {!!}
 
--- Kleisli :
--- Kleisli = record { Hom = 
---                 ; Hom = _⟶_
---                  ; Id = IdProd
---                  ; _o_ = _∘_
---                  ; _≈_ = _≈_
---                  ; isCategory = record { isEquivalence = record { refl  = λ {φ} → ≈-refl {φ = φ}
---                                                                 ; sym   = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
---                                                                 ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
---                                                                 }
---                                        ; identityL = identityL
---                                        ; identityR = identityR
---                                        ; o-resp-≈ = o-resp-≈
---                                        ; associative = associative
---                                        }
---                  }
 
-----
---
--- Adjunction to Monad
---
-----
-
-open Adjunction
-
-UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                 ( U : Functor B A )
-                 ( F : Functor A B )
-                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) → NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
-UεF A B U F ε =  lemma11  (
-     Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○  U} {identityFunctor} ε F)  ) where
-         lemma11 :   NTrans A A   ( U ○ ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) ) 
-                  →  NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
-         lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
-
-Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                 { U : Functor B A }
-                 { F : Functor A B }
-                 { η : NTrans A A identityFunctor ( U ○  F ) }
-                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
-      Adjunction A B U F η ε  → Monad A (U ○  F) η (UεF A B U F ε)
-Adj2Monad A B {U} {F} {η} {ε} adj = record {
-         isMonad = record {
-                    assoc = assoc1;
-                    unity1 = unity1;
-                    unity2 = unity2
-              }
-      }  where
-           T : Functor A A
-           T = U  ○ F
-           μ : NTrans A A ( T ○ T ) T
-           μ = UεF A B U F ε
-           lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → 
-                 B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ] 
-           lemma-assoc1 f =  IsNTrans.naturality ( isNTrans ε )
-           assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-           assoc1 {a} = let open ≈-Reasoning (A) in
-             begin
-                TMap μ a o TMap μ ( FObj T a )
-             ≈⟨⟩
-                (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F  a )))))
-             ≈⟨ sym (distr U) ⟩
-                FMap U (B [ TMap ε ( FObj F a )  o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
-             ≈⟨  (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
-                FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
-             ≈⟨ distr U ⟩
-                (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
-             ≈⟨⟩
-                TMap μ a o FMap T (TMap μ a) 
-             ∎
-           unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-           unity1 {a} = let open ≈-Reasoning (A) in
-             begin
-               TMap μ a o TMap η ( FObj T a )
-             ≈⟨⟩
-               (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F  a ))
-             ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
-               id (FObj U ( FObj F a ))
-             ≈⟨⟩
-               id (FObj T a)
-             ∎
-           unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-           unity2 {a} = let open ≈-Reasoning (A) in
-             begin
-                TMap μ a o (FMap T (TMap η a ))
-             ≈⟨⟩
-                (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
-             ≈⟨ sym (distr U ) ⟩
-                FMap U ( B [  (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
-             ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
-                FMap U ( id1 B (FObj F a) )
-             ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
-                id (FObj T a)
-             ∎