Members/kono/Proof/category: limit-to.agda annotate

annotate limit-to.agda @ 665:9904edf40547

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 23 Oct 2017 07:52:30 +0900
parents	e1d54c0f73a7
children	99065a1e56ea

rev	line source
415 dd086f5fb29f same conflict again ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 414 diff changeset	1 open import Category -- https://github.com/konn/category-agda
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2 open import Level
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	3
403 375edfefbf6a maybe CAT Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 402 diff changeset	4 module limit-to where
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	5
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	6 open import cat-utility
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	7 open import HomReasoning
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	8 open import Relation.Binary.Core
c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	10 open import discrete
427 531b739a1d7c add Nil Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 426 diff changeset	11
365 41ec06dd4b21 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 364 diff changeset	12
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	13 --- Equalizer from Limit ( 2->A IdnexFunctor Γ and IndexNat : K ->　Γ)
458 fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	14 ---
fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	15 ---
387 2f59c2db9d98 what is this ? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 386 diff changeset	16 --- f
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	17 --- e -----→
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	18 --- c -----→ a b A
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	19 --- ^ / -----→
387 2f59c2db9d98 what is this ? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 386 diff changeset	20 --- \|k h g
415 dd086f5fb29f same conflict again ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 414 diff changeset	21 --- \| /
426 1290d6876129 Functor MA → A Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 425 diff changeset	22 --- \| / ^
1290d6876129 Functor MA → A Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 425 diff changeset	23 --- \| / \|
1290d6876129 Functor MA → A Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 425 diff changeset	24 --- \|/ \| Γ
1290d6876129 Functor MA → A Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 425 diff changeset	25 --- d _ \|
432 688066ac172e add another method as a comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 431 diff changeset	26 --- \|\ \|
688066ac172e add another method as a comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 431 diff changeset	27 --- \ K af
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	28 --- \ -----→
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	29 --- \ t0 t1 I
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	30 --- -----→
426 1290d6876129 Functor MA → A Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 425 diff changeset	31 --- ag
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	32 ---
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	33 ---
387 2f59c2db9d98 what is this ? Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 386 diff changeset	34
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	35 open Complete
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	36 open Limit
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	37 open IsLimit
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	38 open NTrans
352 f589e71875ea bad approach Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 351 diff changeset	39
458 fd79b6d9f350 fix comment Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 457 diff changeset	40 -- Functor Γ : TwoCat -> A
424 4329525f5085 fix imit-to-edu for MaybeCat / TwoCat Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 423 diff changeset	41
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	42 IndexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	43 IndexFunctor {c₁} {c₂} {ℓ} A a b f g = record {
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	44 FObj = λ a → fobj a
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	45 ; FMap = λ {a} {b} f → fmap {a} {b} f
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	46 ; isFunctor = record {
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	47 identity = λ{x} → identity x
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	48 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	49 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	50 }
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	51 } where
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	52 T = TwoCat {c₁} {c₂}
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	53 fobj : Obj T → Obj A
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	54 fobj t1 = b
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	55 fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y)
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	56 fmap {t0} {t0} id-t0 = id1 A a
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	57 fmap {t1} {t1} id-t1 = id1 A b
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	58 fmap {t0} {t1} arrow-f = f
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	59 fmap {t0} {t1} arrow-g = g
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	60 ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ]
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	61 ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	62 identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ]
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	63 identity t0 = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	64 identity t1 = let open ≈-Reasoning A in refl-hom
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	65 distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	66 A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ]
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	67 distr1 {t0} {t0} {t0} {id-t0 } { id-t0 } = let open ≈-Reasoning A in sym-hom idL
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	68 distr1 {t1} {t1} {t1} { id-t1 } { id-t1 } = let open ≈-Reasoning A in begin
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	69 id b
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	70 ≈↑⟨ idL ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	71 id b o id b
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	72 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	73 distr1 {t0} {t0} {t1} { id-t0 } { arrow-f } = let open ≈-Reasoning A in begin
462 e618db534987 clean up fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	74 fmap (T [ arrow-f o id-t0 ] )
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	75 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	76 fmap arrow-f
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	77 ≈↑⟨ idR ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	78 fmap arrow-f o id a
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	79 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	80 distr1 {t0} {t0} {t1} { id-t0 } { arrow-g } = let open ≈-Reasoning A in begin
462 e618db534987 clean up fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	81 fmap (T [ arrow-g o id-t0 ] )
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	82 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	83 fmap arrow-g
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	84 ≈↑⟨ idR ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	85 fmap arrow-g o id a
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	86 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	87 distr1 {t0} {t1} {t1} { arrow-f } { id-t1 } = let open ≈-Reasoning A in begin
462 e618db534987 clean up fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	88 fmap (T [ id-t1 o arrow-f ] )
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	89 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	90 fmap arrow-f
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	91 ≈↑⟨ idL ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	92 id b o fmap arrow-f
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	93 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	94 distr1 {t0} {t1} {t1} { arrow-g } { id-t1 } = let open ≈-Reasoning A in begin
462 e618db534987 clean up fix Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 461 diff changeset	95 fmap (T [ id-t1 o arrow-g ] )
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	96 ≈⟨⟩
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	97 fmap arrow-g
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	98 ≈↑⟨ idL ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	99 id b o fmap arrow-g
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	100 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	101
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	102 --- Nat for Limit
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	103 --
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	104 -- Nat : K -> IndexFunctor
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	105 --
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	106
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	107 open Functor
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	108
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	109 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	110 → {a b : Obj A} (f g : Hom A a b )
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	111 (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] →
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	112 NTrans TwoCat A (K A TwoCat d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	113 IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	114 TMap = λ x → nmap x d h ;
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	115 isNTrans = record {
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	116 commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	117 }
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	118 } where
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	119 I = TwoCat {c₁} {c₂}
429 02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	120 Γ : Functor I A
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	121 Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	122 nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	123 nmap t0 d h = h
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	124 nmap t1 d h = A [ f o h ]
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	125 commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ]
427 531b739a1d7c add Nil Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 426 diff changeset	126 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	127 commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	128 f o h
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	129 ≈↑⟨ idR ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	130 (f o h ) o id d
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	131 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	132 commute1 {t0} {t1} {arrow-g} d h fh=gh = let open ≈-Reasoning A in begin
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	133 g o h
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	134 ≈↑⟨ fh=gh ⟩
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	135 f o h
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	136 ≈↑⟨ idR ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	137 (f o h ) o id d
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	138 ∎
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	139 commute1 {t0} {t0} {id-t0} d h fh=gh = let open ≈-Reasoning A in begin
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	140 id a o h
429 02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	141 ≈⟨ idL ⟩
02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	142 h
02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	143 ≈↑⟨ idR ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	144 h o id d
429 02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	145 ∎
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	146 commute1 {t1} {t1} {id-t1} d h fh=gh = let open ≈-Reasoning A in begin
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	147 id b o ( f o h )
429 02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	148 ≈⟨ idL ⟩
428 7f8b9f1f1bba ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 427 diff changeset	149 f o h
429 02eefa110eae nat commute in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 428 diff changeset	150 ≈↑⟨ idR ⟩
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	151 ( f o h ) o id d
428 7f8b9f1f1bba ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 427 diff changeset	152 ∎
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	153
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	154
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	155 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A TwoCat ) ->
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	156 Hom A ( limit-c comp (IndexFunctor A a b f g)) a
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	157 equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) discrete.t0
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	158
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	159 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	160 (comp : Complete A TwoCat )
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	161 → {a b : Obj A} (f g : Hom A a b )
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	162 → IsEqualizer A (equlimit A f g comp) f g
601 2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	163 lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g = record {
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	164 fe=ge = fe=ge0
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	165 ; k = λ {d} h fh=gh → k {d} h fh=gh
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	166 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	167 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	168 } where
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	169 I : Category c₁ c₂ c₂
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	170 I = TwoCat
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	171 Γ : Functor I A
461 8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	172 Γ = IndexFunctor A a b f g
8436a018f88a clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 460 diff changeset	173 e : Hom A (limit-c comp (IndexFunctor A a b f g)) a
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	174 e = equlimit A f g comp
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	175 c : Obj A
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	176 c = limit-c comp Γ
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	177 lim : Limit A I Γ
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	178 lim = climit comp Γ
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 462 diff changeset	179 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) Γ
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	180 inat = IndexNat A f g
601 2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	181 fe=ge0 : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ]
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	182 fe=ge0 = let open ≈-Reasoning A in begin
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	183 f o (equlimit A f g comp)
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	184 ≈⟨⟩
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	185 FMap Γ arrow-f o TMap (limit-u comp Γ) discrete.t0
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	186 ≈⟨ IsNTrans.commute ( isNTrans ( limit-u comp Γ )) {discrete.t0} {discrete.t1} {arrow-f} ⟩
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	187 TMap (limit-u comp Γ) discrete.t1 o FMap (K A (TwoCat {c₁} {c₂} )(limit-c comp Γ)) id-t0
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	188 ≈↑⟨ IsNTrans.commute ( isNTrans ( limit-u comp Γ )) {discrete.t0} {discrete.t1} {arrow-g} ⟩
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	189 FMap Γ arrow-g o TMap (limit-u comp Γ) discrete.t0
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	190 ≈⟨⟩
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	191 g o (equlimit A f g comp)
2e7b5a777984 prove fe=ge in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 508 diff changeset	192 ∎
350 c483374f542b try equalizer from limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	193 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	194 k {d} h fh=gh = limit (isLimit lim) d (inat d h fh=gh )
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	195 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 ]
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	196 ek=h d h fh=gh = let open ≈-Reasoning A in begin
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	197 e o k h fh=gh
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	198 ≈⟨⟩
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	199 TMap (limit-u comp Γ) discrete.t0 o k h fh=gh
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	200 ≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {discrete.t0} ⟩
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	201 TMap (inat d h fh=gh) discrete.t0
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	202 ≈⟨⟩
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	203 h
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	204 ∎
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	205 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c )
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	206 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] →
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 462 diff changeset	207 A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ]
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	208 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	209 TMap (limit-u comp Γ) discrete.t0 o k'
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	210 ≈⟨⟩
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	211 e o k'
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	212 ≈⟨ ek'=h ⟩
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	213 h
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	214 ≈⟨⟩
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	215 TMap (inat d h fh=gh) discrete.t0
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	216 ∎
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	217 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	218 TMap (limit-u comp Γ) t1 o k'
961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	219 ≈↑⟨ car (idR) ⟩
467 ba042c2d3ff5 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 466 diff changeset	220 ( TMap (limit-u comp Γ) t1 o id c ) o k'
460 961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	221 ≈⟨⟩
961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	222 ( TMap (limit-u comp Γ) t1 o FMap (K A I c) arrow-f ) o k'
961c236807f1 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 458 diff changeset	223 ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩
484 fcae3025d900 fix Limit pu a0 and t0 in record definition Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 474 diff changeset	224 ( FMap Γ arrow-f o TMap (limit-u comp Γ) discrete.t0 ) o k'
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	225 ≈⟨⟩
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	226 (f o e ) o k'
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	227 ≈↑⟨ assoc ⟩
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	228 f o ( e o k' )
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	229 ≈⟨ cdr ek'=h ⟩
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	230 f o h
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	231 ≈⟨⟩
466 44bd77c80555 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 462 diff changeset	232 TMap (inat d h fh=gh) t1
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	233 ∎
431 a15f52456c78 clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 430 diff changeset	234 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
372 b4855a3ebd34 add more lemma in limit-to Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 371 diff changeset	235 ( k' : Hom A d c )
457 0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	236 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
0ba86e29f492 limit-to and discrete clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 443 diff changeset	237 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	238 k h fh=gh
495 633df882db86 fryed1 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 487 diff changeset	239 ≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
430 46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	240 k'
46c057cb3d82 limit-to done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 429 diff changeset	241 ∎
368 b18585089d2e add more parameter to nat in lim-to-equ Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 367 diff changeset	242
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	243
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	244 --- Product from Limit ( given Discrete->A functor Γ and pnat : K ->　Γ)
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	245
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	246 open DiscreteHom
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	247
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	248 plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) (comp : Complete A ( DiscreteCat S ) )
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	249 → ( Γ : Functor (DiscreteCat S ) A ) → Obj A
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	250 plimit A S comp Γ = limit-c comp Γ
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	251
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	252 discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ]
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	253 discrete-identity f = refl
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	254
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	255 pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁)
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	256 → (Γ : Functor (DiscreteCat S ) A )
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	257 → {q : Obj A } ( qi : (i : Obj ( DiscreteCat S)) → Hom A q (FObj Γ i) )
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	258 → NTrans (DiscreteCat S )A (K A (DiscreteCat S) q) Γ
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	259 pnat A S Γ {q} qi = record {
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	260 TMap = qi ;
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	261 isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	262 } where
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	263 commute : {a b : Obj (DiscreteCat S) } {f : Hom ( DiscreteCat S) a b} →
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	264 A [ A [ FMap Γ f o qi a ] ≈ A [ qi b o FMap (K A (DiscreteCat S )q) f ] ]
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	265 commute {a} {b} {f} with discrete f
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	266 commute {a} {.a} {f} \| refl = let open ≈-Reasoning A in begin
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	267 FMap Γ f o qi a
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	268 ≈⟨ car ( fcong Γ (discrete-identity f )) ⟩
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	269 FMap Γ (id1 (DiscreteCat S) a ) o qi a
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	270 ≈⟨ car ( IsFunctor.identity (isFunctor Γ) ) ⟩
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	271 id1 A (FObj Γ a) o qi a
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	272 ≈⟨ idL ⟩
f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	273 qi a
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	274 ≈↑⟨ idR ⟩
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	275 qi a o id q
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	276 ≈⟨⟩
472 f3d6d0275a0a discrete equality as a dom equality Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 469 diff changeset	277 qi a o FMap (K A (DiscreteCat S) q) f
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	278 ∎
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	279
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	280 lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ )
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	281 (comp : Complete A ( DiscreteCat S ) )
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	282 → ( Γ : Functor (DiscreteCat S ) A )
508 3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	283 → IProduct A (Obj ( DiscreteCat S ) ) -- (plimit A S comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u comp Γ) i )
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	284 lim-to-product A S comp Γ = record {
508 3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	285 ai = λ i → FObj Γ i
3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	286 ; iprod = plimit A S comp Γ
3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	287 ; pi = λ i → TMap (limit-u comp Γ) i
3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	288 ; isIProduct = record {
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	289 iproduct = λ {q} qi → iproduct {q} qi ;
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	290 pif=q = λ {q } qi { i } → pif=q {q} qi {i} ;
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	291 ip-uniqueness = λ {q } { h } → ip-uniqueness {q} {h} ;
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	292 ip-cong = λ {q } { qi } { qi' } qi=qi' → ip-cong {q} {qi} {qi'} qi=qi'
508 3ce21b2a671a IProduct is written in Sets Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 495 diff changeset	293 }
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	294 } where
469 65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	295 D = DiscreteCat S
65ab0da524b8 discrete f ≡ refl should be passed, but it doesn't Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 468 diff changeset	296 I = Obj ( DiscreteCat S )
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	297 lim = climit comp Γ
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	298 ai = λ i → FObj Γ i
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	299 p = limit-c comp Γ
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	300 pi = λ i → TMap (limit-u comp Γ) i
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	301 iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	302 iproduct {q} qi = limit (isLimit lim) q (pnat A S Γ qi )
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	303 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ]
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	304 pif=q {q} qi {i} = t0f=t (isLimit lim) {q} {pnat A S Γ qi } {i}
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	305 ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ]
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	306 ipu {i} q h = let open ≈-Reasoning A in refl-hom
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	307 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
495 633df882db86 fryed1 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 487 diff changeset	308 ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} (ipu q h)
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	309 ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	310 → (i : I ) → A [ qi i ≈ qi' i ] →
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	311 A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	312 ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	313 TMap (limit-u comp Γ) i o iproduct qi'
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	314 ≈⟨⟩
487 c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	315 TMap (limit-u comp Γ) i o limit (isLimit lim) q (pnat A S Γ qi' )
c257347a27f3 found limit in freyd Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 484 diff changeset	316 ≈⟨ t0f=t (isLimit lim) {q} {pnat A S Γ qi'} {i} ⟩
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	317 TMap (pnat A S Γ qi') i
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	318 ≈⟨⟩
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	319 qi' i
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	320 ≈↑⟨ qi=qi' ⟩
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	321 qi i
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	322 ≈⟨⟩
474 2d32ded94aaf clean up Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 472 diff changeset	323 TMap (pnat A S Γ qi) i
468 c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	324 ∎
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	325 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
c375d8f93a2c discrete category and product from a limit Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 467 diff changeset	326 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
495 633df882db86 fryed1 done Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 487 diff changeset	327 ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))

Mercurial > hg > Members > kono > Proof > category

annotate limit-to.agda @ 665:9904edf40547