Mercurial > hg > Members > kono > Proof > category

changeset 375:5a6db4bc4d9b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
still trying ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Mar 2016 17:33:56 +0900
parents 5641b923201e
children f48940ff0814
files limit-to.agda
diffstat 1 files changed, 44 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 06 12:17:14 2016 +0900
+++ b/limit-to.agda	Sun Mar 06 17:33:56 2016 +0900
@@ -33,27 +33,33 @@
    t0 : TwoObject 
    t1 : TwoObject 
 
-record TwoCat  {ℓ c₁ c₂ : Level  } (A : Category  c₁ c₂ ℓ)  ( a b : Obj A ) ( f g : Hom A a b ): Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
+record TwoCat  {ℓ c₁ c₂ : Level  } (I : Category  c₁ c₂ ℓ) (A : Category  c₁ c₂ ℓ)  ( a b : Obj A ) ( f g : Hom A a b ): Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
     field
-         obj→ : Obj A  -> TwoObject 
-         hom→ : {a b : Obj A} -> Hom A a b -> TwoObject
-         f-rev : Hom A b a   -- existence of this can be shown using completeness
+         obj→ : Obj I  -> TwoObject 
+         obj← : TwoObject  -> Obj I
+         obj-iso : {a : Obj I} -> obj← ( obj→ a) ≡ a
+         obj-rev : {a : TwoObject } -> obj→ ( obj← a) ≡ a
+         hom→ : { x y : Obj I  } -> Hom I x y -> TwoObject
+         hom← : TwoObject  -> Hom I ( obj← t0 ) ( obj← t1)
+         hom-iso : {a :  Hom I ( obj← t0 ) ( obj← t1)} -> hom← ( hom→ a) ≡ a
+         hom-rev : {a : TwoObject } -> hom→ ( hom← a) ≡ a
+         f-rev : Hom A b a   
          feq : A [ A [ f-rev o  f ] ≈  id1 A a ]
          geq : A [ A [ f-rev o  g ] ≈  id1 A a ]
-    fobj : Obj A -> Obj A
-    fobj x with  obj→ x
-    ... | t0 = a
-    ... | t1 = b
+    fobj : Obj I -> Obj A
+    fobj  x with obj→ x 
+    fobj  x | t0 = a
+    fobj  x | t1 = b
     fmap' :   TwoObject -> Hom A a b
     fmap' t0 = f
     fmap' t1 = g
 
 open TwoCat
 
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-        ( a b : Obj A ) ( f g : Hom A a b )  -> (two : TwoCat A a b f g ) 
-            -> Functor A A
-indexFunctor A a b f g two = record {
+indexFunctor :  {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) 
+        ( a b : Obj A ) ( f g : Hom A a b )  -> (two : TwoCat I A a b f g ) 
+            -> Functor I A
+indexFunctor I A a b f g two = record {
          FObj = λ a → fobj two a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
@@ -62,60 +68,65 @@
              ; ≈-cong = {!!}
        }
       } where
-          fmap :  {x y : Obj A } -> Hom A x y -> Hom A (fobj two x) (fobj two y)
-          fmap {x} {y} f' with obj→ two x | obj→ two y 
+          fmap :  {x y : Obj I } -> Hom I x y -> Hom A (fobj two x) (fobj two y)
+          fmap {x} {y} f with obj→ two x | obj→ two y 
           ... | t0 | t0 = id1 A a
           ... | t1 | t0 = f-rev two
           ... | t1 | t1 = id1 A b
-          ... | t0 | t1  = fmap' two (hom→ two f')
-          identity :  {x : Obj A} → A [ fmap (id1 A  x) ≈ id1 A  (fobj two x) ]
+          ... | t0 | t1  = fmap' two (hom→ two f) 
+          identity :  {x : Obj I} → A [ fmap (id1 I  x) ≈ id1 A  (fobj two x) ]
           identity {x} with obj→ two x
           ... | t0 = let open ≈-Reasoning (A) in refl-hom
           ... | t1 = let open ≈-Reasoning (A) in refl-hom
