Mercurial > hg > Members > kono > Proof > category

annotate comparison-functor-conv.agda @ 352:f589e71875ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bad approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Dec 2014 22:16:20 +0900
parents d6a6dd305da2
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- -- -- -- -- -- -- --
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 -- Comparison Functor of Kelisli Category
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 -- defines U_K and F_K as a resolution of Monad
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 -- checks Adjointness
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 --
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 -- -- -- -- -- -- -- --
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Category -- https://github.com/konn/category-agda
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Level
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 --open import Category.HomReasoning
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import HomReasoning
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import cat-utility
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Category.Cat
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Relation.Binary.Core
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 97
diff changeset
18 module comparison-functor-conv
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 { T : Functor A A }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 { η : NTrans A A identityFunctor T }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 { μ : NTrans A A (T ○ T) T }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 { M' : Monad A T η μ }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 { U_K : Functor B A } { F_K : Functor A B }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 ( M : Monad A (U_K ○ F_K) η_K μ_K )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 ( AdjK : Adjunction A B U_K F_K η_K ε_K )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K} AdjK )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
152
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
34 open import kleisli {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' }
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 open Functor
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 open NTrans
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 open Category.Cat.[_]_~_
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 open MResolution
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ≃-sym : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 {F G : Functor C D} → F ≃ G → G ≃ F
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 ≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 helper (Category.Cat.refl Ff≈Gf) =
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 -- to T=UF constraints happy
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 hoge : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 {F G : Functor C D} → F ≃ G → F ≃ G
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 hoge {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] f ~ g
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl Ff≈Gf
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 open KleisliHom
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
58 RHom = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
59 TtoK : (a b : Obj A) → (KHom a b) → {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } →
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
60 ([ A ] g ~ h) → Hom A a (FObj ( U_K ○ F_K ) b)
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 TtoK _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ]
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
62 TKMap : {a b : Obj A} → (f : KHom a b) → Hom A a (FObj ( U_K ○ F_K ) b)
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 TKMap {a} {b} f = TtoK a b f {_} {_} ((hoge (T=UF RK)) (id1 A b))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
65 KtoT : (a b : Obj A) → (RHom a b) → {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } →
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
66 ([ A ] g ~ h) → Hom A a (FObj T b)
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ]
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
68 KTMap : {a b : Obj A} → (f : RHom a b) → Hom A a (FObj T b)
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 KTMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
71 TKMap-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ TKMap f ≈ TKMap g ]
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 TKMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b ))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 open ≈-Reasoning (A)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
75 helper : (a b : Obj A) (f g : KHom a b) → A [ KMap f ≈ KMap g ] →
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
76 {conv : Hom A (FObj T b) (FObj ( U_K ○ F_K ) b) } → ([ A ] conv ~ conv) → A [ TKMap f ≈ TKMap g ]
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 helper _ _ _ _ eq (Category.Cat.refl _) =
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq refl-hom
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
80 kfmap : {a b : Obj A} (f : KHom a b) → Hom B (FObj F_K a) (FObj F_K b)
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (TKMap f) ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 open Adjunction
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 K_T : Functor KleisliCategory B
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 K_T = record {
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 FObj = FObj F_K
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 ; FMap = kfmap
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 ; isFunctor = record
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 { ≈-cong = ≈-cong
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 ; identity = identity
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ; distr = distr1
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 } where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 identity {a} = let open ≈-Reasoning (B) in
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 kfmap (K-id {a})
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 TMap ε_K (FObj F_K a) o FMap F_K (TKMap (K-id {a}))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 id1 B (FObj F_K a)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 ∎
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 152
diff changeset
105 ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
97
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 kfmap f
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 TMap ε_K (FObj F_K b) o FMap F_K (TKMap f)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 ≈⟨ cdr ( fcong F_K (TKMap-cong f≈g)) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 TMap ε_K (FObj F_K b) o FMap F_K (TKMap g)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 kfmap g
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 kfmap (g * f)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 TMap ε_K (FObj F_K c) o FMap F_K (TKMap (g * f))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (TKMap g) o TKMap f ] ] )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 ≈⟨ cdr ( distr F_K ) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (TKMap g) o TKMap f ])))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 ≈⟨ cdr (cdr ( distr F_K )) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (TKMap g))) o (FMap F_K (TKMap f))))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 ≈⟨ cdr assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (TKMap g))))) o (FMap F_K (TKMap f)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 ≈⟨ cdr (car (car ( fcong F_K ( μ=UεF RK )))) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 ( FMap F_K (FMap (U_K ○ F_K) (TKMap g)))) o (FMap F_K (TKMap f)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 ≈⟨ sym (cdr assoc) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f))))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 ≈⟨ assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 ≈⟨ car (sym (nat ε_K)) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 ≈⟨ sym assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 ((( FMap F_K (FMap (U_K ○ F_K) (TKMap g)))) o (FMap F_K (TKMap f))))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 ≈⟨ cdr assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))))) o (FMap F_K (TKMap f)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 ≈⟨ cdr ( car (
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (TKMap g))))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (TKMap g)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 ≈⟨ sym (nat ε_K) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 ( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 )) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 TMap ε_K (FObj F_K c) o ((( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (TKMap f))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 ≈⟨ cdr (sym assoc) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 TMap ε_K (FObj F_K c) o (( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (TKMap f)))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 ≈⟨ assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 (TMap ε_K (FObj F_K c) o FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (TKMap f))
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 kfmap g o kfmap f
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165