Mercurial > hg > Members > kono > Proof > category

comparison freyd1.agda @ 691:917e51be9bbf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
change argument of Limit and K
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 09:56:40 +0900
parents 372205f40ab0
children
comparison
equal deleted inserted replaced
690:3d41a8edbf63 691:917e51be9bbf
49 ∎ 49 ∎
50 50
51 --- Get a nat on A from a nat on CommaCategory 51 --- Get a nat on A from a nat on CommaCategory
52 -- 52 --
53 NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) 53 NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
54 (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) → NTrans I A ( K A I (obj c) ) (FIA Γ) 54 (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K I CommaCategory c ) Γ ) → NTrans I A ( K I A (obj c) ) (FIA Γ)
55 NIA {I} Γ c ta = record { 55 NIA {I} Γ c ta = record {
56 TMap = λ x → arrow (TMap ta x ) 56 TMap = λ x → arrow (TMap ta x )
57 ; isNTrans = record { commute = comm1 } 57 ; isNTrans = record { commute = comm1 }
58 } where 58 } where
59 comm1 : {a b : Obj I} {f : Hom I a b} → 59 comm1 : {a b : Obj I} {f : Hom I a b} →
60 A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ] 60 A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K I A (obj c)) f ] ]
61 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) 61 comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
62 62
63 63
64 open LimitPreserve 64 open LimitPreserve
65 65
66 -- Limit on A from Γ : I → CommaCategory 66 -- Limit on A from Γ : I → CommaCategory
67 -- 67 --
68 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 68 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
69 → ( Γ : Functor I CommaCategory ) 69 → ( Γ : Functor I CommaCategory )
70 → ( glimit : LimitPreserve A I C G ) 70 → ( glimit : LimitPreserve I A C G )
71 → Limit C I (G ○ (FIA Γ)) 71 → Limit I C (G ○ (FIA Γ))
72 LimitC {I} comp Γ glimit = plimit glimit (climit comp (FIA Γ)) 72 LimitC {I} comp Γ glimit = plimit glimit (climit comp (FIA Γ))
73 73
74 tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) 74 tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
75 → NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) 75 → NTrans I C (K I C (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ))
76 tu {I} comp Γ = record { 76 tu {I} comp Γ = record {
77 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ] 77 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ]
78 ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } 78 ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
79 } where 79 } where
80 commute : {a b : Obj I} {f : Hom I a b} → 80 commute : {a b : Obj I} {f : Hom I a b} →
81 C [ C [ FMap (G ○ (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a) ] ] 81 C [ C [ FMap (G ○ (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a) ] ]
82 ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] 82 ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ] ]
83 commute {a} {b} {f} = let open ≈-Reasoning (C) in begin 83 commute {a} {b} {f} = let open ≈-Reasoning (C) in begin
84 FMap (G ○ (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a )) 84 FMap (G ○ (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a ))
85 ≈⟨⟩ 85 ≈⟨⟩
86 FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a )) 86 FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ))
87 ≈⟨ assoc ⟩ 87 ≈⟨ assoc ⟩
93 ≈↑⟨ cdr (distr F) ⟩ 93 ≈↑⟨ cdr (distr F) ⟩
94 hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f) o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) 94 hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f) o TMap (t0 ( climit comp (FIA Γ))) a ] ) )
95 ≈⟨⟩ 95 ≈⟨⟩
96 hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ) f o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) 96 hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ) f o TMap (t0 ( climit comp (FIA Γ))) a ] ) )
97 ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ))) ))) ⟩ 97 ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ))) ))) ⟩
98 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] )) 98 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K I A (a0 (climit comp (FIA Γ)))) f ] ))
99 ≈⟨⟩ 99 ≈⟨⟩
100 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] )) 100 hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] ))
101 ≈⟨ cdr ( distr F ) ⟩ 101 ≈⟨ cdr ( distr F ) ⟩
102 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ)))) 102 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ))))
103 ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩ 103 ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩
104 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ)))) 104 hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ))))
105 ≈⟨ assoc ⟩ 105 ≈⟨ assoc ⟩
106 ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f 106 ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f
107 ∎ 107 ∎
108 limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) 108 limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory )
109 → ( glimit : LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) 109 → ( glimit : LimitPreserve I A C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
110 limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) 110 limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ )
111 111
112 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) 112 commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory )
113 → ( glimit : LimitPreserve A I C G ) 113 → ( glimit : LimitPreserve I A C G )
114 → Obj CommaCategory 114 → Obj CommaCategory
115 commaLimit {I} comp Γ glimit = record { 115 commaLimit {I} comp Γ glimit = record {
116 obj = limit-c comp (FIA Γ) 116 obj = limit-c comp (FIA Γ)
117 ; hom = limitHom comp Γ glimit 117 ; hom = limitHom comp Γ glimit
118 } 118 }
119 119
120 120
121 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) 121 commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
122 → ( glimit : LimitPreserve A I C G ) 122 → ( glimit : LimitPreserve I A C G )
123 → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit)) Γ 123 → NTrans I CommaCategory (K I CommaCategory (commaLimit {I} comp Γ glimit)) Γ
124 commaNat {I} comp Γ glimit = record { 124 commaNat {I} comp Γ glimit = record {
125 TMap = λ x → record { 125 TMap = λ x → record {
126 arrow = TMap ( limit-u comp (FIA Γ ) ) x 126 arrow = TMap ( limit-u comp (FIA Γ ) ) x
127 ; comm = comm1 x 127 ; comm = comm1 x
128 } 128 }
129 ; isNTrans = record { commute = comm2 } 129 ; isNTrans = record { commute = comm2 }
130 } where 130 } where
131 comm1 : (x : Obj I ) → 131 comm1 : (x : Obj I ) →
132 C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] 132 C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x) ]
133 ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] 133 ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ]
134 comm1 x = let open ≈-Reasoning (C) in begin 134 comm1 x = let open ≈-Reasoning (C) in begin
135 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) 135 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x)
136 ≈⟨⟩ 136 ≈⟨⟩
137 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) 137 FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit)
138 ≈⟨⟩ 138 ≈⟨⟩
139 FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) 139 FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ )
140 ≈⟨⟩ 140 ≈⟨⟩
144 ≈⟨⟩ 144 ≈⟨⟩
145 hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) 145 hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x)
146 ∎ 146 ∎
147 comm2 : {a b : Obj I} {f : Hom I a b} → 147 comm2 : {a b : Obj I} {f : Hom I a b} →
148 CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ] 148 CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ]
149 ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ] 149 ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K I CommaCategory (commaLimit comp Γ glimit)) f ] ]
150 comm2 {a} {b} {f} = let open ≈-Reasoning (A) in begin 150 comm2 {a} {b} {f} = let open ≈-Reasoning (A) in begin
151 FMap (FIA Γ) f o TMap (limit-u comp (FIA Γ)) a 151 FMap (FIA Γ) f o TMap (limit-u comp (FIA Γ)) a
152 ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ))) ⟩ 152 ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ))) ⟩
153 TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f 153 TMap (limit-u comp (FIA Γ)) b o FMap (K I A (limit-c comp (FIA Γ))) f
154 ∎ 154 ∎
155 155
156 gnat : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) 156 gnat : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory )
157 → (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → 157 → (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) →
158 NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) 158 NTrans I C (K I C (FObj F (obj a))) (G ○ FIA Γ)
159 gnat {I} Γ a t = record { 159 gnat {I} Γ a t = record {
160 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ] 160 TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ]
161 ; isNTrans = record { commute = λ {x y f} → comm1 x y f } 161 ; isNTrans = record { commute = λ {x y f} → comm1 x y f }
162 } where 162 } where
163 comm1 : (x y : Obj I) (f : Hom I x y ) → 163 comm1 : (x y : Obj I) (f : Hom I x y ) →
164 C [ C [ FMap (G ○ FIA Γ) f o C [ hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x) ] ] 164 C [ C [ FMap (G ○ FIA Γ) f o C [ hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x) ] ]
165 ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K C I (FObj F (obj a))) f ] ] 165 ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K I C (FObj F (obj a))) f ] ]
166 comm1 x y f = let open ≈-Reasoning (C) in begin 166 comm1 x y f = let open ≈-Reasoning (C) in begin
167 FMap (G ○ FIA Γ) f o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x )) 167 FMap (G ○ FIA Γ) f o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x ))
168 ≈⟨⟩ 168 ≈⟨⟩
169 FMap G (FMap (FIA Γ) f) o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x )) 169 FMap G (FMap (FIA Γ) f) o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x ))
170 ≈⟨ assoc ⟩ 170 ≈⟨ assoc ⟩
178 ≈⟨ cdr ( fcong F ( IsNTrans.commute ( isNTrans ( NIA Γ a t )))) ⟩ 178 ≈⟨ cdr ( fcong F ( IsNTrans.commute ( isNTrans ( NIA Γ a t )))) ⟩
179 hom (FObj Γ y) o ( FMap F ( A [ TMap (NIA Γ a t) y o id1 A (obj a) ]) ) 179 hom (FObj Γ y) o ( FMap F ( A [ TMap (NIA Γ a t) y o id1 A (obj a) ]) )
180 ≈⟨ cdr ( fcong F ( IsCategory.identityR (Category.isCategory A))) ⟩ 180 ≈⟨ cdr ( fcong F ( IsCategory.identityR (Category.isCategory A))) ⟩
181 hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) 181 hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y)
182 ≈↑⟨ idR ⟩ 182 ≈↑⟨ idR ⟩
183 ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K C I (FObj F (obj a))) f 183 ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K I C (FObj F (obj a))) f
184 ∎ 184 ∎
185 185
186 186
187 comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) 187 comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
188 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) 188 → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit)
189 comma-a0 {I} comp Γ glimit a t = record { 189 comma-a0 {I} comp Γ glimit a t = record {
190 arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) 190 arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t )
191 ; comm = comm1 191 ; comm = comm1
192 } where 192 } where
193 comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ] 193 comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ]
241 ≈⟨⟩ 241 ≈⟨⟩
242 hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) 242 hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
243 ∎ 243 ∎
244 244
245 comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) 245 comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
246 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) (i : Obj I ) 246 → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) (i : Obj I )
247 → CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ] 247 → CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ]
248 comma-t0f=t {I} comp Γ glimit a t i = let open ≈-Reasoning (A) in begin 248 comma-t0f=t {I} comp Γ glimit a t i = let open ≈-Reasoning (A) in begin
249 TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) 249 TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t )
250 ≈⟨ t0f=t (isLimit ( climit comp (FIA Γ) ) ) ⟩ 250 ≈⟨ t0f=t (isLimit ( climit comp (FIA Γ) ) ) ⟩
251 TMap (NIA {I} Γ a t ) i 251 TMap (NIA {I} Γ a t ) i
252 ∎ 252 ∎
253 253
254 comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) 254 comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory )
255 → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) 255 → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ )
256 → ( f : Hom CommaCategory a (commaLimit comp Γ glimit)) 256 → ( f : Hom CommaCategory a (commaLimit comp Γ glimit))
257 → ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat { I} comp Γ glimit ) i o f ] ≈ TMap t i ] ) 257 → ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat { I} comp Γ glimit ) i o f ] ≈ TMap t i ] )
258 → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ] 258 → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ]
259 comma-uniqueness {I} comp Γ glimit a t f t=f = let open ≈-Reasoning (A) in begin 259 comma-uniqueness {I} comp Γ glimit a t f t=f = let open ≈-Reasoning (A) in begin
260 limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) 260 limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t )
261 ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) t=f ⟩ 261 ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) t=f ⟩
262 arrow f 262 arrow f
263 ∎ 263 ∎
264 264
265 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 265 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I )
266 → ( glimit : LimitPreserve A I C G ) 266 → ( glimit : LimitPreserve I A C G )
267 → ( Γ : Functor I CommaCategory ) 267 → ( Γ : Functor I CommaCategory )
268 → Limit CommaCategory I Γ 268 → Limit I CommaCategory Γ
269 hasLimit {I} comp glimit Γ = record { 269 hasLimit {I} comp glimit Γ = record {
270 a0 = commaLimit {I} comp Γ glimit ; 270 a0 = commaLimit {I} comp Γ glimit ;
271 t0 = commaNat { I} comp Γ glimit ; 271 t0 = commaNat { I} comp Γ glimit ;
272 isLimit = record { 272 isLimit = record {
273 limit = λ a t → comma-a0 comp Γ glimit a t ; 273 limit = λ a t → comma-a0 comp Γ glimit a t ;