-          distr : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} → A [ fmap (A [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
-          distr {a₁} {b₁} {c} {f₁} {g₁}  with obj→  two  a₁  | obj→  two  b₁  | obj→  two  c
+          distr : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ]
+          distr {a₁} {b₁} {c} {f₁} {g₁}  with obj→  two  c   | obj→  two  b₁  | obj→  two  a₁
           ... | t0 | t0 | t0 = let open ≈-Reasoning (A) in
               begin
                  id1 A a
               ≈↑⟨ idL ⟩
                  id1 A a  o id1 A a
               ∎
-          ... | t0 | t0 | t1 = {!!}
+          ... | t0 | t0 | t1 = let open ≈-Reasoning (A) in 
+              begin
+                  ?
+              ≈⟨ {!!} ⟩
+                 {!!}
+              ∎
           ... | t0 | t1 | t0 = {!!} 
           ... | t0 | t1 | t1 = {!!} 
           ... | t1 | t0 | t0 = {!!}
           ... | t1 | t0 | t1 = {!!}
           ... | t1 | t1 | t0 = {!!}
-          ... | t1 | t1 | t1 = {!!}
-          ≈-cong :   {a : Obj A} {b : Obj A} {f : Hom A a b} {g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ]
-          ≈-cong {a} {b} {f} {g}  f≈g = let open ≈-Reasoning (A) in ?
+          ... | t1 | t1 | t1 = let open ≈-Reasoning (A) in {!!}
+          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]
+          ≈-cong {a} {b} {f} {g}  f≈g = let open ≈-Reasoning (A) in {!!}
 
 open Limit
 
-lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+lim-to-equ : {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) 
       (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
-        →  {a b c : Obj A}   (f g : Hom A  a b ) (two : TwoCat A a b f g ) 
+        →  {a b c : Obj A}   (f g : Hom A  a b ) (two : TwoCat I A a b f g ) 
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ A lim {a} {b} {c}  f g two e fe=ge = record {
+lim-to-equ I A lim {a} {b} {c}  f g two e fe=ge = record {
         fe=ge =  fe=ge
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
-         Γ = indexFunctor A a b f g two
-         nmap :  (x : Obj A) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A A d) x) (FObj Γ x)
+         Γ = indexFunctor I A a b f g two
+         nmap :  (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x)
          nmap x d h with (obj→  two x)
          ... | t0 = h
          ... | t1 = A [ fmap' two (obj→  two x) o  h ]
-         lemma1 :  {x y : Obj A}  {f' : Hom A x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ]
+         lemma1 :  {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 ] ]
                  →  A [ A [ fmap' two (hom→ two f') o h ] ≈ A [ fmap' two (obj→ two y)  o h ] ]
          lemma1 {x} {y} {f'} d h fh=gh with  (hom→ two f') |  (obj→ two y)
          ... | t0 | t0 = let open ≈-Reasoning (A) in refl-hom
          ... | t0 | t1 = fh=gh
          ... | t1 | t0 = let open ≈-Reasoning (A) in sym fh=gh
          ... | t1 | t1 =  let open ≈-Reasoning (A) in refl-hom
-         commute1 : {x y : Obj A}  {f' : Hom A x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] 
-                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A A d) f' ] ]
+         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 ] ] 
+                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
          commute1  {x} {y} {f'} d h fh=gh with (obj→ two x) | (obj→ two y)
          ... | t0 | t0 = let open ≈-Reasoning (A) in 
               begin
@@ -127,7 +138,7 @@
               ∎ 
          ... | t0 | t1 = let open ≈-Reasoning (A) in 
               begin
-                fmap' two (hom→ two f')  o h
+                fmap' two (hom→ two f') o h
               ≈⟨ lemma1 {x} {y} {f'} d h fh=gh ⟩
                 fmap' two (obj→  two y) o  h 
               ≈↑⟨ idR ⟩
@@ -145,7 +156,7 @@
               ≈⟨ {!!} ⟩
                  (fmap' two (obj→  two y) o  h ) o id1 A d
               ∎
-         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans A A (K A A d) Γ
+         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
          nat d h fh=gh = record {
             TMap = λ x → nmap x d h ; 
             isNTrans = record {
@@ -153,7 +164,7 @@
             }
           }
          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
-         k {d} h fh=gh  = limit (lim A Γ  {c} {nat c e fe=ge }) d (nat d h fh=gh )
+         k {d} h fh=gh  = limit (lim I Γ  {c} {nat c e fe=ge }) d (nat d h fh=gh )
          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 ]
          ek=h d h fh=gh = {!!}
          uniquness :  (d : Obj A ) (h : Hom A d a ) ->  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  ->