Mercurial > hg > Members > kono > Proof > category

changeset 678:867ea41b331c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
extensionality remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Nov 2017 13:22:59 +0900
parents 3b23eeecd4f8
children 20bdd2f5f708
files pullback.agda
diffstat 1 files changed, 74 insertions(+), 56 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sat Nov 04 15:49:26 2017 +0900
+++ b/pullback.agda	Sun Nov 05 13:22:59 2017 +0900
@@ -313,52 +313,54 @@
 --        p                                     |               |
 --        ^                    proj i o e = ε i |               | ε j = proj j o e
 --        |                                     |               |
---        | e = equalizer (id p) (id p)         |               |
+--        | e = equalizer f g                   |               |
 --        |                                     v               v
 --       lim <------------------ d'     a i = Γ i -----------→ Γ j = a j
 --         k ( product pi )                          Γ f
 --                                              Γ f o ε i = ε j 
 --
 
-equc : ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
-        ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
-            → Obj A
-equc prod eqa = equalizer-c (eqa p0id p0id)
-   where
-         p0id = let  open ≈-Reasoning (A) in id1 A (iprod (prod (FObj Γ)))
+-- homprod should be written by IProduct
+record homprod {c : Level } : Set (suc c₁' ⊔ suc c₂' ) where
+   field
+      hom-j : Obj I
+      hom-k : Obj I
+      hom : Hom I hom-j hom-k
+open homprod
+
+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 :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
-     ( aprod :  ( ai : { j k : Obj I} → (Hom I j k)  → Obj A  ) →  ∀{ i j : Obj I} → IProduct A (Hom I i j) ai )
+     ( 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 (equc prod eqa )) Γ
-limit-ε = {!!}
-
-limit-ε' :
-     ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
-     ( aprod :  ( ai : { j k : Obj I} → (Hom I j k)  → Obj A  ) →  ∀{ i j : Obj I} → IProduct A (Hom I i j) ai )
-     ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
-          → NTrans I A (K A I {!!} ) Γ
-limit-ε' prod aprod eqa = record {
+          → NTrans I A (K A I (equalizer-c (equ-ε prod eqa  )) ) Γ
+limit-ε prod eqa = record {
        TMap = λ i → tmap i ; 
-       isNTrans = record { commute = {!!} }
+       isNTrans = record { commute = commute1 }
    } where
        p0 : Obj A
        p0 = iprod (prod (FObj Γ))
-       Fcod : { j k : Obj I } ( u : Hom I j k ) → Obj A
-       Fcod = λ  u →  FObj Γ (Category.cod I u)
-       equ : ∀{ j k : Obj I } → Equalizer A
-           (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → A [ FMap Γ h o pi (prod (FObj Γ)) j ] ))
-           (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → pi (prod (FObj Γ)) k ))
-       equ {j} {k} = let  open ≈-Reasoning (A) in
-           eqa (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → A [ FMap Γ h o pi (prod (FObj Γ)) j ] ))
-           (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → pi (prod (FObj Γ)) k ))
-       d : ∀{ j k : Obj I } → Obj A
-       d {j} {k} = equalizer-c (equ {j} {k} )
-       e : ∀{ j k : Obj I } → Hom A d p0
-       e {j} {k} = equalizer (equ {j} {k} )
+       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} →
@@ -369,16 +371,16 @@
               FMap Γ u o ( proj j o e )
          ≈⟨ assoc ⟩
               ( FMap Γ u o  pi (prod (FObj Γ)) j ) o e 
-         ≈↑⟨ car (car ( pif=q (isIProduct (aprod Fcod )))  ) ⟩
-             (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (FMap Γ)) o  pi (prod (FObj Γ)) j ) o e 
-         ≈⟨ {!!} ⟩
-             (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (FMap Γ)) o  pi (prod (FObj Γ)) j ) o e 
-         ≈⟨ {!!} ⟩
-             (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (λ e → id1 A (FObj Γ (Category.cod I e)))) o  pi (prod (FObj Γ)) k ) o e 
-         ≈⟨ car (car ( pif=q (isIProduct (aprod Fcod )))  ) ⟩
-              ( id1 A (FObj Γ k) o pi (prod (FObj Γ)) k  ) o e 
-         ≈⟨ {!!} ⟩
-              ( pi (prod (FObj Γ)) k ) o e 
+         ≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩
+             ( pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o g ) o e 
+         ≈↑⟨ assoc ⟩
+               pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o (g  o e )
+         ≈⟨ cdr ( fe=ge (isEqualizer (equ-ε prod eqa ))) ⟩
+               pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o (f  o e )
+         ≈⟨ assoc ⟩
+             ( pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o f ) o e 
+         ≈⟨ car ( pif=q (isIProduct (prod Fcod )))   ⟩
+               pi (prod (FObj Γ)) k o e 
          ≈⟨⟩
               proj k o e 
          ≈↑⟨ idR ⟩
