Mercurial > hg > Members > kono > Proof > category

comparison adj-monad.agda @ 688:a5f2ca67e7c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix monad/adjunction definition couniversal to limit does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Nov 2017 21:34:58 +0900
parents 5f331dfc000b
children
comparison
equal deleted inserted replaced
687:d0bc017c6b61 688:a5f2ca67e7c5
18 -- 18 --
19 -- Adjunction to Monad 19 -- Adjunction to Monad
20 -- 20 --
21 ---- 21 ----
22 22
23 open Adjunction
24 open NTrans 23 open NTrans
25 open Functor 24 open Functor
26 25
27 UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 26 UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
28 ( U : Functor B A ) 27 ( U : Functor B A )
33 lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) ) 32 lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) )
34 → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) 33 → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
35 lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }} 34 lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }}
36 35
37 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 36 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
38 { U : Functor B A } 37 → Adjunction A B → Monad A
39 { F : Functor A B } 38 Adj2Monad A B adj = record {
40 { η : NTrans A A identityFunctor ( U ○ F ) } 39 T = T ;
41 { ε : NTrans B B ( F ○ U ) identityFunctor } → 40 η = η ;
42 Adjunction A B U F η ε → Monad A (U ○ F) η (UεF A B U F ε) 41 μ = μ ;
43 Adj2Monad A B {U} {F} {η} {ε} adj = record {
44 isMonad = record { 42 isMonad = record {
45 assoc = assoc1; 43 assoc = assoc1;
46 unity1 = unity1; 44 unity1 = unity1;
47 unity2 = unity2 45 unity2 = unity2
48 } 46 }
49 } where 47 } where
48 U : Functor B A
49 U = Adjunction.U adj
50 F : Functor A B
51 F = Adjunction.F adj
52 η : NTrans A A identityFunctor ( U ○ F )
53 η = Adjunction.η adj
54 ε : NTrans B B ( F ○ U ) identityFunctor
55 ε = Adjunction.ε adj
50 T : Functor A A 56 T : Functor A A
51 T = U ○ F 57 T = U ○ F
52 μ : NTrans A A ( T ○ T ) T 58 μ : NTrans A A ( T ○ T ) T
53 μ = UεF A B U F ε 59 μ = UεF A B U F ε
54 lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → 60 lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) →
73 unity1 {a} = let open ≈-Reasoning (A) in 79 unity1 {a} = let open ≈-Reasoning (A) in
74 begin 80 begin
75 TMap μ a o TMap η ( FObj T a ) 81 TMap μ a o TMap η ( FObj T a )
76 ≈⟨⟩ 82 ≈⟨⟩
77 (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F a )) 83 (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F a ))
78 ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩ 84 ≈⟨ IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ⟩
79 id (FObj U ( FObj F a )) 85 id (FObj U ( FObj F a ))
80 ≈⟨⟩ 86 ≈⟨⟩
81 id (FObj T a) 87 id (FObj T a)
82 ∎ 88 ∎
83 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] 89 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
86 TMap μ a o (FMap T (TMap η a )) 92 TMap μ a o (FMap T (TMap η a ))
87 ≈⟨⟩ 93 ≈⟨⟩
88 (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a ))) 94 (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
89 ≈⟨ sym (distr U ) ⟩ 95 ≈⟨ sym (distr U ) ⟩
90 FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ]) 96 FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
91 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ 97 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩
92 FMap U ( id1 B (FObj F a) ) 98 FMap U ( id1 B (FObj F a) )
93 ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩ 99 ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
94 id (FObj T a) 100 id (FObj T a)
95 ∎ 101 ∎