Mercurial > hg > Members > kono > Proof > category

annotate comparison-functor.agda @ 152:5435469c6cf0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Aug 2013 21:08:33 +0900
parents 5f331dfc000b
children d6a6dd305da2
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 -- -- -- -- -- -- -- --
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 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 { 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
25 { η_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
26 { ε_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
27 { μ_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
28 ( 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
29 ( 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
30 where
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 open import adj-monad
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
99
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
34 T_K = U_K ○ F_K
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
35
98
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 μ_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
37 μ_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
38
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 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
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 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
42
152
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 130
diff changeset
43 open import kleisli {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
44
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 open Functor
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 open NTrans
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 open KleisliHom
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 open Adjunction
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 open MResolution
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 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
52 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
53
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 K_T : Functor KleisliCategory B
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 K_T = record {
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 FObj = FObj F_K
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 ; FMap = kfmap
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 ; isFunctor = record
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 { ≈-cong = ≈-cong
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ; identity = identity
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ; distr = distr1
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 }
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 } where
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 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
65 identity {a} = let open ≈-Reasoning (B) in
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 begin
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 kfmap (K-id {a})
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 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
70 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 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
72 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 id1 B (FObj F_K a)
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 ∎
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ≈-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
76 ≈-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
77 begin
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 kfmap f
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 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
81 ≈⟨ cdr ( fcong F_K f≈g) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 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
83 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 kfmap g
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 ∎
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 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
87 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
88 begin
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 kfmap (g * f)
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 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
92 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 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
94 ≈⟨ cdr ( distr F_K ) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 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
96 ≈⟨ cdr (cdr ( distr F_K )) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 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
98 ≈⟨ cdr assoc ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 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
100 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 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
102 ( 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 ≈⟨ sym (cdr assoc) ⟩
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 ≈⟨ 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 ≈⟨ car (sym (nat ε_K)) ⟩
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 ( 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
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 ≈⟨ sym assoc ⟩
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 ≈⟨ cdr 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 ( car (
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 begin
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 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
121 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 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
123 ≈⟨ sym (nat ε_K) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 ( 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
125 ∎
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 )) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 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
128 ≈⟨ cdr (sym assoc) ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 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
130 ≈⟨ assoc ⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 (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
132 ≈⟨⟩
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 kfmap g o kfmap f
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 ∎
b0ba34a27783 generated version of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135
99
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
136 Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) -> B [ FMap K_T ( FMap F_T f) ≈ FMap F_K f ]
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
137 Lemma-K1 {a} {b} f = let open ≈-Reasoning (B) in
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
138 begin
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
139 FMap K_T ( FMap F_T f)
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
140 ≈⟨⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
141 TMap ε_K (FObj F_K b) o FMap F_K (KMap( FMap F_T f))
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
142 ≈⟨⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
143 TMap ε_K (FObj F_K b) o FMap F_K (A [ TMap η_K b o f ])
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
144 ≈⟨ cdr ( distr F_K) ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
145 TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f )
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
146 ≈⟨ assoc ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
147 (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
148 ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
149 id1 B (FObj F_K b) o FMap F_K f
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
150 ≈⟨ idL ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
151 FMap F_K f
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
152 ∎
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
153
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
154 Lemma-K2 : {a b : Obj A} ( f : KHom a b ) -> A [ FMap U_K ( FMap K_T f) ≈ FMap U_T f ]
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
155 Lemma-K2 {a} {b} f = let open ≈-Reasoning (A) in
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
156 begin
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
157 FMap U_K ( FMap K_T f)
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
158 ≈⟨⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
159 FMap U_K ( B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ] )
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
160 ≈⟨ distr U_K ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
161 FMap U_K ( TMap ε_K (FObj F_K b)) o FMap U_K (FMap F_K (KMap f) )
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
162 ≈⟨⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
163 TMap μ_K b o FMap T_K (KMap f)
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
164 ≈⟨⟩ -- the definition
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
165 FMap U_T f
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
166 ∎
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
167
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
168 Lemma-K3 : (b : Obj A) -> B [ FMap K_T (record { KMap = (TMap η_K b) }) ≈ id1 B (FObj F_K b) ]
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
169 Lemma-K3 b = let open ≈-Reasoning (B) in
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
170 begin
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
171 FMap K_T (record { KMap = (TMap η_K b) })
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
172 ≈⟨⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
173 TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
174 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
175 id1 B (FObj F_K b)
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
176 ∎
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
177
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
178 Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) ->
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
179 B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] }) ≈ FMap F_K g ]
99
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
180 Lemma-K4 b c g = let open ≈-Reasoning (B) in
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
181 begin
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
182 FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] })
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
183 ≈⟨⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
184 TMap ε_K (FObj F_K (FObj T_K c)) o FMap F_K (A [ (TMap η_K (FObj T_K c)) o g ])
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
185 ≈⟨ cdr (distr F_K) ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
186 TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)) o FMap F_K g )
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
187 ≈⟨ assoc ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
188 (TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)))) o FMap F_K g
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
189 ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
190 id1 B (FObj F_K (FObj T_K c)) o FMap F_K g
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
191 ≈⟨ idL ⟩
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
192 FMap F_K g
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
193 ∎
bd542a1caf08 uniquness of comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
194
128
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
195 -- Lemma-K5 : (a : Obj A) -> FObj U_K ( FObj K_T a ) = U_T a
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
196
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
197 Lemma-K6 : (b c : Obj A) (g : KHom b c) -> A [ FMap U_K ( FMap K_T g ) ≈ FMap U_T g ]
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
198 Lemma-K6 b c g = let open ≈-Reasoning (A) in
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
199 begin
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
200 FMap U_K ( FMap K_T g )
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
201 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
202 FMap U_K ( B [ TMap ε_K ( FObj F_K c ) o FMap F_K (KMap g) ] )
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
203 ≈⟨ distr U_K ⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
204 FMap U_K ( TMap ε_K ( FObj F_K c )) o FMap U_K ( FMap F_K (KMap g) )
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
205 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
206 TMap μ_K c o FMap U_K ( FMap F_K (KMap g) )
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
207 ≈⟨⟩
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
208 FMap U_T g
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
209 ∎
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
210
276f33602700 Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 99
diff changeset
211