Mercurial > hg > Members > kono > Proof > category
annotate comparison-functor.agda @ 98:b0ba34a27783
generated version of comparison functor
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 29 Jul 2013 16:49:11 +0900 |
parents | |
children | bd542a1caf08 |
rev | line source |
---|---|
98
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 -- -- -- -- -- -- -- -- |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 -- Comparison Functor of Kelisli Category |
b0ba34a27783
generated version of 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 |
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 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 module comparison-functor |
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 } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 { M' : Monad A T η μ } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 { K' : Kleisli A T η μ M' } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 { U_K : Functor B A } { F_K : Functor A B } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } |
b0ba34a27783
generated version of 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 ) } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 ( AdjK : Adjunction A B U_K F_K η_K ε_K ) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK ) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 where |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 open import adj-monad |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 μ_K = UεF A B U_K F_K ε_K |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 M : Monad A (U_K ○ F_K ) η_K μ_K |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 -- M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 K : Kleisli A (U_K ○ F_K ) η_K μ_K M |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 K = record {} |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 open import nat {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } { K } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 open Functor |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 open NTrans |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 open Kleisli |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 open KleisliHom |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 open Adjunction |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 open MResolution |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 K_T : Functor KleisliCategory B |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 K_T = record { |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 FObj = FObj F_K |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 ; FMap = kfmap |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 ; isFunctor = record |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 { ≈-cong = ≈-cong |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 ; identity = identity |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 ; distr = distr1 |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 } |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 } where |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ] |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 identity {a} = let open ≈-Reasoning (B) in |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 begin |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 kfmap (K-id {a}) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a})) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 id1 B (FObj F_K a) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 begin |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 kfmap f |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 TMap ε_K (FObj F_K b) o FMap F_K (KMap f) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 ≈⟨ cdr ( fcong F_K f≈g) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 TMap ε_K (FObj F_K b) o FMap F_K (KMap g) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 kfmap g |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )] |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 begin |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 kfmap (g * f) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 TMap ε_K (FObj F_K c) o FMap F_K (KMap (g * f)) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ] ] ) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 ≈⟨ cdr ( distr F_K ) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (KMap g) o KMap f ]))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
99 ≈⟨ cdr (cdr ( distr F_K )) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (KMap g))) o (FMap F_K (KMap f)))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 ≈⟨ cdr assoc ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
102 TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 ( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 ≈⟨ sym (cdr assoc) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
108 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f)))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
109 ≈⟨ assoc ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
110 (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 ≈⟨ car (sym (nat ε_K)) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))) o (FMap F_K (KMap f))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 ≈⟨ sym assoc ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
117 ((( FMap F_K (FMap (U_K ○ F_K) (KMap g)))) o (FMap F_K (KMap f)))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
118 ≈⟨ cdr assoc ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 (( FMap F_K (FMap (U_K ○ F_K) (KMap g))))) o (FMap F_K (KMap f))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 ≈⟨ cdr ( car ( |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 begin |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (KMap g)))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
124 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
125 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (KMap g))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
126 ≈⟨ sym (nat ε_K) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
127 ( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b)) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
128 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
129 )) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
130 TMap ε_K (FObj F_K c) o ((( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (KMap f)) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
131 ≈⟨ cdr (sym assoc) ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
132 TMap ε_K (FObj F_K c) o (( FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f))) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
133 ≈⟨ assoc ⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
134 (TMap ε_K (FObj F_K c) o FMap F_K (KMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (KMap f)) |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
135 ≈⟨⟩ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
136 kfmap g o kfmap f |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
137 ∎ |
b0ba34a27783
generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
138 |