Mercurial > hg > Members > kono > Proof > category

changeset 365:41ec06dd4b21

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 05 Mar 2016 13:20:36 +0900
parents e8e98be4ce57
children e07b7578d2e7
files limit-to.agda
diffstat 1 files changed, 50 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sat Mar 05 08:23:46 2016 +0900
+++ b/limit-to.agda	Sat Mar 05 13:20:36 2016 +0900
@@ -15,8 +15,25 @@
 ---          f
 ---       ------>
 ---     0         1
+---       <------
+---          frev
+---          
+---          
+---          
+---          f
 ---       ------>
----          g
+---     a         b
+---       ------>
+---     ^    g
+---     |    
+---     |e     
+---     |    
+---     c    
+---     ^    
+---     |    
+---     |k   
+---     |    
+---     d    
 
 
 data TwoObject   : Set where
@@ -26,51 +43,53 @@
 
 record TwoCat  {ℓ c₁ c₂ : Level  } (Two : Category  c₁ c₂ ℓ) : Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
     field
-         hom→ : Obj Two  -> TwoObject 
-         hom← : TwoObject  -> Obj Two
-         hom-iso : {a : Obj Two} -> hom← ( hom→ a) ≡ a
+         obj→ : Obj Two  -> TwoObject 
+         obj← : TwoObject  -> Obj Two
+         obj-iso : {a : Obj Two} -> obj← ( obj→ a) ≡ a
+         obj-rev : {a : TwoObject } -> obj→ ( obj← a) ≡ a
+         hom→ : Hom Two ( obj← t0 ) ( obj← t1) -> TwoObject
+         hom← : TwoObject  -> Hom Two ( obj← t0 ) ( obj← t1)
+         hom-iso : {a :  Hom Two ( obj← t0 ) ( obj← t1)} -> hom← ( hom→ a) ≡ a
          hom-rev : {a : TwoObject } -> hom→ ( hom← a) ≡ a
 
+open TwoCat
 
-open TwoCat
+record TwoFunctor  {ℓ c₁ c₂ : Level  } (I A : Category  c₁ c₂ ℓ) (two : TwoCat I) ( Γ : Functor I A ) ( a b : Obj A ) 
+           ( f g : Hom A  a b )
+                          : Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
+    field
+          Γa :  FObj Γ (obj← two t0)   ≡ a 
+          Γb :  FObj Γ (obj← two t1)   ≡ b 
+          Γmap :  Hom A a b  -> Hom A (FObj Γ (obj← two t0)) (FObj Γ (obj← two t1))
+          Γmap-rev :  Hom A (FObj Γ (obj← two t0)) (FObj Γ (obj← two t1)) -> Hom A a b  
+          Γf :  A [ FMap Γ (hom← two t0)   ≈ Γmap f ]
+          Γg :  A [ FMap Γ (hom← two t1)   ≈ Γmap g ]
+
+open TwoFunctor
 open Limit
 
 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (two : TwoCat A ) 
+      (Two : Category c₁ c₂ ℓ) (two : TwoCat Two ) 
       (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} {frev : Hom A b a } (f g : Hom A a b)  → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ {c₁} A two lim {a} {b} {c} {frev} f g e fe=ge = record {
+        →  {a b c : Obj A}  (f g : Hom A  a b )
+        → (  Γ : Functor Two A ) (  Γ-two : TwoFunctor Two A two  Γ 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 {c₁} A Two two 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} → {!!}
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
-         Γobj :  TwoObject → Obj A
-         Γobj t0 = a
-         Γobj t1 = b
-         Γmap :  (x : Obj A ) → (y : Obj A ) → Hom A x y →  Hom A (Γobj (hom→ two x)) (Γobj (hom→ two y))
-         Γmap  x y _ with  (hom→ two x) | (hom→ two y)  
-         ... | t0 | t0 = id1 A a
-         ... | t0 | t1 = f
-         ... | t1 | t0 = frev
-         ... | t1 | t1 = id1 A b
-         Γ : Functor A A
-         Γ = record {
-            FObj  = λ x → ( Γobj ( hom→ two x ) ) ;
-            FMap  = λ {x} {y} f  → Γmap x y f ;
-            isFunctor = record {
-                     ≈-cong  = {!!} ; 
-                    identity = {!!} ;
-                    distr = {!!}
-            }
-          }
-         nat : (d : Obj A) → NTrans A A (K A A d) Γ
+         nmap :  (x : Obj Two) ( d : Obj A ) -> Hom A (FObj (K A Two d) x) (FObj Γ x)
+         nmap x d with (obj→  two x)
+         ... | t0 = ?
+         ... | t1 = {!!}
+         nat : (d : Obj A) → NTrans Two A (K A Two d) Γ
          nat d = record {
-            TMap = λ x → {!!} ;
+            TMap = λ x → nmap x d ; 
             isNTrans = record {
                 commute = {!!}
             }
           }
          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}) d (nat d) 
-
+         k {d} h fh=gh  = limit (lim Two Γ  {c} {nat c}) d (nat d)