Mercurial > hg > Members > kono > Proof > category

changeset 461:8436a018f88a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Mar 2017 10:43:17 +0900
parents 961c236807f1
children e618db534987
files discrete.agda limit-to.agda
diffstat 2 files changed, 33 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Fri Mar 03 12:12:06 2017 +0900
+++ b/discrete.agda	Sat Mar 04 10:43:17 2017 +0900
@@ -27,20 +27,16 @@
    arrow-g :  TwoHom t0 t1
 
 
-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 
-comp {_}  {_}  {t0} {t0} {t1}  arrow-f   id-t0    =   arrow-f 
-comp {_}  {_}  {t0} {t0} {t1}  arrow-g   id-t0    =   arrow-g 
-comp {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    =   id-t0 
+_×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  TwoHom {c₁} {c₂} b c  →  TwoHom {c₁} {c₂} a b   →  TwoHom {c₁} {c₂} a c 
+_×_ {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f   =   arrow-f 
+_×_ {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  =   arrow-g 
+_×_ {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    =   id-t1 
+_×_ {_}  {_}  {t0} {t0} {t1}  arrow-f   id-t0    =   arrow-f 
+_×_ {_}  {_}  {t0} {t0} {t1}  arrow-g   id-t0    =   arrow-g 
+_×_ {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    =   id-t0 
 
 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  =  comp  {c₁}  {c₂}  {a} {b} {c} f g
-
-
 --          f    g    h
 --       d <- c <- b <- a
 --
@@ -48,8 +44,8 @@
 
 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 )} →
+       {g : (TwoHom b c )} →
+       {h : (TwoHom a b )} →
        ( f × (g × h)) ≡ ((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
@@ -68,11 +64,11 @@
 
 TwoCat : {c₁ c₂ : Level  } →  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} = record {
-    Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →    ( TwoHom {c₁}  {c₂ } a b ) ;
+    Obj  = TwoObject ;
+    Hom = λ a b →   TwoHom a b  ;
     _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
     _≈_ =  λ x y → x  ≡ y ;
-    Id  =  λ{a} → TwoId {c₁ } { c₂} a ;
+    Id  =  λ{a} → TwoId a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
             identityL  = λ{a b f} → identityL {c₁}  {c₂ } {a} {b} {f} ;
@@ -93,16 +89,4 @@
         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)} →
             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
-                    ( h × f )
-                ≡⟨ refl ⟩
-                    comp (h) (f)
-                ≡⟨ cong (λ x  → comp ( h ) x )  f==g ⟩
-                    comp (h) (g)
-                ≡⟨ cong (λ x  → comp x ( g ) )  h==i ⟩
-                    comp (i) (g)
-                ≡⟨ refl ⟩
-                    ( i × g )
-                ∎
-
+        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
--- a/limit-to.agda	Fri Mar 03 12:12:06 2017 +0900
+++ b/limit-to.agda	Sat Mar 04 10:43:17 2017 +0900
@@ -38,7 +38,7 @@
 
 -- Functor Γ : TwoCat -> A
 
-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₂ ℓ : 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
@@ -48,7 +48,7 @@
              ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
        }
       } where
-          T = TwoCat {c₁} {c₂}
+          T = TwoCat   {c₁} {c₂}
           fobj :  Obj T → Obj A
           fobj t0 = a
           fobj t1 = b
@@ -109,14 +109,14 @@
 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
         →  {a b : Obj A}      (f g : Hom A  a b )
     (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → 
-        NTrans (TwoCat {c₁} {c₂}) A (K A (TwoCat {c₁} {c₂}) d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
+        NTrans TwoCat  A (K A TwoCat  d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
 IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
     TMap = λ x → nmap x d h ;
     isNTrans = record {
         commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh 
     }
  } where
-         I = TwoCat {c₁} {c₂}
+         I = TwoCat  {c₁} {c₂}
          Γ : Functor I A
          Γ = IndexFunctor {c₁} {c₂} {ℓ} 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)
@@ -152,12 +152,12 @@
                 ∎
 
 
-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 {c₁} {c₂} {ℓ} A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0
+equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A TwoCat ) -> 
+         Hom A ( limit-c comp (IndexFunctor A a b f g)) a
+equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (comp : Complete A (TwoCat {c₁} {c₂} ) )
+      (comp : Complete A TwoCat  )
         →  {a b : Obj A}  (f g : Hom A  a b ) 
         → (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
@@ -167,22 +167,28 @@
         ; 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
-         I = TwoCat {c₁} {c₂}
+         I : Category  c₁ c₂ c₂ 
+         I = TwoCat 
          Γ : Functor I A
-         Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
+         Γ = IndexFunctor A a b f g
+         e : Hom A (limit-c comp (IndexFunctor A a b f g)) a
          e = equlimit A f g comp
+         c : Obj A 
          c = limit-c comp Γ
+         natL : NTrans I A (K A I c) Γ
          natL = limit-u comp Γ
-         eqlim =  isLimit comp  Γ 
+         lim : Limit A I Γ c natL
+         lim =  isLimit comp  Γ 
+         nat0 : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
          nat0 = IndexNat A f g 
          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 eqlim d (nat0 d h fh=gh )
+         k {d} h fh=gh  =  limit lim d (nat0 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 = let open  ≈-Reasoning A in  begin
                     e o k h fh=gh
                 ≈⟨⟩
                     TMap (limit-u comp Γ) t0  o k h fh=gh
-                ≈⟨ t0f=t eqlim {d} {nat0 d h fh=gh } {t0}  ⟩
+                ≈⟨ t0f=t lim {d} {nat0 d h fh=gh } {t0}  ⟩
                     TMap (nat0 d h fh=gh) t0
                 ≈⟨⟩
                     h
@@ -221,7 +227,7 @@
                 → A [ A [ e o k' ] ≈ h ] → A [ k h  fh=gh   ≈ k' ]
          uniquness d h fh=gh k' ek'=h =  let open  ≈-Reasoning A in  begin
                     k h fh=gh
-                ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
+                ≈⟨ limit-uniqueness lim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
                     k'
                 ∎