Mercurial > hg > Members > kono > Proof > category

annotate adj-monad.agda @ 586:c78df4c0453c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 11 May 2017 17:06:27 +0900
parents 5f331dfc000b
children a5f2ca67e7c5
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- Monad
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 -- Category A
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 -- A = Category
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 -- Functor T : A → A
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 --T(a) = t(a)
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 --T(f) = tf(f)
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Category -- https://github.com/konn/category-agda
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Level
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 --open import Category.HomReasoning
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import HomReasoning
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import cat-utility
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Category.Cat
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 module adj-monad where
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 ----
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 --
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 -- Adjunction to Monad
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 --
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 ----
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open Adjunction
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 open NTrans
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 open Functor
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 ( U : Functor B A )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 ( F : Functor A B )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 ( ε : NTrans B B ( F ○ U ) identityFunctor ) → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 UεF A B U F ε = lemma11 (
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) where
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
35 lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }}
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 { U : Functor B A }
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 { F : Functor A B }
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 { η : NTrans A A identityFunctor ( U ○ F ) }
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 { ε : NTrans B B ( F ○ U ) identityFunctor } →
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 Adjunction A B U F η ε → Monad A (U ○ F) η (UεF A B U F ε)
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 Adj2Monad A B {U} {F} {η} {ε} adj = record {
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 isMonad = record {
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 assoc = assoc1;
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 unity1 = unity1;
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 unity2 = unity2
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 }
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 } where
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 T : Functor A A
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 T = U ○ F
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 μ : NTrans A A ( T ○ T ) T
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 μ = UεF A B U F ε
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) →
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ]
130
5f331dfc000b remove Kleisli record
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
56 lemma-assoc1 f = IsNTrans.commute ( isNTrans ε )
72
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 assoc1 {a} = let open ≈-Reasoning (A) in
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 begin
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 TMap μ a o TMap μ ( FObj T a )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ≈⟨⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F a )))))
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ≈⟨ sym (distr U) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 FMap U (B [ TMap ε ( FObj F a ) o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ≈⟨ distr U ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ≈⟨⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 TMap μ a o FMap T (TMap μ a)
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ∎
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 unity1 {a} = let open ≈-Reasoning (A) in
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 begin
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 TMap μ a o TMap η ( FObj T a )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 ≈⟨⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F a ))
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 id (FObj U ( FObj F a ))
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 ≈⟨⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 id (FObj T a)
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 ∎
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 unity2 {a} = let open ≈-Reasoning (A) in
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 begin
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 TMap μ a o (FMap T (TMap η a ))
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 ≈⟨⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 ≈⟨ sym (distr U ) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 FMap U ( id1 B (FObj F a) )
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 id (FObj T a)
cbc30519e961 stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ∎