Mercurial > hg > Members > kono > Proof > category

changeset 670:99065a1e56ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove comp from limit-to
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Oct 2017 18:14:41 +0900
parents 220ea177572f
children 959954fc29f8
files limit-to.agda
diffstat 1 files changed, 46 insertions(+), 48 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Mon Oct 30 17:49:58 2017 +0900
+++ b/limit-to.agda	Mon Oct 30 18:14:41 2017 +0900
@@ -10,7 +10,7 @@
 open import discrete
 
 
----  Equalizer  from Limit ( 2->A IdnexFunctor Γ and  IndexNat :  K ->　Γ)
+---  Equalizer  from Limit ( 2→A IdnexFunctor Γ and  IndexNat :  K →　Γ)
 ---
 ---
 ---                     f
@@ -37,7 +37,7 @@
 open IsLimit
 open NTrans
 
--- Functor Γ : TwoCat -> A
+-- 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₂} {ℓ} A a b f g = record {
@@ -51,6 +51,7 @@
       } where
           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
@@ -59,7 +60,7 @@
           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 : (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} →
@@ -101,7 +102,7 @@
 
 --- Nat for Limit
 --
---     Nat : K -> IndexFunctor
+--     Nat : K → IndexFunctor
 --
 
 open Functor
@@ -152,15 +153,15 @@
                 ∎
 
 
-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)) discrete.t0
+equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} → (f g : Hom A a b)  (lim : Limit A TwoCat (IndexFunctor A a b f g) ) →
+         Hom A (a0 lim) a
+equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) discrete.t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (comp : Complete A TwoCat  )
         →  {a b : Obj A}  (f g : Hom A  a b )
-        → IsEqualizer A (equlimit A f g comp) f g
-lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g =  record {
+       (lim : Limit A TwoCat (IndexFunctor A a b f g) )
+        → IsEqualizer A (equlimit A f g lim) f g
+lim-to-equ {c₁} {c₂} {ℓ} A {a} {b} f g lim =  record {
         fe=ge =  fe=ge0
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
@@ -170,25 +171,23 @@
          I = TwoCat
          Γ : Functor I A
          Γ = 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
+         e : Hom A (a0 lim) a
+         e = equlimit A f g lim
          c : Obj A
-         c = limit-c comp Γ
-         lim : Limit A I Γ 
-         lim =  climit comp  Γ
+         c = a0 lim
          inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
          inat = IndexNat A f g
-         fe=ge0 : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ]
+         fe=ge0 : A [ A [ f o (equlimit A f g lim ) ] ≈ A [ g o (equlimit A f g lim ) ] ]
          fe=ge0 = let open  ≈-Reasoning A in  begin
-                    f o (equlimit A f g comp)
+                    f o (equlimit A f g lim )
                 ≈⟨⟩
-                    FMap  Γ arrow-f o TMap (limit-u comp Γ) discrete.t0
-                ≈⟨  IsNTrans.commute ( isNTrans ( limit-u comp Γ )) {discrete.t0} {discrete.t1} {arrow-f} ⟩ 
-                    TMap (limit-u comp Γ) discrete.t1 o FMap (K A (TwoCat {c₁} {c₂} )(limit-c comp Γ)) id-t0
-                ≈↑⟨ IsNTrans.commute ( isNTrans ( limit-u comp Γ )) {discrete.t0} {discrete.t1} {arrow-g} ⟩ 
-                    FMap  Γ arrow-g o TMap (limit-u comp Γ) discrete.t0
+                    FMap  Γ arrow-f o TMap (Limit.t0 lim) discrete.t0
+                ≈⟨  IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-f} ⟩ 
+                    TMap (Limit.t0 lim) discrete.t1 o FMap (K A (TwoCat {c₁} {c₂} ) (a0 lim)) id-t0
+                ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-g} ⟩ 
+                    FMap  Γ arrow-g o TMap (Limit.t0 lim) discrete.t0
                 ≈⟨⟩
-                    g o (equlimit A f g comp)
+                    g o (equlimit A f g lim )
                 ∎
          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 (isLimit lim) d (inat d h fh=gh )
@@ -196,7 +195,7 @@
          ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
                     e o k h fh=gh
                 ≈⟨⟩
-                    TMap (limit-u comp Γ) discrete.t0  o k h fh=gh
+                    TMap (Limit.t0 lim) discrete.t0  o k h fh=gh
                 ≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {discrete.t0}  ⟩
                     TMap (inat d h fh=gh) discrete.t0
                 ≈⟨⟩
