Mercurial > hg > Members > kono > Proof > category

annotate comparison-functor-conv.agda @ 119:32ef4cdb18a2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nat-μ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2013 15:01:31 +0900
parents b0ba34a27783
children 5f331dfc000b
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 { K' : Kleisli A T η μ M' }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 { 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
27 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 { μ_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
30 ( M : Monad A (U_K ○ F_K) η_K μ_K )
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 ( 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
32 ( 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
33 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 open import nat {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' } { K' }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 open Functor
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 open NTrans
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 open Category.Cat.[_]_~_
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 open MResolution
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ≃-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
42 {F G : Functor C D} → F ≃ G → G ≃ F
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 ≃-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
44 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 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
46 helper (Category.Cat.refl Ff≈Gf) =
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 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
48
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 -- to T=UF constraints happy
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 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
51 {F G : Functor C D} → F ≃ G → F ≃ G
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 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
53 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 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
55 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
56
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 open KleisliHom
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 TtoK : (a b : Obj A) -> (KHom a b) -> {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } ->
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 TtoK _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 TKMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 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
65
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 KtoT : (a b : Obj A) -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } ->
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ([ A ] g ~ h) -> Hom A a (FObj T b)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 KTMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 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
71
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 TKMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ TKMap f ≈ TKMap g ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 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
74 where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 open ≈-Reasoning (A)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 helper : (a b : Obj A) (f g : KHom a b) -> A [ KMap f ≈ KMap g ] ->
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 {conv : Hom A (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] conv ~ conv) -> A [ TKMap f ≈ TKMap g ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 helper _ _ _ _ eq (Category.Cat.refl _) =
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 (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
80
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 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
83
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 open Adjunction
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 K_T : Functor KleisliCategory B
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 K_T = record {
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 FObj = FObj F_K
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 ; FMap = kfmap
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 ; isFunctor = record
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 { ≈-cong = ≈-cong
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ; identity = identity
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 ; distr = distr1
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 }
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 } where
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 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
96 identity {a} = let open ≈-Reasoning (B) in
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 kfmap (K-id {a})
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 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
101 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 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
103 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 id1 B (FObj F_K a)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 ≈-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
108 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 kfmap f
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 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
112 ≈⟨ cdr ( fcong F_K (TKMap-cong f≈g)) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 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
114 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 kfmap g
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 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
118 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
119 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 kfmap (g * f)
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 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
123 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 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
125 ≈⟨ cdr ( distr F_K ) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 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
127 ≈⟨ cdr (cdr ( distr F_K )) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 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
129 ≈⟨ cdr assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 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
131 ≈⟨ cdr (car (car ( fcong F_K ( μ=UεF RK )))) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 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
133 ( 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
134 ≈⟨ sym (cdr assoc) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 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
136 (( 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
137 ≈⟨ assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 (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
139 (( 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
140 ≈⟨ car (sym (nat ε_K)) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 (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
142 (( 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
143 ≈⟨ sym assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 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
145 ((( 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
146 ≈⟨ cdr assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 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
148 (( 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
149 ≈⟨ cdr ( car (
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 begin
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 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
152 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 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
154 ≈⟨ sym (nat ε_K) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 ( 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
156 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 )) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 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
159 ≈⟨ cdr (sym assoc) ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 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
161 ≈⟨ assoc ⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 (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
163 ≈⟨⟩
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 kfmap g o kfmap f
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 ∎
2feec58bb02d seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166