Mercurial > hg > Members > kono > Proof > category
diff pullback.agda @ 303:7f40d6a51c72
Limit form equalizer and product done.
Use equalizer to provle naturality of limit-ε
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 Nov 2013 14:46:07 +0900 |
| parents | c5b2656dbec6 |
| children | 702adc45704f |
line wrap: on
line diff
--- a/pullback.agda Wed Oct 30 19:35:14 2013 +0900 +++ b/pullback.agda Mon Nov 04 14:46:07 2013 +0900 @@ -314,6 +314,18 @@ f ∎ + +lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : Product A a b ab π1 π2 ) → + A [ _×_ prod π1 π2 ≈ id1 A ab ] +lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin + _×_ prod π1 π2 + ≈↑⟨ ×-cong prod idR idR ⟩ + _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ]) + ≈⟨ Product.uniqueness prod ⟩ + id1 A ab + ∎ + + ----- -- -- product on arbitrary index @@ -327,17 +339,14 @@ field product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ] - -- special case of product ( qi = pi ) ( should b proved from pif=q ) - -- we cannot prove this because qi/pi cannot be interleaved , should be the way to prove - pif=q1 : { i : I } → { qi : Hom A p (ai i) } → A [ pi i ≈ qi ] ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] -- another form of uniquness - ip-uniquness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) + ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) → A [ product' ≈ product qi ] - ip-uniquness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin + ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin product' ≈↑⟨ ip-uniqueness ⟩ product (λ i₁ → A [ pi i₁ o product' ]) @@ -348,20 +357,6 @@ ∎ ) ⟩ product qi ∎ - pif=q1' : { i : I } → { qi : (j : I ) → Hom A p (ai j) } → A [ pi i ≈ qi i ] - pif=q1' {i} {qi} = let open ≈-Reasoning (A) in begin - pi i - ≈↑⟨ idR ⟩ - pi i o id1 A p - ≈⟨ cdr ( ip-uniquness1 {p} qi (id1 A p) ( begin - pi ? o id1 A p - ≈⟨ {!!} ⟩ - qi ? - ∎ )) ⟩ - pi i o product qi - ≈⟨ pif=q {p} qi {i} ⟩ - qi i - ∎ open IProduct open Equalizer @@ -375,7 +370,7 @@ -- | pi lim = K i -----------→ K j = lim -- | | | -- p | | --- ^ ε i | | ε j +-- ^ proj i o e = ε i | | ε j = proj j o e -- | | | -- | e = equalizer (id p) (id p) | | -- | v v @@ -383,35 +378,15 @@ -- k ( product pi ) Γ f -- Γ f o ε i = ε j -- --- - --- pi-ε -- : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) --- → IProduct {c₁'} A (Obj I) p ai pi ) --- ( lim p : Obj A ) ( e : Hom A lim p ) --- ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → --- { i : Obj I } → { q : ( i : Obj I ) → Hom A p (FObj Γ i) } → A [ proj i ≈ q i ] --- pi-ε prod lim p e proj {i} {q} = let open ≈-Reasoning (A) in begin --- proj i --- ≈↑⟨ idR ⟩ --- proj i o id1 A p --- ≈⟨ cdr {!!} ⟩ --- proj i o product (prod p (FObj Γ) proj) q --- ≈⟨ pif=q (prod p (FObj Γ) proj) q ⟩ --- q i --- ∎ - limit-ε : - ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) - → IProduct {c₁'} A (Obj I) p ai pi ) + ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g ) ( lim p : Obj A ) ( e : Hom A lim p ) ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → NTrans I A (K A I lim) Γ -limit-ε prod lim p e proj = record { +limit-ε eqa lim p e proj = record { TMap = tmap ; - isNTrans = record { - commute = commute1 - } + isNTrans = record { commute = commute1 } } where tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i) tmap i = A [ proj i o e ] @@ -423,7 +398,7 @@ FMap Γ f o ( proj i o e ) ≈⟨ assoc ⟩ ( FMap Γ f o proj i ) o e - ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ) proj ) {j} ) ⟩ + ≈⟨ fe=ge ( eqa e (FMap Γ f o proj i) ( proj j )) ⟩ proj j o e ≈↑⟨ idR ⟩ (proj j o e ) o id1 A lim @@ -438,7 +413,7 @@ ( lim p : Obj A ) -- limit to be made ( e : Hom A lim p ) -- existing of equalizer ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) - → Limit A I Γ lim ( limit-ε prod lim p e proj ) + → Limit A I Γ lim ( limit-ε eqa lim p e proj ) limit-from prod eqa lim p e proj = record { limit = λ a t → limit1 a t ; t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; @@ -447,9 +422,9 @@ limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → - A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ] + A [ A [ TMap (limit-ε eqa lim p e proj ) i o limit1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin - TMap (limit-ε prod lim p e proj ) i o limit1 a t + TMap (limit-ε eqa lim p e proj ) i o limit1 a t ≈⟨⟩ ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ≈↑⟨ assoc ⟩ @@ -460,7 +435,7 @@ TMap t i ∎ limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} - → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) → + → ({i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) i o f ] ≈ TMap t i ]) → A [ limit1 a t ≈ f ] limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin limit1 a t