Mercurial > hg > Members > kono > Proof > category

changeset 385:ff3803fc0c8a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add level
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 14 Mar 2016 14:53:54 +0900
parents e2b493fec8c3
children 1e136aaad5cb
files limit-to.agda
diffstat 1 files changed, 70 insertions(+), 186 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Mon Mar 14 13:08:36 2016 +0900
+++ b/limit-to.agda	Mon Mar 14 14:53:54 2016 +0900
@@ -30,48 +30,48 @@
 ---     d  
 
 
-data  TwoObject   : Set  where
+data  TwoObject {c₁ : Level}  : Set c₁ where
    t0 : TwoObject 
    t1 : TwoObject 
 
-data Arrow   : Set  where
+data Arrow {ℓ : Level }  : Set ℓ where
    id-t0 : Arrow  
    id-t1 :  Arrow
    arrow-f :  Arrow
    arrow-g :  Arrow
 
-record RawHom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
+record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
    field
-       RawMap    : Maybe Arrow 
-       RawSel    : Maybe TwoObject
+       RawMap    : Maybe ( Arrow  {ℓ })
+       RawSel    : Maybe ( TwoObject {c₁} )
 
 open RawHom
 
-arrow2hom : {a b : TwoObject}  -> Maybe Arrow -> RawHom a b
-arrow2hom {t0} {t0} (just id-t0)    =  record { RawMap = just id-t0  ; RawSel = just t0  }
-arrow2hom {t0} {t1} (just arrow-f)  =  record { RawMap = just arrow-f  ; RawSel = just t0  }
-arrow2hom {t0} {t1} (just arrow-g)  =  record { RawMap = just arrow-g  ; RawSel = just t1  }
-arrow2hom {t1} {t1} (just id-t1)    =  record { RawMap = just id-t1  ; RawSel = just t0  }
-arrow2hom {a} {b} _   =  record { RawMap = nothing ; RawSel = nothing  }
+arrow2hom :  {c₁ ℓ : Level} (a b : TwoObject  {c₁} )  -> Maybe (Arrow {ℓ}  ) -> RawHom {c₁} {ℓ} a b
+arrow2hom {_} {_} t0 t0 (just id-t0)    =  record { RawMap = just id-t0  ; RawSel = just t0  }
+arrow2hom {_} {_} t0 t1 (just arrow-f)  =  record { RawMap = just arrow-f  ; RawSel = just t0  }
+arrow2hom {_} {_} t0 t1 (just arrow-g)  =  record { RawMap = just arrow-g  ; RawSel = just t1  }
+arrow2hom {_} {_} t1 t1 (just id-t1)    =  record { RawMap = just id-t1  ; RawSel = just t0  }
+arrow2hom {_} {_} a b _   =  record { RawMap = nothing ; RawSel = nothing  }
 
 
-record Two-Hom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
+record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
-      hom : RawHom a b
-      two-hom-iso :  arrow2hom {a} {b} (RawMap hom)  ≡  hom
+      hom : RawHom { c₁}  {ℓ } a b
+      two-hom-iso :  arrow2hom a b (RawMap hom)  ≡  hom
    Map : Maybe Arrow
    Map = RawMap hom
    Sel : Maybe TwoObject
    Sel = RawSel hom
 
-Two-id :  (a : TwoObject ) ->   Two-Hom a a 
+Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
 Two-id t0  = record { hom = record { RawMap = just id-t0 ; RawSel = just t0 } ; two-hom-iso = refl }
 Two-id t1  = record { hom = record { RawMap = just id-t1 ; RawSel = just t0 } ; two-hom-iso = refl }
 
-Two-nothing : ( a b : TwoObject) -> Two-Hom a b
+Two-nothing : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> Two-Hom  {c₁} { ℓ} a b
 Two-nothing a b  = record { hom = record { RawMap = nothing ; RawSel = nothing  } ; two-hom-iso =  nothing-iso a b }
  where
