Mercurial > hg > Members > kono > Proof > category

changeset 455:55a9b6177ed4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 14:58:40 +0900
parents 2f07f4dd9a6d
children 4d97955ea419
files HomReasoning.agda discrete.agda
diffstat 2 files changed, 100 insertions(+), 82 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Mar 02 13:25:05 2017 +0900
+++ b/HomReasoning.agda	Thu Mar 02 14:58:40 2017 +0900
@@ -73,6 +73,8 @@
   sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
+  sym-hom = sym
+
   -- working on another cateogry
   idL1 :  { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } →  A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f  ]
   idL1 A =  IsCategory.identityL (Category.isCategory A)
--- a/discrete.agda	Thu Mar 02 13:25:05 2017 +0900
+++ b/discrete.agda	Thu Mar 02 14:58:40 2017 +0900
@@ -26,17 +26,14 @@
 ---       -----→
 ---          g
 
-data Arrow {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
-   id-t0 : Arrow t0 t0
-   id-t1 : Arrow t1 t1
-   arrow-f :  Arrow t0 t1
-   arrow-g :  Arrow t0 t1
+data TwoHom {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
+   id-t0 : TwoHom t0 t0
+   id-t1 : TwoHom t1 t1
+   arrow-f :  TwoHom t0 t1
+   arrow-g :  TwoHom t0 t1
 
-record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set ( c₂)  where
-   field
-       hom   :  Arrow {c₁} {c₂} a b 
 
-comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  Arrow {c₁} {c₂} b c  →  Arrow {c₁} {c₂} a b   →  Arrow {c₁} {c₂} a c 
+comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  TwoHom {c₁} {c₂} b c  →  TwoHom {c₁} {c₂} a b   →  TwoHom {c₁} {c₂} a c 
 comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f   =   arrow-f 
 comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  =   arrow-g 
 comp {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    =   id-t1 
@@ -47,20 +44,20 @@
 open TwoHom
 
 _×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  ( TwoHom {c₁}  {c₂} b c ) →  ( TwoHom {c₁} {c₂} a b )  →  ( TwoHom {c₁}  {c₂} a c )
-_×_  {c₁}  {c₂}  {a} {b} {c} f g  = record { hom = comp  {c₁}  {c₂}  {a} {b} {c} (hom f) (hom g ) }
+_×_  {c₁}  {c₂}  {a} {b} {c} f g  =  comp  {c₁}  {c₂}  {a} {b} {c} f g
 
 
 --          f    g    h
 --       d <- c <- b <- a
 --
---   It can be proved without Arrow constraints
+--   It can be proved without TwoHom constraints
 
 assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
        {f : (TwoHom {c₁}  {c₂ } c d )} →
        {g : (TwoHom {c₁}  {c₂ } b c )} →
        {h : (TwoHom {c₁}  {c₂ } a b )} →
-       hom ( f × (g × h)) ≡ hom ((f × g) × h )
-assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with  hom f | hom g | hom h
+       ( f × (g × h)) ≡ ((f × g) × h )
+assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with  f | g | h
 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0   | id-t0   | id-t0  = refl
 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0   | id-t0  = refl
 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0   | id-t0  = refl
@@ -71,18 +68,18 @@
 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1   | id-t1   | id-t1  = refl
 
 TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} t0 = record { hom =  id-t0 }
-TwoId {_} {_} t1 = record { hom =  id-t1 }
+TwoId {_} {_} t0 = id-t0 
+TwoId {_} {_} t1 = id-t1 
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
 
-TwoCat : {c₁ c₂ ℓ : Level  } →  Category   c₁  c₂  c₂
-TwoCat   {c₁}  {c₂} {ℓ} = record {
+TwoCat : {c₁ c₂ : Level  } →  Category   c₁  c₂  c₂
+TwoCat   {c₁}  {c₂} = record {
     Obj  = TwoObject  {c₁} ;
     Hom = λ a b →    ( TwoHom {c₁}  {c₂ } a b ) ;
     _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
-    _≈_ =  λ x y → hom x  ≡ hom y ;
+    _≈_ =  λ x y → x  ≡ y ;
     Id  =  λ{a} → TwoId {c₁ } { c₂} a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
@@ -92,36 +89,35 @@
             associative  = λ{a b c d f g h } → assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
        }
    }  where
-        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  ≡ hom f
-        identityL  {c₁}  {c₂}  {a} {b} {f} with hom f
+        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  ((TwoId B)  × f)  ≡ f
+        identityL  {c₁}  {c₂}  {a} {b} {f} with f
         identityL  {c₁}  {c₂}  {t1} {t1} | id-t1 = refl
         identityL  {c₁}  {c₂}  {t0} {t0} | id-t0 = refl
         identityL  {c₁}  {c₂}  {t0} {t1} | arrow-f = refl
         identityL  {c₁}  {c₂}  {t0} {t1} | arrow-g = refl
-        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  ≡ hom f
-        identityR  {c₁}  {c₂}  {_} {_} {f}  with hom f
+        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  ≡ f
+        identityR  {c₁}  {c₂}  {_} {_} {f}  with f
         identityR  {c₁}  {c₂}  {t1} {t1} | id-t1  = refl
         identityR  {c₁}  {c₂}  {t0} {t0} | id-t0 = refl
         identityR  {c₁}  {c₂}  {t0} {t1} | arrow-f = refl
         identityR  {c₁}  {c₂}  {t0} {t1} | arrow-g = refl
         o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
-            hom f  ≡ hom g → hom h  ≡ hom i → hom ( h × f )  ≡ hom ( i × g )
+            f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
         o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = 
           let open  ≡-Reasoning in begin
-                    hom ( h × f )
+                    ( h × f )
                 ≡⟨ refl ⟩
-                    comp (hom h) (hom f)
-                ≡⟨ cong (λ x  → comp ( hom h ) x )  f==g ⟩
-                    comp (hom h) (hom g)
-                ≡⟨ cong (λ x  → comp x ( hom g ) )  h==i ⟩
-                    comp (hom i) (hom g)
+                    comp (h) (f)
+                ≡⟨ cong (λ x  → comp ( h ) x )  f==g ⟩
+                    comp (h) (g)
+                ≡⟨ cong (λ x  → comp x ( g ) )  h==i ⟩
+                    comp (i) (g)
                 ≡⟨ refl ⟩
-                    hom ( i × g )
+                    ( i × g )
                 ∎
 
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  
-    (obj→ : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoHom  {c₁} {c₂} (obj→ a) (obj→ b) )  → Functor A A
-indexFunctor  {c₁} {c₂} {ℓ} A a b f g obj→ hom→ = record {
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} {c₂})  A
+indexFunctor  {c₁} {c₂} {ℓ} A a b f g = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
        ; isFunctor = record {
@@ -130,38 +126,57 @@
              ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
        }
       } where
