Mercurial > hg > Members > kono > Proof > category

comparison monoidal.agda @ 708:975aa343a963

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets is Monoidal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 Nov 2017 09:34:15 +0900
parents 808b03184fd3
children 2807335e3fa0
comparison
equal deleted inserted replaced
707:808b03184fd3 708:975aa343a963
1 open import Level
2 open import Level
3 open import Level 1 open import Level
4 open import Category 2 open import Category
5 module monoidal where 3 module monoidal where
6 4
7 open import Data.Product renaming (_×_ to _*_) 5 open import Data.Product renaming (_×_ to _*_)
289 _●_ : (x y : Obj D ) → Obj D 287 _●_ : (x y : Obj D ) → Obj D
290 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y 288 _●_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
291 field 289 field
292 MF : Functor C D 290 MF : Functor C D
293 unit : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) ) 291 unit : Hom D (Monoidal.m-i N) (FObj MF (Monoidal.m-i M) )
294 ** : {a b : Obj C} → Hom D ((FObj MF a) ● (FObj MF b )) ( FObj MF ( a ⊗ b ) ) 292 φ : {a b : Obj C} → Hom D ((FObj MF a) ● (FObj MF b )) ( FObj MF ( a ⊗ b ) )
295 293
296 open import Category.Sets 294 open import Category.Sets
297 295
298 import Relation.Binary.PropositionalEquality 296 import Relation.Binary.PropositionalEquality
299 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) 297 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
300 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 298 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
301 299
302 data One {c : Level} : Set c where 300 data One {c : Level} : Set c where
303 OneObj : One -- () in Haskell ( or any one object set ) 301 OneObj : One -- () in Haskell ( or any one object set )
304 302
305 isoSets :{c₁ : Level} {a : Obj (Sets {c₁} ) } → Iso (Sets {c₁}) a ( a * One {c₁} ) 303 SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} ) (Sets {c})
306 isoSets {a} = record { 304 SetsTensorProduct = record {
307 ≅→ = λ x → ( x , OneObj ) ; 305 FObj = λ x → proj₁ x * proj₂ x
308 ≅← = λ x → proj₁ x ; 306 ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f) (proj₂ f)
309 iso→ = refl ; 307 ; isFunctor = record {
310 iso← = iso← 308 ≈-cong = ≈-cong
309 ; identity = refl
310 ; distr = refl
311 } 311 }
312 where 312 } where
313 lemma : {a : Obj Sets } → (x : a * One) → (Sets [ (λ x₁ → x₁ , OneObj) o proj₁ ]) x ≡ id1 Sets (a * One) x 313 ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} →
314 lemma (_ , OneObj ) = refl 314 (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ]
315 iso← : {a : Obj Sets} → Sets [ Sets [ (λ x → x , OneObj) o proj₁ ] ≈ id1 Sets (a * One) ] 315 ≈-cong (refl , refl) = refl
316 iso← {a} = extensionality Sets ( λ x → lemma x ) 316
317
318
319 MonoidalSets : {c : Level} → Monoidal (Sets {c})
320 MonoidalSets = record {
321 m-i = One ;
322 m-bi = SetsTensorProduct ;
323 isMonoidal = record {
324 mα-iso = record { ≅→ = mα→ ; ≅← = mα← ; iso→ = refl ; iso← = refl } ;
325 mλ-iso = record { ≅→ = mλ→ ; ≅← = mλ← ; iso→ = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ;
326 mρ-iso = record { ≅→ = mρ→ ; ≅← = mρ← ; iso→ = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ;
327 mα→nat1 = λ f → refl ;
328 mα→nat2 = λ f → refl ;
329 mα→nat3 = λ f → refl ;
330 mλ→nat = λ f → refl ;
331 mρ→nat = λ f → refl ;
332 comm-penta = refl ;
333 comm-unit = refl
334 }
335 } where
336 _⊗_ : ( a b : Obj Sets ) → Obj Sets
337 _⊗_ a b = FObj SetsTensorProduct (a , b )
338 mα→ : {a b c : Obj Sets} → Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
339 mα→ ((a , b) , c ) = (a , ( b , c ) )
340 mα← : {a b c : Obj Sets} → Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c )
341 mα← (a , ( b , c ) ) = ((a , b) , c )
342 mλ→ : {a : Obj Sets} → Hom Sets ( One ⊗ a ) a
343 mλ→ (_ , a) = a
344 mλ← : {a : Obj Sets} → Hom Sets a ( One ⊗ a )
345 mλ← a = ( OneObj , a )
346 mλiso : {a : Obj Sets} (x : One ⊗ a) → (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x
347 mλiso (OneObj , _ ) = refl
348 mρ→ : {a : Obj Sets} → Hom Sets ( a ⊗ One ) a
349 mρ→ (a , _) = a
350 mρ← : {a : Obj Sets} → Hom Sets a ( a ⊗ One )
351 mρ← a = ( a , OneObj )
352 mρiso : {a : Obj Sets} (x : a ⊗ One ) → (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
353 mρiso (_ , OneObj ) = refl
354
317 355
318 356
319 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 357 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
320 : Set (suc (suc c₁)) where 358 : Set (suc (suc c₁)) where
321 field 359 field
322 unit : FObj f One 360 unit : FObj f One
323 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) ) 361 φ : {a b : Obj Sets} → Hom Sets ((FObj f a) * (FObj f b )) ( FObj f ( a * b ) )
324 ** : {a b : Obj Sets} → FObj f a → FObj f b → FObj f ( a * b ) 362 ** : {a b : Obj Sets} → FObj f a → FObj f b → FObj f ( a * b )
325 ** x y = φ ( x , y ) 363 ** x y = φ ( x , y )
326 364
327 -- HaskellMonoidalFunctor f → MonoidalFunctor 365 lemma0 : {c : Level} ( f : Functor (Sets {c}) (Sets {c}) ) → HaskellMonoidalFunctor f → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
366 lemma0 f = {!!}
328 367
329 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) 368 record Applicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
330 : Set (suc (suc c₁)) where 369 : Set (suc (suc c₁)) where
331 field 370 field
332 pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) 371 pure : {a : Obj Sets} → Hom Sets a ( FObj f a )
346 lemma2 f mono = record { pure = pure ; <*> = <*> } 385 lemma2 f mono = record { pure = pure ; <*> = <*> }
347 where 386 where
348 open HaskellMonoidalFunctor 387 open HaskellMonoidalFunctor
349 pure : {a : Obj Sets} → Hom Sets a ( FObj f a ) 388 pure : {a : Obj Sets} → Hom Sets a ( FObj f a )
350 pure {a} x = FMap f ( λ y → x ) (unit mono) 389 pure {a} x = FMap f ( λ y → x ) (unit mono)
351 <*> : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b 390 <*> : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b -- ** mono x y
352 <*> {a} {b} x y = FMap f ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) ( ** mono x y ) 391 <*> {a} {b} x y = FMap f ( λ a→b*b → ( proj₁ a→b*b ) ( proj₂ a→b*b ) ) (φ mono ( x , y ))