changeset 495:633df882db86

fryed1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Mar 2017 13:08:03 +0900
parents ba6a67523523
children 5c7908202d5a
files cat-utility.agda freyd.agda freyd1.agda limit-to.agda pullback.agda
diffstat 5 files changed, 38 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Tue Mar 14 12:14:57 2017 +0900
+++ b/cat-utility.agda	Tue Mar 14 13:08:03 2017 +0900
@@ -308,7 +308,7 @@
              limit :  ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
              t0f=t :  { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
                  A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
-             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → ( f : Hom A a a0 ) → ( ∀ { i : Obj I } →
+             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
                  A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
 
         record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
--- a/freyd.agda	Tue Mar 14 12:14:57 2017 +0900
+++ b/freyd.agda	Tue Mar 14 13:08:03 2017 +0900
@@ -82,9 +82,9 @@
       e=id  {e} uce=uc =  let open ≈-Reasoning (A) in
             begin
               e
-            ≈↑⟨ limit-uniqueness  (isLimit (lim F)) e ( λ {i} → uce=uc ) ⟩
+            ≈↑⟨ limit-uniqueness  (isLimit (lim F)) ( λ {i} → uce=uc ) ⟩
               limit (isLimit (lim F)) a00 u 
-            ≈⟨ limit-uniqueness (isLimit (lim F)) (id1 A a00) ( λ {i} → idR ) ⟩
+            ≈⟨ limit-uniqueness (isLimit (lim F))  ( λ {i} → idR ) ⟩
               id1 A a00

       kfuc=uc : {c k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ TMap u  c  o  
--- a/freyd1.agda	Tue Mar 14 12:14:57 2017 +0900
+++ b/freyd1.agda	Tue Mar 14 13:08:03 2017 +0900
@@ -166,10 +166,10 @@
               TMap (limit-u comp (FIA Γ)) b  o FMap (K A I (limit-c comp (FIA Γ))) f 

 
-gnat :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
-     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → 
+gnat :  { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory )
+     →  (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → 
               NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ)
-gnat {I} comp Γ glimit a t = record {
+gnat {I} Γ a t = record {
        TMap = λ i → C [  hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ]
       ; isNTrans = record { commute = λ {x y f} → comm1 x y f }
     } where
@@ -209,12 +209,24 @@
         ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ]
       comm1 =  let  open ≈-Reasoning (C) in begin
             FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a 
-         ≈⟨ {!!} ⟩
-            limit (isLimit (LimitC comp Γ glimit  )) (FObj F (obj a)) (gnat comp Γ glimit a t )
-         ≈⟨ limit-uniqueness  (isLimit (LimitC comp Γ glimit  )) 
-             (limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )  
-                o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
-             ) ( λ {i} → begin 
+         ≈↑⟨ limit-uniqueness  (isLimit (LimitC comp Γ glimit  ))  ( λ {i} → begin
+                     TMap (t0 (LimitC comp Γ glimit)) i o ( FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a )
+                  ≈⟨ assoc  ⟩ 
+                     ( TMap (t0 (LimitC comp Γ glimit)) i o  FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a 
+                  ≈⟨⟩ 
+                     ( FMap G ( TMap (limit-u comp (FIA Γ )) i ) o  FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a 
+                  ≈↑⟨ car ( distr G ) ⟩ 
+                     FMap G ( A [ TMap (limit-u comp (FIA Γ )) i  o  limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] )  o hom a 
+                  ≈⟨ car ( fcong G ( t0f=t (isLimit (climit comp (FIA Γ ))))) ⟩ 
+                     FMap G (arrow (TMap t i))  o hom a 
+                  ≈⟨ comm ( TMap t i) ⟩ 
+                     hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i )
+                  ≈⟨⟩ 
+                     TMap (gnat Γ a t) i
+                  ∎
+           ) ⟩
+            limit (isLimit (LimitC comp Γ glimit  )) (FObj F (obj a)) (gnat Γ a t )
+         ≈⟨ limit-uniqueness  (isLimit (LimitC comp Γ glimit  )) ( λ {i} → begin 
                       TMap (t0 (LimitC comp Γ glimit  )) i  o
                          ( limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )  
                           o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) )
@@ -235,8 +247,8 @@
                                FMap F ( A [ TMap (t0 ( climit comp (FIA Γ)))  i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] )
                    ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ 
                            hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i )
-                   ≈⟨ {!!} ⟩ 
-                       TMap {!!} i
+                   ≈⟨⟩ 
+                       TMap (gnat Γ a t ) i

            ) ⟩
             limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )  