-        nothing-iso :  (a b : TwoObject ) ->   arrow2hom {a} {b} nothing  ≡  record { RawMap = nothing ; RawSel = nothing  }
+        nothing-iso :  (a b : TwoObject ) ->   arrow2hom a b nothing  ≡  record { RawMap = nothing ; RawSel = nothing  }
         nothing-iso t0 t0 = refl
         nothing-iso t0 t1 = refl
         nothing-iso t1 t0 = refl
@@ -81,17 +81,17 @@
 
 -- arrow composition
 
-twocomp :  Maybe Arrow -> Maybe Arrow -> Maybe Arrow
+twocomp :  {ℓ : Level } -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ }) -> Maybe (Arrow {ℓ } )
 twocomp (just arrow-f) (just id-t0) = just arrow-f
 twocomp (just arrow-g) (just id-t0) = just arrow-g
 twocomp (just id-t0) (just id-t0) = just id-t0
 twocomp (just id-t1) (just id-t1) = just id-t1
 twocomp _ _ = nothing
 
-_×_ :  {A B C : TwoObject } →  Two-Hom B C →  Two-Hom A B  →  Two-Hom A C 
-_×_   {a} {b} {c} f g  = record { hom = arrow2hom ( twocomp (Map f) (Map g) ); two-hom-iso  = comp-iso a c }
+_×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
+_×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom = arrow2hom a c ( twocomp (Map f) (Map g) ); two-hom-iso  = comp-iso a c }
  where
-    comp-iso :  (a c : TwoObject ) →  arrow2hom (RawMap (arrow2hom {a} {c} (twocomp (Map f) (Map g)))) ≡ arrow2hom {a} {c} (twocomp (Map f) (Map g))
+    comp-iso :  (a c : TwoObject ) →  arrow2hom a c (RawMap (arrow2hom a c (twocomp (Map f) (Map g)))) ≡ arrow2hom a c (twocomp (Map f) (Map g))
     comp-iso a c  with (twocomp (Map f) (Map g))
     comp-iso t0 t0 | nothing = refl
     comp-iso t0 t1 | nothing = refl
@@ -115,11 +115,11 @@
     comp-iso t1 t0 | just arrow-g = refl
 
 
-twocat : {ℓ c₁ c₂ : Level  } ->  Category _ _ _ 
-twocat  = record {
-    Obj  = TwoObject  ;
-    Hom = λ a b →   Two-Hom a b   ; 
-    _o_ =  _×_ ;
+TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  (ℓ ⊔ c₁)  ℓ
+TwoCat   {c₁}  {c₂} {ℓ} = record {
+    Obj  = TwoObject  {c₁} ;
+    Hom = λ a b →   Two-Hom {c₁ } { ℓ}  a b   ; 
+    _o_ =  _×_  { c₁}  {ℓ} ;
     _≈_ = λ a b →   Map a ≡ Map b  ;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
@@ -133,92 +133,39 @@
         open  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
         identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
-        identityL {a} {b} {f} with (Map f)
-        identityL {a} {b} {f} | nothing =   let open ≡-Reasoning in
+        identityL {a} {b} {f} =   let open ≡-Reasoning in
               begin
                 {!!}
               ≡⟨ {!!} ⟩
                 {!!}
-              ≡⟨⟩
-                nothing
-             ∎
-        identityL {a} {b} {f} | just id-t0  =   let open ≡-Reasoning in
+              ∎
+        identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
+        identityR {a} {b} {f} =   let open ≡-Reasoning in
               begin
                 {!!}
               ≡⟨ {!!} ⟩
-                just id-t0
-             ∎
-        identityL {a} {b} {f} | just id-t1  =   {!!}
-        identityL {a} {b} {f} | just arrow-f  =  {!!}
-        identityL {a} {b} {f} | just arrow-g  =  {!!}
-        identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
-        identityR {t0} {t0} {f} = {!!}
-        identityR {t1} {t1} {f} = {!!}
-        identityR {t1} {t0} {f} = {!!}
-        identityR {t0} {t1} {f} =  {!!}
+               {!!}
+              ∎
         o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom B C} →
             Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g )
