Mercurial > hg > Members > kono > Proof > category

annotate comparison-em.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 d3cd28a71b3f
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- -- -- -- -- -- -- --
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
2 -- Comparison Functor of Eilenberg-Moore Category
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
3 -- defines U^K and F^K as a resolution of Monad
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 -- checks Adjointness
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 --
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 -- -- -- -- -- -- -- --
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Category -- https://github.com/konn/category-agda
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Level
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 --open import Category.HomReasoning
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import HomReasoning
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import cat-utility
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Category.Cat
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Relation.Binary.Core
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
17 module comparison-em
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 { T : Functor A A }
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 { η : NTrans A A identityFunctor T }
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 { μ : NTrans A A (T ○ T) T }
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
22 { M' : IsMonad A T η μ }
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
24 { U^K : Functor B A } { F^K : Functor A B }
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
25 { η^K : NTrans A A identityFunctor ( U^K ○ F^K ) }
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
26 { ε^K : NTrans B B ( F^K ○ U^K ) identityFunctor }
122
f8fbd5ecec97 no yellow on em-category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 121
diff changeset
27 { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
28 ( Adj^K : IsAdjunction A B U^K F^K η^K ε^K )
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
29 where
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 open import adj-monad
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
33 T^K = U^K ○ F^K
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
35 μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K )
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
36 μ^K' = UεF A B U^K F^K ε^K
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
37
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
38 M : IsMonad A (U^K ○ F^K ) η^K μ^K'
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
39 M = Monad.isMonad ( Adj2Monad A B ( record { U = U^K; F = F^K ; η = η^K ; ε = ε^K ; isAdjunction = Adj^K } ) )
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
41 open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K' } { M }
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 open Functor
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 open NTrans
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 open Adjunction
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 open MResolution
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
47 open EMHom
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
49 emkobj : Obj B → EMObj
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
50 emkobj b = record {
465
d3cd28a71b3f clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
51 obj = FObj U^K b ; φ = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b }
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
52 } where
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
53 identity1 : (b : Obj B) → A [ A [ (FMap U^K (TMap ε^K b)) o TMap η^K (FObj U^K b) ] ≈ id1 A (FObj U^K b) ]
125
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
54 identity1 b = let open ≈-Reasoning (A) in
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
55 begin
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
56 (FMap U^K (TMap ε^K b)) o TMap η^K (FObj U^K b)
688
a5f2ca67e7c5 fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 465
diff changeset
57 ≈⟨ IsAdjunction.adjoint1 Adj^K ⟩
125
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
58 id1 A (FObj U^K b)
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
59 ∎
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
60
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
61 eval1 : (b : Obj B) → A [ A [ (FMap U^K (TMap ε^K b)) o TMap μ^K' (FObj U^K b) ] ≈ A [ (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b)) ] ]
125
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
62 eval1 b = let open ≈-Reasoning (A) in
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
63 begin
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
64 (FMap U^K (TMap ε^K b)) o TMap μ^K' (FObj U^K b)
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
65 ≈⟨⟩
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
66 (FMap U^K (TMap ε^K b)) o FMap U^K (TMap ε^K ( FObj F^K (FObj U^K b)))
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
67 ≈⟨ sym (distr U^K) ⟩
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
68 FMap U^K (B [ TMap ε^K b o (TMap ε^K ( FObj F^K (FObj U^K b))) ] )
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
69 ≈⟨ fcong U^K (nat ε^K) ⟩ -- Horizontal composition
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
70 FMap U^K (B [ TMap ε^K b o FMap F^K (FMap U^K (TMap ε^K b)) ] )
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
71 ≈⟨ distr U^K ⟩
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
72 (FMap U^K (TMap ε^K b)) o FMap U^K (FMap F^K (FMap U^K (TMap ε^K b)))
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
73 ≈⟨⟩
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
74 (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b))
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
75 ∎
dec1f5db1edd on going (horizontal composition)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
76
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
124
aaeb92b58647 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
78 open EMObj
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
79 emkmap : {a b : Obj B} (f : Hom B a b) → EMHom (emkobj a) (emkobj b)
124
aaeb92b58647 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
80 emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 a b f
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
81 } where
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
82 homomorphism1 : (a b : Obj B) (f : Hom B a b) → A [ A [ (φ (emkobj b)) o FMap T^K (FMap U^K f) ] ≈ A [ (FMap U^K f) o (φ (emkobj a)) ] ]
126
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
83 homomorphism1 a b f = let open ≈-Reasoning (A) in
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
84 begin
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
85 (φ (emkobj b)) o FMap T^K (FMap U^K f)
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
86 ≈⟨⟩
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
87 FMap U^K (TMap ε^K b) o FMap U^K (FMap F^K (FMap U^K f))
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
88 ≈⟨ sym (distr U^K) ⟩
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
89 FMap U^K ( B [ TMap ε^K b o FMap F^K (FMap U^K f) ] )
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
90 ≈⟨ sym (fcong U^K (nat ε^K)) ⟩
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
91 FMap U^K ( B [ f o TMap ε^K a ] )
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
92 ≈⟨ distr U^K ⟩
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
93 (FMap U^K f) o FMap U^K (TMap ε^K a)
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
94 ≈⟨⟩
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
95 (FMap U^K f) o ( φ (emkobj a))
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
96 ∎
f117cba46532 Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
97
121
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
98
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
99 K^T : Functor B Eilenberg-MooreCategory
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
100 K^T = record {
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
101 FObj = emkobj
324511654f23 add Comparison functor for EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
102 ; FMap = emkmap
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 ; isFunctor = record
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 { ≈-cong = ≈-cong
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 ; identity = identity
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ; distr = distr1
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 }
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 } where
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
109 identity : {a : Obj B} → emkmap (id1 B a) ≗ EM-id {emkobj a}
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
110 identity {a} = let open ≈-Reasoning (A) in
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 begin
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
112 EMap (emkmap (id1 B a))
127
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
113 ≈⟨⟩
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
114 FMap U^K (id1 B a)
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
115 ≈⟨ IsFunctor.identity (isFunctor U^K) ⟩
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
116 id1 A ( FObj U^K a )
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
117 ≈⟨⟩
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
118 EMap (EM-id {emkobj a})
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 ∎
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
120 ≈-cong : {a b : Obj B} → {f g : Hom B a b} → B [ f ≈ g ] → emkmap f ≗ emkmap g
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
121 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 begin
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
123 EMap (emkmap f)
127
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
124 ≈⟨ IsFunctor.≈-cong (isFunctor U^K) f≈g ⟩
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
125 EMap (emkmap g)
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 ∎
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
127 distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → ( (emkmap (B [ g o f ])) ≗ (emkmap g ∙ emkmap f) )
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
128 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 begin
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
130 EMap (emkmap (B [ g o f ] ))
127
3e05417b0876 Comparison Functor for Eilenberg-Moore Category is constructed.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 126
diff changeset
131 ≈⟨ distr U^K ⟩
123
44c58c27d12d problems written Comparison Functor on EM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
132 EMap (emkmap g ∙ emkmap f)
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 ∎
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
135 Lemma-EM20 : { a b : Obj B} { f : Hom B a b } → A [ FMap U^T ( FMap K^T f) ≈ FMap U^K f ]
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
136 Lemma-EM20 {a} {b} {f} = let open ≈-Reasoning (A) in
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
137 begin
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
138 FMap U^T ( FMap K^T f)
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
139 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
140 FMap U^K f
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
141 ∎
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
142
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
143 -- Lemma-EM21 : { a : Obj B} → FObj U^T ( FObj K^T a) = FObj U^K a
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
144
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
145 Lemma-EM22 : { a b : Obj A} { f : Hom A a b } → A [ EMap ( FMap K^T ( FMap F^K f) ) ≈ EMap ( FMap F^T f ) ]
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
146 Lemma-EM22 {a} {b} {f} = let open ≈-Reasoning (A) in
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
147 begin
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
148 EMap ( FMap K^T ( FMap F^K f) )
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
149 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
150 FMap U^K ( FMap F^K f)
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
151 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
152 EMap ( FMap F^T f )
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
153 ∎
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
154
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
155
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
156 -- Lemma-EM23 : { a b : Obj A} → ( FObj K^T ( FObj F^K f) ) = ( FObj F^T f )
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
157
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
158 -- Lemma-EM24 : {a : Obj A } {b : Obj B} → A [ TMap η^K (FObj U^K b) ≈ TMap η^K a ]
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
159 -- Lemma-EM24 = ?
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
160
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
161 Lemma-EM26 : {b : Obj B} → A [ EMap (TMap ε^T ( FObj K^T b)) ≈ FMap U^K ( TMap ε^K b) ]
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
162 Lemma-EM26 {b} = let open ≈-Reasoning (A) in
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
163 begin
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
164 EMap (TMap ε^T ( FObj K^T b))
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
165 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
166 FMap U^K ( TMap ε^K b)
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
167 ∎
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
168
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
169
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
170