@@ -388,12 +390,12 @@
          ∎ 
 
 limit-from :
-     ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+     ( 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 = equalizer-c p0equ ;
-     t0 = limit-ε prod {!!} eqa ; 
+     a0 = lim ;
+     t0 = limit-ε prod eqa ; 
      isLimit = record {
              limit = λ a t → limit1 a t ;
              t0f=t = λ {a t i } → t0f=t1  {a} {t} {i} ;
@@ -401,36 +403,52 @@
      }
     }  where
          lim : Obj A 
-         lim = equc prod eqa 
+         lim = equalizer-c ( equ-ε prod eqa )
          p0 = iprod (prod (FObj Γ))
-         p0id = let  open ≈-Reasoning (A) in id1 A p0 
-         p0equ = eqa p0id p0id
-         e = let  open ≈-Reasoning (A) in equalizer ( eqa (id1 A p0 ) ( id1 A p0 ) )
-         equ = isEqualizer (eqa (id1 A p0) (id1 A p0 ))
+         e = let  open ≈-Reasoning (A) in equalizer ( equ-ε prod eqa )
+         equ = isEqualizer  ( equ-ε prod eqa )
          proj = pi ( prod  (FObj Γ) )
          prodΓ = isIProduct ( prod (FObj Γ) ) 
+         open import Relation.Binary.Core
+         import Relation.Binary.PropositionalEquality
+         postulate extensionality : {c : Level} {U : Set c} {x y  : Obj A } {f g : U  → Hom A x y } → ( ∀ (u : U)  → A [ f u ≈  g u ] ) → ( λ u → f u ) ≡ ( λ u → g u ) 
+         comm : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) →
+            A [ A [ iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ])
+                  o iproduct prodΓ (TMap t) ]
+              ≈ A [ iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u))
+                  o iproduct prodΓ (TMap t) ] ]
+         comm a t = let  open ≈-Reasoning (A) in begin
+                  iproduct (isIProduct (prod Fcod)) (λ u → ( FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u))) o iproduct prodΓ (TMap t) 
+                ≈⟨ car ( ip-cong (isIProduct (prod Fcod)) ( extensionality  ( λ u →   begin
+                        FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u)
+                     ≈⟨ ? ⟩
+                        pi (prod (FObj Γ)) (hom-k u)
+                     ∎
+                    ))) ⟩
+                  iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u)) o iproduct prodΓ (TMap t) 
+                ∎
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
-         limit1 a t = let  open ≈-Reasoning (A) in k equ (iproduct prodΓ (TMap t) ) refl-hom
+         limit1 a t = let  open ≈-Reasoning (A) in k equ (iproduct prodΓ (TMap t) ) ( comm 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-ε prod eqa ) 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-ε prod eqa ) i o limit1 a t 
                 ≈⟨⟩
-                   ( ( proj i )  o e ) o  k equ (iproduct prodΓ (TMap t) ) refl-hom
+                   ( ( proj i )  o e ) o  k equ (iproduct prodΓ (TMap t) ) (comm a t)
                 ≈↑⟨ assoc  ⟩
-                    proj i  o ( e  o  k equ (iproduct prodΓ (TMap t) ) refl-hom )
+                    proj i  o ( e  o  k equ (iproduct prodΓ (TMap t) ) (comm a t ) )
                 ≈⟨ cdr ( ek=h equ) ⟩
                     proj i  o iproduct prodΓ (TMap t)
                 ≈⟨ 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 ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa ) 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
                 ≈⟨⟩
-                    k equ (iproduct prodΓ (TMap t) ) refl-hom
+                    k equ (iproduct prodΓ (TMap t) ) (comm a t)
                 ≈⟨ IsEqualizer.uniqueness  equ ( begin
                       e o f 
                 ≈↑⟨ ip-uniqueness prodΓ ⟩