-        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in {!!}
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in
+              begin
+                 {!!}
+              ≡⟨ {!!} ⟩
+                Map (i × g)
+              ∎
         associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )
-        associative {t0} {t0} {t0} {t0} {f} {g} {h} = {!!}
-        associative {t0} {t0} {t0} {t1} {f} {g} {h} = {!!}
-        associative {t0} {t0} {t1} {t0} {f} {g} {h} = {!!}
-        associative {t0} {t0} {t1} {t1} {f} {g} {h} = {!!}
-        associative {t0} {t1} {t0} {t0} {f} {g} {h} = {!!}
-        associative {t0} {t1} {t0} {t1} {f} {g} {h} = {!!}
-        associative {t0} {t1} {t1} {t0} {f} {g} {h} = {!!}
-        associative {t0} {t1} {t1} {t1} {f} {g} {h} = {!!}
-        associative {t1} {t0} {t0} {t0} {f} {g} {h} = {!!}
-        associative {t1} {t0} {t0} {t1} {f} {g} {h} = {!!}
-        associative {t1} {t0} {t1} {t0} {f} {g} {h} = {!!}
-        associative {t1} {t0} {t1} {t1} {f} {g} {h} = {!!}
-        associative {t1} {t1} {t0} {t0} {f} {g} {h} = {!!}
-        associative {t1} {t1} {t0} {t1} {f} {g} {h} = {!!}
-        associative {t1} {t1} {t1} {t0} {f} {g} {h} = {!!}
-        associative {t1} {t1} {t1} {t1} {f} {g} {h} = {!!}
-
-
+        associative {_} {_} {_} {_} {f} {g} {h} =  let open ≡-Reasoning in
+              begin
+                Map ( f × (g × h) )
+              ≡⟨ {!!} ⟩
+                Map ( (f × g) × h )
+              ∎
 