-          fobj :  Obj A → Obj A
-          fobj x with obj→ x 
-          fobj x | t0 = a
-          fobj x | t1 = b
-          fmap :  {x y : Obj A } →  (Hom A x y  ) → Hom A (fobj x) (fobj y)
-          fmap  {x} {y} h with obj→ x | obj→ y | hom ( hom→ h )
-          fmap  h | t0 | t0 | id-t0 = id1 A a
-          fmap  h | t1 | t1 | id-t1 = id1 A b
-          fmap  h | t0 | t1 | arrow-f = f
-          fmap  h | t0 | t1 | arrow-g = g
-          ≈-cong :  {a : Obj A} {b : Obj A} {f g : Hom A a b}  → A [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
-          ≈-cong  {a} {b} {f} {g}  f≈g = {!!}
-          identity : (x : Obj A ) ->  A [ {!!} ≈ {!!} ] -- {!!} -- A [ fmap (id1 A x) ≈  id1 A (fobj x) ]
-          identity x with obj→ x 
-          identity x  | t0 =  let open ≈-Reasoning (A) in begin
-                 fmap (id1 A x)
-              ≈⟨ {!!} ⟩
-                 id1 A {!!}
-              ≈⟨⟩
-                 id1 A (fobj x )
-              ∎
-          identity _  | t1  =  let open ≈-Reasoning (A) in {!!}
-          distr1 : {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 ] ]
-          distr1  {a} {b} {c} {f} {g}  = {!!}
-          -- distr1  {a} {b} {c} {f} {g}  with   (obj→ a) | (obj→ b ) | ( obj→ c ) | (  hom→  f ) | (  hom→  g ) 
-          -- distr1  {a} {b} {c} {f} {g}  | _ | _ | _ | _ | _ = ?
-
-
-
-
-
+          T = TwoCat {c₁} {c₂} 
+          fobj :  Obj T → Obj A
+          fobj t0 = a
+          fobj t1 = b
+          fmap :  {x y : Obj T } →  (Hom T x y  ) → Hom A (fobj x) (fobj y)
+          fmap  {t0} {t0} id-t0 = id1 A a
+          fmap  {t1} {t1} id-t1 = id1 A b
+          fmap  {t0} {t1} arrow-f = f
+          fmap  {t0} {t1} arrow-g = g
+          ≈-cong :  {a : Obj T} {b : Obj T} {f g : Hom T a b}  → T [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
+          ≈-cong  {a} {b} {f} {.f} refl = let open  ≈-Reasoning A in refl-hom
+          identity : (x : Obj T ) ->  A [ fmap (id1 T x) ≈  id1 A (fobj x) ]
+          identity t0  = let open  ≈-Reasoning A in refl-hom
+          identity t1  = let open  ≈-Reasoning A in refl-hom
+          distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
+               A [ fmap (T [ g o f ])  ≈  A [ fmap g o fmap f ] ]
+          distr1  {a} {b} {c} {f} {g}  with f | g
+          distr1  {t0} {t0} {t0} {f} {g}  | id-t0 | id-t0 = let open  ≈-Reasoning A in sym-hom idL
+          distr1  {t1} {t1} {t1} {f} {g}  | id-t1 | id-t1 = let open  ≈-Reasoning A in begin 
+                   id1 A b 
+                ≈↑⟨ idL ⟩
+                   id1 A b o id1 A b
+                ∎
+          distr1  {t0} {t0} {t1} {f} {g}  | id-t0 | arrow-f = let open  ≈-Reasoning A in begin
+                  fmap (comp arrow-f id-t0)
+                ≈⟨⟩
+                  fmap arrow-f 
+                ≈↑⟨ idR ⟩
+                   fmap arrow-f o id1 A a
+                ∎
+          distr1  {t0} {t0} {t1} {f} {g}  | id-t0 | arrow-g = let open  ≈-Reasoning A in begin
+                  fmap (comp arrow-g id-t0)
+                ≈⟨⟩
+                  fmap arrow-g 
+                ≈↑⟨ idR ⟩
+                   fmap arrow-g o id1 A a
+                ∎
+          distr1  {t0} {t1} {t1} {f} {g}  | arrow-f | id-t1 = let open  ≈-Reasoning A in begin
+                  fmap (comp id-t1 arrow-f)
+                ≈⟨⟩
+                  fmap arrow-f 
+                ≈↑⟨ idL ⟩
+                   id1 A b o  fmap arrow-f 
+                ∎
+          distr1  {t0} {t1} {t1} {f} {g}  | arrow-g | id-t1 = let open  ≈-Reasoning A in begin
+                  fmap (comp id-t1 arrow-g)
+                ≈⟨⟩
+                  fmap arrow-g 
+                ≈↑⟨ idL ⟩
+                   id1 A b o  fmap arrow-g 
+                ∎
 
 ---  Equalizer
 ---                     f
@@ -187,33 +202,34 @@
 open Limit
 open NTrans
 
-equlimit : {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A I) -> 
-         Hom A ( limit-c comp ({!!} )) a
-equlimit A I f g comp = {!!}
+equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A (TwoCat {c₁} {c₂} )) -> 
+         Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a
+equlimit A f g comp = {!!}
 
