Mercurial > hg > Members > kono > Proof > category

comparison limit-to.agda @ 484:fcae3025d900

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Limit pu a0 and t0 in record definition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Mar 2017 16:38:08 +0900
parents 2d32ded94aaf
children c257347a27f3
comparison
equal deleted inserted replaced
483:265f13adf93b 484:fcae3025d900
152 ∎ 152 ∎
153 153
154 154
155 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A TwoCat ) -> 155 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A TwoCat ) ->
156 Hom A ( limit-c comp (IndexFunctor A a b f g)) a 156 Hom A ( limit-c comp (IndexFunctor A a b f g)) a
157 equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) t0 157 equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) discrete.t0
158 158
159 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 159 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
160 (comp : Complete A TwoCat ) 160 (comp : Complete A TwoCat )
161 → {a b : Obj A} (f g : Hom A a b ) 161 → {a b : Obj A} (f g : Hom A a b )
162 → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] ) 162 → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] )
173 Γ = IndexFunctor A a b f g 173 Γ = IndexFunctor A a b f g
174 e : Hom A (limit-c comp (IndexFunctor A a b f g)) a 174 e : Hom A (limit-c comp (IndexFunctor A a b f g)) a
175 e = equlimit A f g comp 175 e = equlimit A f g comp
176 c : Obj A 176 c : Obj A
177 c = limit-c comp Γ 177 c = limit-c comp Γ
178 lim : Limit A I Γ c ( limit-u comp Γ ) 178 lim : Limit A I Γ
179 lim = isLimit comp Γ 179 lim = isLimit comp Γ
180 inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ 180 inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
181 inat = IndexNat A f g 181 inat = IndexNat A f g
182 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c 182 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
183 k {d} h fh=gh = limit lim d (inat d h fh=gh ) 183 k {d} h fh=gh = limit lim d (inat d h fh=gh )
184 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 ] 184 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 ]
185 ek=h d h fh=gh = let open ≈-Reasoning A in begin 185 ek=h d h fh=gh = let open ≈-Reasoning A in begin
186 e o k h fh=gh 186 e o k h fh=gh
187 ≈⟨⟩ 187 ≈⟨⟩
188 TMap (limit-u comp Γ) t0 o k h fh=gh 188 TMap (limit-u comp Γ) discrete.t0 o k h fh=gh
189 ≈⟨ t0f=t lim {d} {inat d h fh=gh } {t0} ⟩ 189 ≈⟨ t0f=t lim {d} {inat d h fh=gh } {discrete.t0} ⟩
190 TMap (inat d h fh=gh) t0 190 TMap (inat d h fh=gh) discrete.t0
191 ≈⟨⟩ 191 ≈⟨⟩
192 h 192 h
193 ∎ 193 ∎
194 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) 194 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c )
195 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → 195 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] →
196 A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ] 196 A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ]
197 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin 197 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
198 TMap (limit-u comp Γ) t0 o k' 198 TMap (limit-u comp Γ) discrete.t0 o k'
199 ≈⟨⟩ 199 ≈⟨⟩
200 e o k' 200 e o k'
201 ≈⟨ ek'=h ⟩ 201 ≈⟨ ek'=h ⟩
202 h 202 h
203 ≈⟨⟩ 203 ≈⟨⟩
204 TMap (inat d h fh=gh) t0 204 TMap (inat d h fh=gh) discrete.t0
205 ∎ 205 ∎
206 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin 206 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
207 TMap (limit-u comp Γ) t1 o k' 207 TMap (limit-u comp Γ) t1 o k'
208 ≈↑⟨ car (idR) ⟩ 208 ≈↑⟨ car (idR) ⟩
209 ( TMap (limit-u comp Γ) t1 o id c ) o k' 209 ( TMap (limit-u comp Γ) t1 o id c ) o k'
210 ≈⟨⟩ 210 ≈⟨⟩
211 ( TMap (limit-u comp Γ) t1 o FMap (K A I c) arrow-f ) o k' 211 ( TMap (limit-u comp Γ) t1 o FMap (K A I c) arrow-f ) o k'
212 ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩ 212 ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩
213 ( FMap Γ arrow-f o TMap (limit-u comp Γ) t0 ) o k' 213 ( FMap Γ arrow-f o TMap (limit-u comp Γ) discrete.t0 ) o k'
214 ≈⟨⟩ 214 ≈⟨⟩
215 (f o e ) o k' 215 (f o e ) o k'
216 ≈↑⟨ assoc ⟩ 216 ≈↑⟨ assoc ⟩
217 f o ( e o k' ) 217 f o ( e o k' )
218 ≈⟨ cdr ek'=h ⟩ 218 ≈⟨ cdr ek'=h ⟩