Mercurial > hg > Members > kono > Proof > category
changeset 682:50a01df1169a
clean up of pullback
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Nov 2017 23:48:46 +0900 |
| parents | bd8f7346f252 |
| children | 88e8a1290dc4 |
| files | pullback.agda |
| diffstat | 1 files changed, 112 insertions(+), 125 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Tue Nov 07 17:12:08 2017 +0900 +++ b/pullback.agda Tue Nov 07 23:48:46 2017 +0900 @@ -15,10 +15,10 @@ -- Pullback from equalizer and product -- f -- a ------→ c --- ^ ^ --- π1 | |g --- | | --- ab ------→ b +-- ^ ^ +-- π1 | |g +-- | | +-- axb -----→ b -- ^ π2 -- | -- | e = equalizer (f π1) (g π1) @@ -38,7 +38,7 @@ ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) ( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g pullback-from {a} {b} {c} f g eqa prod0 = record { - ab = ab ; + ab = d ; π1 = A [ π1 o e ] ; π2 = A [ π2 o e ] ; isPullback = record { @@ -49,22 +49,28 @@ uniqueness = uniqueness1 } } where + ab : Obj A + ab = Product.product (prod0 a b) + π1 : Hom A ab a π1 = Product.π1 (prod0 a b ) + π2 : Hom A ab b π2 = Product.π2 (prod0 a b ) + d : Obj A + d = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ])) + e : Hom A d ab e = equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) - ab = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ])) prod = Product.isProduct (prod0 a b) - commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] - ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] + commute1 : A [ A [ f o A [ π1 o e ] ] + ≈ A [ g o A [ π2 o e ] ] ] commute1 = let open ≈-Reasoning (A) in begin - f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) + f o ( π1 o e ) ≈⟨ assoc ⟩ - ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) + ( f o π1 ) o e ≈⟨ fe=ge (isEqualizer (eqa (A [ f o π1 ]) (A [ g o π2 ]))) ⟩ - ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) + ( g o π2 ) o e ≈↑⟨ assoc ⟩ - g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) + g o ( π2 o e ) ∎ lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] @@ -82,7 +88,7 @@ ≈⟨ assoc ⟩ ( g o π2 ) o (prod × π1') π2' ∎ - p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' ab + p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d p1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in k (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ))) (_×_ prod π1' π2' ) ( lemma1 eq ) π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → @@ -113,7 +119,7 @@ ≈⟨ π2fxg=g prod ⟩ π2' ∎ - uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ ab) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} + uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → @@ -316,18 +322,24 @@ -- limit from equalizer and product -- -- --- ai --- ^ K f = id lim --- | pi lim = K i -----------→ K j = lim --- | | | --- p | | --- ^ proj i o e = ε i | | ε j = proj j o e --- | | | +-- Γ j = Γ k +-- ↑ ^ ↑ +-- | | | +-- | |mu u |mu u +-- | | | +-- | product of Hom i +-- | ↑ ↑ K u = id lim +-- | | | +-- | f|id g|λ u → Γ u d = K j -----------→ K k = d +-- proj u | | | | u | +-- | | | proj j o e = ε j | | ε k = proj k o e +-- product of Obj i -+ mu u o g o e | | mu u o f o e +-- ^ | | -- | e = equalizer f g | | --- | v v --- lim <------------------ d' a i = Γ i -----------→ Γ j = a j --- k ( product pi ) Γ f --- Γ f o ε i = ε j +-- | ↓ ↓ +-- lim ←---------------- d' a j = Γ j -----------→ Γ k = a j +-- k ( product pi ) Γ u +-- Γ u o ε j = ε k -- -- homprod should be written by IProduct @@ -341,134 +353,109 @@ Homprod : {j k : Obj I} (u : Hom I j k) → homprod {c₁} Homprod {j} {k} u = record {hom-j = j ; hom-k = k ; hom = u} -Fcod : homprod {c₁} → Obj A -Fcod = λ u → FObj Γ ( hom-k u ) - -equ-ε : - ( prod : {c : Level} { I : Set c } → ( ai : I → Obj A ) → IProduct A I ai ) - ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) - → Equalizer A - (iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] )) - (iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u ))) -equ-ε prod eqa = eqa - (iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] )) - (iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u ))) - -limit-ε : - ( prod : {c : Level} { I : Set c } → ( ai : I → Obj A ) → IProduct A I ai ) - ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) - → NTrans I A (K A I (equalizer-c (equ-ε prod eqa )) ) Γ -limit-ε prod eqa = record { - TMap = λ i → tmap i ; - isNTrans = record { commute = commute1 } - } where - p0 : Obj A - p0 = iprod (prod (FObj Γ)) - d : Obj A - d = equalizer-c (equ-ε prod eqa ) - e : Hom A d p0 - e = equalizer (equ-ε prod eqa ) - proj : (i : Obj I) → Hom A p0 (FObj Γ i) - proj = pi ( prod (FObj Γ) ) - f : Hom A p0 (iprod (prod Fcod)) - f = (iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u ))) - g : Hom A p0 (iprod (prod Fcod)) - g = (iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] )) - tmap : (i : Obj I) → Hom A (FObj (K A I d) i) (FObj Γ i) - tmap i = A [ proj i o e ] - commute1 : {j k : Obj I} {u : Hom I j k} → - A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K A I d) u ] ] - commute1 {j} {k} {u} = let open ≈-Reasoning (A) in begin - FMap Γ u o tmap j - ≈⟨⟩ - FMap Γ u o ( proj j o e ) - ≈⟨ assoc ⟩ - ( FMap Γ u o pi (prod (FObj Γ)) j ) o e - ≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩ - ( pi (prod Fcod ) (Homprod u) o g ) o e - ≈↑⟨ assoc ⟩ - pi (prod Fcod ) (Homprod u) o (g o e ) - ≈⟨ cdr ( fe=ge (isEqualizer (equ-ε prod eqa ))) ⟩ - pi (prod Fcod ) (Homprod u) o (f o e ) - ≈⟨ assoc ⟩ - ( pi (prod Fcod ) (Homprod u) o f ) o e - ≈⟨ car ( pif=q (isIProduct (prod Fcod ))) ⟩ - pi (prod (FObj Γ)) k o e - ≈⟨⟩ - proj k o e - ≈↑⟨ idR ⟩ - (proj k o e ) o id1 A d - ≈⟨⟩ - tmap k o FMap (K A I d) u - ∎ - limit-from : ( prod : {c : Level} { I : Set c } → ( ai : I → Obj A ) → IProduct A I ai ) ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) → Limit A I Γ limit-from prod eqa = record { - a0 = lim ; - t0 = limit-ε prod eqa ; + a0 = d ; + t0 = limit-ε ; isLimit = record { limit = λ a t → limit1 a t ; t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f } } where - lim : Obj A - lim = equalizer-c ( equ-ε prod eqa ) p0 : Obj A p0 = iprod (prod (FObj Γ)) - e : Hom A lim p0 - e = let open ≈-Reasoning (A) in equalizer ( equ-ε prod eqa ) - equ = isEqualizer ( equ-ε prod eqa ) - proj = pi ( prod (FObj Γ) ) - prodΓ = isIProduct ( prod (FObj Γ) ) + Fcod : homprod {c₁} → Obj A + Fcod = λ u → FObj Γ ( hom-k u ) f : Hom A p0 (iprod (prod Fcod)) f = iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u )) g : Hom A p0 (iprod (prod Fcod)) g = iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] ) - comm3 : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → (u : homprod {c₁} ) - → A [ A [ pi (prod Fcod) u o A [ g o iproduct prodΓ (TMap t) ] ] ≈ - A [ pi (prod Fcod) u o A [ f o iproduct prodΓ (TMap t) ] ] ] - comm3 a t u = let open ≈-Reasoning (A) in begin - pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) ) - ≈⟨ assoc ⟩ - ( pi (prod Fcod) u o g ) o iproduct prodΓ (TMap t) - ≈⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ - (FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ) o iproduct prodΓ (TMap t) - ≈↑⟨ assoc ⟩ - FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u) o iproduct prodΓ (TMap t) ) - ≈⟨ cdr ( pif=q prodΓ ) ⟩ - FMap Γ (hom u) o TMap t (hom-j u) - ≈⟨ IsNTrans.commute (isNTrans t) ⟩ - TMap t (hom-k u) o id1 A a - ≈⟨ idR ⟩ - TMap t (hom-k u) - ≈↑⟨ pif=q prodΓ ⟩ - pi (prod (FObj Γ)) (hom-k u) o iproduct prodΓ (TMap t) - ≈↑⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ - (pi (prod Fcod) u o f ) o iproduct prodΓ (TMap t) - ≈↑⟨ assoc ⟩ - pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t) ) - ∎ + equ-ε : Equalizer A g f + equ-ε = eqa g f + d : Obj A + d = equalizer-c equ-ε + e : Hom A d p0 + e = equalizer equ-ε + equ = isEqualizer equ-ε + proj : (i : Obj I) → Hom A p0 (FObj Γ i) + proj = pi ( prod (FObj Γ) ) + prodΓ = isIProduct ( prod (FObj Γ) ) + mu : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u)) + mu u = pi (prod Fcod ) (Homprod u) + limit-ε : NTrans I A (K A I (equalizer-c equ-ε ) ) Γ + limit-ε = record { + TMap = λ i → tmap i ; + isNTrans = record { commute = commute1 } + } where + tmap : (i : Obj I) → Hom A (FObj (K A I d) i) (FObj Γ i) + tmap i = A [ proj i o e ] + commute1 : {j k : Obj I} {u : Hom I j k} → + A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K A I d) u ] ] + commute1 {j} {k} {u} = let open ≈-Reasoning (A) in begin + FMap Γ u o tmap j + ≈⟨⟩ + FMap Γ u o ( proj j o e ) + ≈⟨ assoc ⟩ + ( FMap Γ u o pi (prod (FObj Γ)) j ) o e + ≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩ + ( mu u o g ) o e + ≈↑⟨ assoc ⟩ + mu u o (g o e ) + ≈⟨ cdr ( fe=ge (isEqualizer equ-ε )) ⟩ + mu u o (f o e ) + ≈⟨ assoc ⟩ + (mu u o f ) o e + ≈⟨ car ( pif=q (isIProduct (prod Fcod ))) ⟩ + pi (prod (FObj Γ)) k o e + ≈⟨⟩ + proj k o e + ≈↑⟨ idR ⟩ + (proj k o e ) o id1 A d + ≈⟨⟩ + tmap k o FMap (K A I d) u + ∎ fh=gh : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → A [ A [ g o iproduct prodΓ (TMap t) ] ≈ A [ f o iproduct prodΓ (TMap t) ] ] fh=gh a t = let open ≈-Reasoning (A) in begin g o iproduct prodΓ (TMap t) ≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) )) - ≈⟨ ip-cong (isIProduct (prod Fcod)) (comm3 a t ) ⟩ + ≈⟨ ip-cong (isIProduct (prod Fcod)) ( λ u → begin + pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) ) + ≈⟨ assoc ⟩ + ( pi (prod Fcod) u o g ) o iproduct prodΓ (TMap t) + ≈⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ + (FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ) o iproduct prodΓ (TMap t) + ≈↑⟨ assoc ⟩ + FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u) o iproduct prodΓ (TMap t) ) + ≈⟨ cdr ( pif=q prodΓ ) ⟩ + FMap Γ (hom u) o TMap t (hom-j u) + ≈⟨ IsNTrans.commute (isNTrans t) ⟩ + TMap t (hom-k u) o id1 A a + ≈⟨ idR ⟩ + TMap t (hom-k u) + ≈↑⟨ pif=q prodΓ ⟩ + pi (prod (FObj Γ)) (hom-k u) o iproduct prodΓ (TMap t) + ≈↑⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ + (pi (prod Fcod) u o f ) o iproduct prodΓ (TMap t) + ≈↑⟨ assoc ⟩ + pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t) ) + ∎ + ) ⟩ iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t)) ) ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ f o iproduct prodΓ (TMap t) ∎ - limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim + limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d limit1 a t = k equ (iproduct prodΓ (TMap t) ) ( fh=gh a t ) t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → - A [ A [ TMap (limit-ε prod eqa ) i o limit1 a t ] ≈ TMap t i ] + A [ A [ TMap limit-ε i o limit1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin - TMap (limit-ε prod eqa ) i o limit1 a t + TMap limit-ε i o limit1 a t ≈⟨⟩ ( ( proj i ) o e ) o k equ (iproduct prodΓ (TMap t) ) (fh=gh a t) ≈↑⟨ assoc ⟩ @@ -478,8 +465,8 @@ ≈⟨ pif=q prodΓ ⟩ 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 eqa ) i o f ] ≈ TMap t i ]) → + limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a d} + → ({i : Obj I} → A [ A [ TMap limit-ε 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