-lim-to-equ :  {c₁ c₂ ℓ : Level} (A I : Category c₁ c₂ ℓ) 
-      (comp : Complete A I)
+lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+      (comp : Complete A (TwoCat {c₁} {c₂} ) )
         →  {a b : Obj A}      (f g : Hom A  a b )
-        → IsEqualizer A (equlimit A I f g comp ) f g
-lim-to-equ {c₁} {c₂} {ℓ} A I comp {a} {b} f g =  record {
-        fe=ge =  {!!}
+        → (fe=ge : A [ A [ f o (equlimit A  f g comp ) ] ≈ A [ g o (equlimit A  f g comp ) ] ] ) 
+        → IsEqualizer A (equlimit A  f g comp ) f g
+lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g 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
-         open  ≈-Reasoning A
+         I = TwoCat {c₁} {c₂}
          Γ : Functor I A
-         Γ = {!!} 
+         Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g
          eqlim = isLimit comp Γ
-         c = {!!}
-         e = {!!}
-         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  = {!!}
-         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 ]
+         c = limit-c comp Γ
+         e = equlimit A f g comp
+         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  = {!!}
+         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 = {!!} 
-         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
+         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
          uniq-nat  = {!!}
          uniquness :  (d : Obj A ) (h : Hom A d a ) →  ?　→ -- ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
                  ( k' : Hom A d c )
-                → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
+                → A [ A [ e o k' ] ≈ h ] → A [ k h {!!} ≈ k' ]
          uniquness = {!!}