Mercurial > hg > Members > kono > Proof > category

changeset 369:a8ac736d73ff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplify
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Mar 2016 00:23:35 +0900
parents b18585089d2e
children 93540deafde7
files limit-to.agda
diffstat 1 files changed, 24 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sat Mar 05 23:56:17 2016 +0900
+++ b/limit-to.agda	Sun Mar 06 00:23:35 2016 +0900
@@ -29,25 +29,17 @@
    t0 : TwoObject 
    t1 : TwoObject 
 
-
-record TwoCat  {ℓ c₁ c₂ : Level  } (Two : Category  c₁ c₂ ℓ) : Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
+record TwoCat  {ℓ c₁ c₂ : Level  } (A : Category  c₁ c₂ ℓ) : Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
     field
-         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
-         hom-conv :  (x y : Obj Two) -> Hom Two x y -> Hom Two (obj← t0) (obj← t1)
+         obj→ : Obj A  -> TwoObject 
+         hom→ : {a b : Obj A} -> Hom A a b -> TwoObject
 
 open TwoCat
 
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (Two : Category c₁ c₂ ℓ) (two : TwoCat Two ) -> 
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> (two : TwoCat A) ->
         ( a b : Obj A ) ( f g : Hom A a b ) ( f-rev : Hom A b a ) 
-        -> Functor Two A
-indexFunctor A Two two a b f g f-rev = record {
+        -> Functor A A
+indexFunctor A two a b f g f-rev = record {
          FObj = λ a → fobj a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
@@ -56,40 +48,39 @@
              ; ≈-cong = {!!}
        }
       } where
-          fobj : Obj Two -> Obj A
+          fobj : Obj A -> Obj A
           fobj x with  obj→ two x
           ... | t0 = a
           ... | t1 = b
-          fmap' :  (x y : Obj Two) -> TwoObject -> Hom A a b
+          fmap' :  (x y : Obj A) -> TwoObject -> Hom A a b
           fmap' _ _ t0 = f
           fmap' _ _ t1 = g
-          fmap :  {x y : Obj Two } -> Hom Two x y -> Hom A (fobj x) (fobj y)
+          fmap :  {x y : Obj A } -> Hom A x y -> Hom A (fobj x) (fobj y)
           fmap {x} {y} f' with obj→ two x | obj→ two y 
           ... | t0 | t0 = id1 A a
           ... | t1 | t0 = f-rev
           ... | t1 | t1 = id1 A b
-          ... | t0 | t1  = fmap' x y (hom→ two (hom-conv two x y f'))
+          ... | t0 | t1  = fmap' x y (hom→ two f')
 
 open Limit
 
-lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (Two : Category c₁ c₂ ℓ) (two : TwoCat Two ) 
+lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (two : TwoCat A ) 
       (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-rev : 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 two lim {a} {b} {c} f-rev f g e fe=ge = record {
+lim-to-equ A two lim {a} {b} {c} f-rev f g 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
-         Γ = indexFunctor A Two two a b f g f-rev
-         nmap :  (x : Obj Two) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A Two d) x) (FObj Γ x)
+         Γ = indexFunctor A two a b f g f-rev
+         nmap :  (x : Obj A) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A A d) x) (FObj Γ x)
          nmap x d h with (obj→  two x)
          ... | t0 = h
          ... | t1 = A [ f  o  h ]
-         commute1 : {x y : Obj Two}  {f' : Hom Two x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ] -> TwoObject -> TwoObject 
-                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A Two d) f' ] ]
+         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 ] ] -> TwoObject -> TwoObject 
+                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A A d) f' ] ]
          commute1  {x} {y} {f'} d h fh=gh t0 t0 =   let open ≈-Reasoning (A) in 
               begin
                   FMap Γ f' o nmap x d h
@@ -98,17 +89,21 @@
               ≈↑⟨ idR ⟩
                   nmap y d h o id1 A d
               ≈⟨⟩
-                  nmap y d h o FMap (K A Two d) f' 
+                  nmap y d h o FMap (K A A d) f' 
               ∎
          commute1  {x} {y} {f'} d h fh=gh t0 t1 =   let open ≈-Reasoning (A) in 
               begin
                   FMap Γ f' o nmap x d h
               ≈⟨ {!!} ⟩
-                  nmap y d h o FMap (K A Two d) f'
+                  nmap y d h 
+              ≈↑⟨ idR ⟩
+                  nmap y d h o id1 A d
+              ≈⟨⟩
+                  nmap y d h o FMap (K A A d) f'
               ∎
          commute1  {x} {y} {f'} d h fh=gh t1 t0 =  {!!}
          commute1  {x} {y} {f'} d h fh=gh t1 t1 =  {!!}
-         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans Two A (K A Two 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 h fh=gh = record {
             TMap = λ x → nmap x d h ; 
             isNTrans = record {
@@ -116,5 +111,5 @@
             }
           }
          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 Two Γ  {c} {nat c e fe=ge }) d (nat d h fh=gh )
+         k {d} h fh=gh  = limit (lim A Γ  {c} {nat c e fe=ge }) d (nat d h fh=gh )