@@ -261,7 +273,7 @@
      → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ]
 comma-uniqueness  {I} comp Γ glimit a t f t=f    = let  open ≈-Reasoning (A) in begin
              limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
-         ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) (arrow f)  t=f ⟩
+         ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) )   t=f ⟩
              arrow f

 
@@ -275,6 +287,6 @@
      isLimit = record {
              limit = λ a t → comma-a0 comp Γ glimit a t ;
              t0f=t = λ {a t i } →  comma-t0f=t  comp Γ glimit a t i ;
-             limit-uniqueness =  λ {a} {t} f t=f →  comma-uniqueness  {I} comp Γ glimit a t f t=f
+             limit-uniqueness =  λ {a} {t} {f} t=f →  comma-uniqueness  {I} comp Γ glimit a t f t=f
      }
    }
--- a/limit-to.agda	Tue Mar 14 12:14:57 2017 +0900
+++ b/limit-to.agda	Tue Mar 14 13:08:03 2017 +0900
@@ -226,7 +226,7 @@
                 → A [ A [ e o k' ] ≈ h ] → A [ k h  fh=gh   ≈ k' ]
          uniquness d h fh=gh k' ek'=h =  let open  ≈-Reasoning A in  begin
                     k h fh=gh
-                ≈⟨ limit-uniqueness (isLimit lim) k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
+                ≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
                     k'

 
@@ -290,7 +290,7 @@
         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 ] ]
         ipu {i} q h = let open  ≈-Reasoning A in  refl-hom
         ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
-        ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i  o h ]  )} h (ipu q h)
+        ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i  o h ]  )} (ipu q h)
         ipc : {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 [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
@@ -309,4 +309,4 @@

         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 [ iproduct qi ≈ iproduct qi' ]
-        ip-cong {q} {qi} {qi'} qi=qi' =  limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))
+        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))
--- a/pullback.agda	Tue Mar 14 12:14:57 2017 +0900
+++ b/pullback.agda	Tue Mar 14 13:08:03 2017 +0900
@@ -155,7 +155,7 @@
            iso-l I Γ lim lim' o iso-r I Γ lim lim'
       ≈⟨⟩
            limit (isLimit lim') (a0 lim) ( t0 lim) o  limit (isLimit lim) (a0 lim') (t0 lim')
-      ≈↑⟨ limit-uniqueness (isLimit lim') ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim )(a0 lim') (t0 lim') )( λ {i} → ( begin
+      ≈↑⟨ limit-uniqueness (isLimit lim') ( λ {i} → ( begin
           TMap (t0 lim') i o ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') )
       ≈⟨ assoc  ⟩
           ( TMap (t0 lim') i o  limit (isLimit lim') (a0 lim) (t0 lim) ) o limit (isLimit lim) (a0 lim') (t0 lim')
@@ -165,7 +165,7 @@
           TMap (t0 lim') i
       ∎) ) ⟩
            limit (isLimit lim') (a0 lim') (t0 lim')
-      ≈⟨ limit-uniqueness (isLimit lim') (id (a0 lim')) idR ⟩
+      ≈⟨ limit-uniqueness (isLimit lim')  idR ⟩
            id (a0 lim' )

 
@@ -246,7 +246,7 @@
          → A [ limit (isLimit (lim b )) a f ≈ g ]
    couniquness2 {b} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
             limit (isLimit (lim b )) a f
-        ≈⟨ limit-uniqueness (isLimit ( lim b )) g lim-g=f ⟩
+        ≈⟨ limit-uniqueness (isLimit ( lim b )) lim-g=f ⟩
             g

 
@@ -266,7 +266,7 @@
      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
+             limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
  } where
      limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
@@ -362,7 +362,7 @@
      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
+             limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
     }  where
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
@@ -437,7 +437,7 @@
      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
+             limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
     } where
          ta = ta1 B Γ (a0 limitb) (t0 limitb) U
@@ -509,7 +509,7 @@
                  limit1 a t
                ≈⟨⟩
                  FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a  
-               ≈⟨ car ( fcong U (limit-uniqueness (isLimit limitb) (B [ TMap ε lim o FMap F f ] ) ( λ {i} →  lemma1 i) )) ⟩
+               ≈⟨ car ( fcong U (limit-uniqueness (isLimit limitb)  ( λ {i} →  lemma1 i) )) ⟩
                  FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a   -- Universal mapping 
                ≈⟨ car (distr U ) ⟩
                  ( (FMap U (TMap ε lim))  o (FMap U ( FMap F f )) ) o TMap η a