@@ -204,9 +203,9 @@
                 ∎
          uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c )
                        ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ]) → A [ A [ e o k' ] ≈ h ] →
-                       A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ]
+                       A [ A [ TMap (Limit.t0 lim) i o k' ] ≈ TMap (inat d h fh=gh) i ]
          uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
-                    TMap (limit-u comp Γ) discrete.t0 o k'
+                    TMap (Limit.t0 lim) discrete.t0 o k'
                 ≈⟨⟩
                     e o k'
                 ≈⟨ ek'=h ⟩
@@ -215,13 +214,13 @@
                     TMap (inat d h fh=gh) discrete.t0
                 ∎
          uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
-                    TMap (limit-u comp Γ) t1 o k'
+                    TMap (Limit.t0 lim) t1 o k'
                 ≈↑⟨ car (idR) ⟩
-                    ( TMap (limit-u comp Γ) t1  o  id c ) o k'
+                    ( TMap (Limit.t0 lim) t1  o  id c ) o k'
                 ≈⟨⟩
-                    ( TMap (limit-u comp Γ) t1  o  FMap (K A I c) arrow-f ) o k'
-                ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩
-                    ( FMap Γ  arrow-f  o TMap (limit-u comp Γ) discrete.t0 ) o k'
+                    ( TMap (Limit.t0 lim) t1  o  FMap (K A I c) arrow-f ) o k'
+                ≈↑⟨ car ( nat1 (Limit.t0 lim) arrow-f ) ⟩
+                    ( FMap Γ  arrow-f  o TMap (Limit.t0 lim) discrete.t0 ) o k'
                 ≈⟨⟩
                    (f o e ) o k'
                 ≈↑⟨ assoc ⟩
@@ -241,13 +240,13 @@
                 ∎
 
 
----  Product  from Limit ( given Discrete->A functor Γ and  pnat :  K ->　Γ)
+---  Product  from Limit ( given Discrete→A functor Γ and  pnat :  K →　Γ)
 
 open DiscreteHom
 
-plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set  c₁) (comp : Complete A ( DiscreteCat  S ) )  
-      →  ( Γ : Functor (DiscreteCat  S ) A ) → Obj A
-plimit A S comp Γ = limit-c comp Γ
+plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set  c₁) 
+      →  ( Γ : Functor (DiscreteCat  S ) A ) → (lim : Limit A ( DiscreteCat  S ) Γ )  → Obj A
+plimit A S Γ lim = a0 lim
 
 discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) →  (DiscreteCat S)  [ f  ≈  id1 (DiscreteCat S) a ]
 discrete-identity  f =   refl
@@ -278,13 +277,13 @@
                 ∎
 
 lim-to-product :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set  c₁ )
-      (comp : Complete A ( DiscreteCat S ) )
         →  ( Γ : Functor (DiscreteCat  S ) A )  
-        → IProduct  A (Obj ( DiscreteCat  S ) ) -- (plimit A S comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u  comp Γ) i )
-lim-to-product A S comp Γ = record {
+        → (lim : Limit A ( DiscreteCat S ) Γ )
+        → IProduct  A (Obj ( DiscreteCat  S ) ) 
+lim-to-product A S Γ lim = record {
           ai  = λ i → FObj Γ i
-          ; iprod = plimit A S comp Γ
-          ; pi =  λ  i →   TMap (limit-u  comp Γ) i 
+          ; iprod = plimit A S Γ lim
+          ; pi =  λ  i →   TMap (Limit.t0 lim) i 
           ; isIProduct =  record {
               iproduct = λ {q} qi → iproduct {q} qi ;
               pif=q =  λ {q } qi { i } → pif=q {q} qi {i}  ;
@@ -292,27 +291,26 @@
               ip-cong  =  λ {q } { qi }  { qi' } qi=qi' → ip-cong  {q} {qi} {qi'} qi=qi'
           }
    } where
-        D =  DiscreteCat   S
+        D = DiscreteCat S
         I = Obj ( DiscreteCat S )
-        lim = climit comp Γ
         ai = λ i → FObj Γ i
-        p = limit-c comp Γ
-        pi =  λ i → TMap (limit-u  comp Γ) i
+        p = a0 lim
+        pi =  λ i → TMap (Limit.t0 lim) i
         iproduct : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
         iproduct {q} qi = limit (isLimit lim) q (pnat A S Γ qi )
         pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( iproduct qi ) ] ≈  (qi i) ]
         pif=q {q} qi {i} = t0f=t (isLimit lim)  {q} {pnat A S Γ qi } {i}
-        ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ]
+        ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (Limit.t0 lim) i o h ] ≈ A [ pi i o h ] ]
         ipu {i} q h = let open  ≈-Reasoning A in  refl-hom
         ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
         ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i  o h ]  )} (ipu q h)
         ipc : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } 
              → (i : I ) →  A [ qi i ≈ qi' i ]  → 
-             A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
+             A [ A [ TMap (Limit.t0 lim) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
         ipc {q} {qi} {qi'} i qi=qi' = let open  ≈-Reasoning A in begin
-                  TMap (limit-u comp Γ) i o iproduct qi' 
+                  TMap (Limit.t0 lim) i o iproduct qi' 
                 ≈⟨⟩
-                  TMap (limit-u comp Γ) i o limit (isLimit lim) q (pnat A S Γ qi' )
+                  TMap (Limit.t0 lim) i o limit (isLimit lim) q (pnat A S Γ qi' )
                 ≈⟨ t0f=t (isLimit lim) {q} {pnat A S Γ qi'} {i} ⟩
                   TMap (pnat A S Γ qi') i
                 ≈⟨⟩