Mercurial > hg > Members > kono > Proof > category

comparison discrete.agda @ 455:55a9b6177ed4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 14:58:40 +0900
parents 2f07f4dd9a6d
children 4d97955ea419
comparison
equal deleted inserted replaced
454:2f07f4dd9a6d 455:55a9b6177ed4
24 --- -----→ 24 --- -----→
25 --- 0 1 25 --- 0 1
26 --- -----→ 26 --- -----→
27 --- g 27 --- g
28 28
29 data Arrow {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where 29 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where
30 id-t0 : Arrow t0 t0 30 id-t0 : TwoHom t0 t0
31 id-t1 : Arrow t1 t1 31 id-t1 : TwoHom t1 t1
32 arrow-f : Arrow t0 t1 32 arrow-f : TwoHom t0 t1
33 arrow-g : Arrow t0 t1 33 arrow-g : TwoHom t0 t1
34 34
35 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set ( c₂) where 35
36 field 36 comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c
37 hom : Arrow {c₁} {c₂} a b
38
39 comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Arrow {c₁} {c₂} b c → Arrow {c₁} {c₂} a b → Arrow {c₁} {c₂} a c
40 comp {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f 37 comp {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f
41 comp {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g 38 comp {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g
42 comp {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 39 comp {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1
43 comp {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f 40 comp {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f
44 comp {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g 41 comp {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g
45 comp {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 42 comp {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0
46 43
47 open TwoHom 44 open TwoHom
48 45
49 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c ) 46 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c )
50 _×_ {c₁} {c₂} {a} {b} {c} f g = record { hom = comp {c₁} {c₂} {a} {b} {c} (hom f) (hom g ) } 47 _×_ {c₁} {c₂} {a} {b} {c} f g = comp {c₁} {c₂} {a} {b} {c} f g
51 48
52 49
53 -- f g h 50 -- f g h
54 -- d <- c <- b <- a 51 -- d <- c <- b <- a
55 -- 52 --
56 -- It can be proved without Arrow constraints 53 -- It can be proved without TwoHom constraints
57 54
58 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } 55 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} }
59 {f : (TwoHom {c₁} {c₂ } c d )} → 56 {f : (TwoHom {c₁} {c₂ } c d )} →
60 {g : (TwoHom {c₁} {c₂ } b c )} → 57 {g : (TwoHom {c₁} {c₂ } b c )} →
61 {h : (TwoHom {c₁} {c₂ } a b )} → 58 {h : (TwoHom {c₁} {c₂ } a b )} →
62 hom ( f × (g × h)) ≡ hom ((f × g) × h ) 59 ( f × (g × h)) ≡ ((f × g) × h )
63 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with hom f | hom g | hom h 60 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with f | g | h
64 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl 61 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl
65 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl 62 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl
66 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl 63 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl
67 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-f | id-t0 = refl 64 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-f | id-t0 = refl
68 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-g | id-t0 = refl 65 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-g | id-t0 = refl
69 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-f = refl 66 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-f = refl
70 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-g = refl 67 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-g = refl
71 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl 68 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl
72 69
73 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) 70 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a )
74 TwoId {_} {_} t0 = record { hom = id-t0 } 71 TwoId {_} {_} t0 = id-t0
75 TwoId {_} {_} t1 = record { hom = id-t1 } 72 TwoId {_} {_} t1 = id-t1
76 73
77 open import Relation.Binary 74 open import Relation.Binary
78 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) 75 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
79 76
80 TwoCat : {c₁ c₂ ℓ : Level } → Category c₁ c₂ c₂ 77 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂
81 TwoCat {c₁} {c₂} {ℓ} = record { 78 TwoCat {c₁} {c₂} = record {
82 Obj = TwoObject {c₁} ; 79 Obj = TwoObject {c₁} ;
83 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ; 80 Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ;
84 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ; 81 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
85 _≈_ = λ x y → hom x ≡ hom y ; 82 _≈_ = λ x y → x ≡ y ;
86 Id = λ{a} → TwoId {c₁ } { c₂} a ; 83 Id = λ{a} → TwoId {c₁ } { c₂} a ;
87 isCategory = record { 84 isCategory = record {
88 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; 85 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
89 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ; 86 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ;
90 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ; 87 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ;
91 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ; 88 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
92 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} 89 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
93 } 90 }
94 } where 91 } where
95 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ((TwoId B) × f) ≡ hom f 92 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f
96 identityL {c₁} {c₂} {a} {b} {f} with hom f 93 identityL {c₁} {c₂} {a} {b} {f} with f
97 identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl 94 identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl
98 identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl 95 identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl
99 identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl 96 identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl
100 identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl 97 identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl
101 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) ≡ hom f 98 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f
102 identityR {c₁} {c₂} {_} {_} {f} with hom f 99 identityR {c₁} {c₂} {_} {_} {f} with f
103 identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl 100 identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl
104 identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl 101 identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl
105 identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl 102 identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl
106 identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl 103 identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl
107 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → 104 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} →
108 hom f ≡ hom g → hom h ≡ hom i → hom ( h × f ) ≡ hom ( i × g ) 105 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
109 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = 106 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i =
110 let open ≡-Reasoning in begin 107 let open ≡-Reasoning in begin
111 hom ( h × f ) 108 ( h × f )
112 ≡⟨ refl ⟩ 109 ≡⟨ refl ⟩
113 comp (hom h) (hom f) 110 comp (h) (f)
114 ≡⟨ cong (λ x → comp ( hom h ) x ) f==g ⟩ 111 ≡⟨ cong (λ x → comp ( h ) x ) f==g ⟩
115 comp (hom h) (hom g) 112 comp (h) (g)
116 ≡⟨ cong (λ x → comp x ( hom g ) ) h==i ⟩ 113 ≡⟨ cong (λ x → comp x ( g ) ) h==i ⟩
117 comp (hom i) (hom g) 114 comp (i) (g)
118 ≡⟨ refl ⟩ 115 ≡⟨ refl ⟩
119 hom ( i × g ) 116 ( i × g )
120 ∎ 117 ∎
121 118
122 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → 119 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A
123 (obj→ : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoHom {c₁} {c₂} (obj→ a) (obj→ b) ) → Functor A A 120 indexFunctor {c₁} {c₂} {ℓ} A a b f g = record {
124 indexFunctor {c₁} {c₂} {ℓ} A a b f g obj→ hom→ = record {
125 FObj = λ a → fobj a 121 FObj = λ a → fobj a
126 ; FMap = λ {a} {b} f → fmap {a} {b} f 122 ; FMap = λ {a} {b} f → fmap {a} {b} f
127 ; isFunctor = record { 123 ; isFunctor = record {
128 identity = λ{x} → identity x 124 identity = λ{x} → identity x
129 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} 125 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
130 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} 126 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
131 } 127 }
132 } where 128 } where
133 fobj : Obj A → Obj A 129 T = TwoCat {c₁} {c₂}
134 fobj x with obj→ x 130 fobj : Obj T → Obj A
135 fobj x | t0 = a 131 fobj t0 = a
136 fobj x | t1 = b 132 fobj t1 = b
137 fmap : {x y : Obj A } → (Hom A x y ) → Hom A (fobj x) (fobj y) 133 fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y)
138 fmap {x} {y} h with obj→ x | obj→ y | hom ( hom→ h ) 134 fmap {t0} {t0} id-t0 = id1 A a
139 fmap h | t0 | t0 | id-t0 = id1 A a 135 fmap {t1} {t1} id-t1 = id1 A b
140 fmap h | t1 | t1 | id-t1 = id1 A b 136 fmap {t0} {t1} arrow-f = f
141 fmap h | t0 | t1 | arrow-f = f 137 fmap {t0} {t1} arrow-g = g
142 fmap h | t0 | t1 | arrow-g = g 138 ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ]
143 ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ] 139 ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom
144 ≈-cong {a} {b} {f} {g} f≈g = {!!} 140 identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ]
145 identity : (x : Obj A ) -> A [ {!!} ≈ {!!} ] -- {!!} -- A [ fmap (id1 A x) ≈ id1 A (fobj x) ] 141 identity t0 = let open ≈-Reasoning A in refl-hom
146 identity x with obj→ x 142 identity t1 = let open ≈-Reasoning A in refl-hom
147 identity x | t0 = let open ≈-Reasoning (A) in begin 143 distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
148 fmap (id1 A x) 144 A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ]
149 ≈⟨ {!!} ⟩ 145 distr1 {a} {b} {c} {f} {g} with f | g
150 id1 A {!!} 146 distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL
151 ≈⟨⟩ 147 distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin
152 id1 A (fobj x ) 148 id1 A b
153 ∎ 149 ≈↑⟨ idL ⟩
154 identity _ | t1 = let open ≈-Reasoning (A) in {!!} 150 id1 A b o id1 A b
155 distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → 151 ∎
156 A [ fmap (A [ g o f ]) ≈ A [ fmap g o fmap f ] ] 152 distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin
157 distr1 {a} {b} {c} {f} {g} = {!!} 153 fmap (comp arrow-f id-t0)
158 -- distr1 {a} {b} {c} {f} {g} with (obj→ a) | (obj→ b ) | ( obj→ c ) | ( hom→ f ) | ( hom→ g ) 154 ≈⟨⟩
159 -- distr1 {a} {b} {c} {f} {g} | _ | _ | _ | _ | _ = ? 155 fmap arrow-f
160 156 ≈↑⟨ idR ⟩
161 157 fmap arrow-f o id1 A a
162 158 ∎
163 159 distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin
164 160 fmap (comp arrow-g id-t0)
161 ≈⟨⟩
162 fmap arrow-g
163 ≈↑⟨ idR ⟩
164 fmap arrow-g o id1 A a
165 ∎
166 distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin
167 fmap (comp id-t1 arrow-f)
168 ≈⟨⟩
169 fmap arrow-f
170 ≈↑⟨ idL ⟩
171 id1 A b o fmap arrow-f
172 ∎
173 distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin
174 fmap (comp id-t1 arrow-g)
175 ≈⟨⟩
176 fmap arrow-g
177 ≈↑⟨ idL ⟩
178 id1 A b o fmap arrow-g
179 ∎
165 180
166 --- Equalizer 181 --- Equalizer
167 --- f 182 --- f
168 --- e -----→ 183 --- e -----→
169 --- c -----→ a b 184 --- c -----→ a b
185 200
186 open Complete 201 open Complete
187 open Limit 202 open Limit
188 open NTrans 203 open NTrans
189 204
190 equlimit : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A I) -> 205 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) ->
191 Hom A ( limit-c comp ({!!} )) a 206 Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a
192 equlimit A I f g comp = {!!} 207 equlimit A f g comp = {!!}
193 208
194 lim-to-equ : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) 209 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
195 (comp : Complete A I) 210 (comp : Complete A (TwoCat {c₁} {c₂} ) )
196 → {a b : Obj A} (f g : Hom A a b ) 211 → {a b : Obj A} (f g : Hom A a b )
197 → IsEqualizer A (equlimit A I f g comp ) f g 212 → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] )
198 lim-to-equ {c₁} {c₂} {ℓ} A I comp {a} {b} f g = record { 213 → IsEqualizer A (equlimit A f g comp ) f g
199 fe=ge = {!!} 214 lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record {
215 fe=ge = fe=ge
200 ; k = λ {d} h fh=gh → k {d} h fh=gh 216 ; k = λ {d} h fh=gh → k {d} h fh=gh
201 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh 217 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
202 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' 218 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
203 } where 219 } where
204 open ≈-Reasoning A 220 I = TwoCat {c₁} {c₂}
205 Γ : Functor I A 221 Γ : Functor I A
206 Γ = {!!} 222 Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g
207 eqlim = isLimit comp Γ 223 eqlim = isLimit comp Γ
208 c = {!!} 224 c = limit-c comp Γ
209 e = {!!} 225 e = equlimit A f g comp
210 k : {d : Obj A} (h : Hom A d a) → {!!} -- A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c 226 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
211 k = {!!} -- {d} h fh=gh = {!!} 227 k {d} h fh=gh = {!!}
212 ek=h : (d : Obj A ) (h : Hom A d a ) → {!!} -- ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] 228 ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ]
213 ek=h = {!!} 229 ek=h = {!!}
214 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ] 230 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
215 uniq-nat = {!!} 231 uniq-nat = {!!}
216 uniquness : (d : Obj A ) (h : Hom A d a ) → ?　→ -- ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → 232 uniquness : (d : Obj A ) (h : Hom A d a ) → ?　→ -- ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
217 ( k' : Hom A d c ) 233 ( k' : Hom A d c )
218 → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] 234 → A [ A [ e o k' ] ≈ h ] → A [ k h {!!} ≈ k' ]
219 uniquness = {!!} 235 uniquness = {!!}