-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 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)
-         cong-hom→ : { x y : Obj I  } -> {f g : Hom I x y } ->  I [ f ≈  g ] ->  hom→ f  ≡   hom→ g
-         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 ]
-         feq' : A [ A [ f o  f-rev ] ≈  id1 A b ]
-         geq' : A [ A [ g o  f-rev ] ≈  id1 A b ]
-         I-id : { d : Obj I } -> ( i : Hom I d d ) -> I [ i  ≈  id1 I d ]
-    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
-    two-lemma-1 : {x y : Obj I } -> (i : Hom I x y ) ->  A [ A [ f-rev o fmap' ( hom→  i ) ]  ≈  id1 A a  ] 
-    two-lemma-1 i with hom→ i
-    ... | t0 =  feq
-    ... | t1 =  geq
-    two-lemma-2 : {x y : Obj I } -> (i : Hom I x y ) ->  A [ A [ fmap' ( hom→  i ) o f-rev ]  ≈  id1 A b  ] 
-    two-lemma-2 i with hom→ i
-    ... | t0 =  feq'
-    ... | t1 =  geq'
-
-open TwoCat
-
-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
+indexFunctor :  {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) 
+        ( a b : Obj A ) ( f g : Hom A a b )  ->  Functor TwoCat A
+indexFunctor A a b f g = record {
+         FObj = λ a → fobj a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
              identity = \{x} -> identity {x}
@@ -226,106 +173,43 @@
              ; ≈-cong = {!!}
        }
       } where
-          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 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
+          I = TwoCat
+          fobj :  Obj TwoCat -> Obj A
+          fobj t0 = a
+          fobj t1 = b
+          fmap :  {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y)
+          fmap {X} {Y} x with Map x
+          fmap {t0} {t1} x  | just arrow-f = f
+          fmap {t0} {t1} x  | just arrow-g = g
+          fmap {t0} {t0} x  | just id-t0 = id1 A a
+          fmap {t1} {t1} x  | just id-t1 = id1 A b
+          fmap {_} {_} x  | _ = {!!}
+          identity :  {x : Obj I} → A [ fmap (id1 I  x) ≈ id1 A  (fobj x) ]
+          identity  = {!!}
           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 sym idL
-          ... | t0 | t0 | t1 = let open ≈-Reasoning (A) in sym idL
-          ... | t0 | t1 | t0 = let open ≈-Reasoning (A) in
-              begin
-                id1 A a
-              ≈↑⟨ two-lemma-1 two  f₁  ⟩
-                f-rev two  o fmap' two ( hom→  two  f₁ )
-              ∎
-          ... | t0 | t1 | t1 = let open ≈-Reasoning (A) in 
-              begin
-                f-rev two
-              ≈↑⟨ idR ⟩
-                 f-rev two o id1 A b
-              ∎
-          ... | t1 | t0 | t0 = let open ≈-Reasoning (A) in  
-              begin
-                fmap' two ( hom→  two ( I [ g₁ o f₁ ] ))
-              ≈↑⟨  ≡-cong  (cong-hom→ two  ( {!!} ) ) (\x -> fmap' two x )  ⟩
-                fmap' two ( hom→  two  g₁ )   
-              ≈↑⟨ idR ⟩
-                fmap' two ( hom→  two  g₁ )   o id1 A a
-              ∎
-          ... | t1 | t0 | t1 = let open ≈-Reasoning (A) in 
-              begin
-                id1 A b
-              ≈↑⟨ two-lemma-2 two  g₁  ⟩
-                fmap' two ( hom→  two  g₁ ) o f-rev two
-              ∎
-          ... | t1 | t1 | t0 = let open ≈-Reasoning (A) in {!!}
-          ... | t1 | t1 | t1 = let open ≈-Reasoning (A) in sym idR
+          distr {a₁} {b₁} {c} {f₁} {g₁}  = {!!}
           ≈-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} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) 
+lim-to-equ : {c₁ c₂ ℓ : Level}  (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 I A a b f g ) 
+        →  {a b c : Obj 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 I A lim {a} {b} {c}  f g two e fe=ge = record {
+lim-to-equ A lim {a} {b} {c}  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} → ek=h d h fh=gh
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
-         Γ = indexFunctor I A a b f g two
+         I = TwoCat
+         Γ = indexFunctor A a b f g 
          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 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
+         nmap x d h = {!!}
          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
-                  id1 A a  o h
-              ≈⟨ idL ⟩
-                  h 
-              ≈↑⟨ idR ⟩
-                  h o id1 A d
-              ∎ 
-         ... | t0 | t1 = let open ≈-Reasoning (A) in 
-              begin
-                fmap' two (hom→ two f') o h
-              ≈⟨ lemma1 {x} {y} {f'} d h fh=gh ⟩
-                fmap' two (obj→  two y) o  h 
-              ≈↑⟨ idR ⟩
-                (fmap' two (obj→  two y) o  h )  o id1 A d
-              ∎ 
-         ... | t1 | t0 =   let open ≈-Reasoning (A) in
-              begin
-                 f-rev two  o ( fmap' two (obj→  two x) o  h )
-              ≈⟨ {!!} ⟩
-                  h o id1 A d
-              ∎
-         ... | t1 | t1 =   let open ≈-Reasoning (A) in
-              begin
-                 id1 A b  o ( fmap' two (obj→  two x) o  h )
-              ≈⟨ {!!} ⟩
-                 (fmap' two (obj→  two y) o  h ) o id1 A d
-              ∎
+         commute1  {x} {y} {f'} d h fh=gh = {!!}
          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 ; 
@@ -334,7 +218,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 I Γ  {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 ] ] )  ->