Mercurial > hg > Members > kono > Proof > category

changeset 460:961c236807f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit-to done discrete done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Mar 2017 12:12:06 +0900
parents 9d24fb809746
children 8436a018f88a
files HomReasoning.agda cat-utility.agda freyd.agda limit-to.agda
diffstat 4 files changed, 40 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Mar 02 20:22:42 2017 +0900
+++ b/HomReasoning.agda	Fri Mar 03 12:12:06 2017 +0900
@@ -124,6 +124,12 @@
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
   nat η  =  IsNTrans.commute ( isNTrans η  )
 
+  nat1 : { c₁ c₂ ℓ : Level}  {A : Category c₁ c₂ ℓ}  { c₁′ c₂′ ℓ′ : Level}  {D : Category c₁′ c₂′ ℓ′} 
+         {a b : Obj D}   {F G : Functor D A }
+      →  (η : NTrans D A F G ) → (f : Hom D a b)
+      →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
+  nat1 η f =  IsNTrans.commute ( isNTrans η  )
+
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
   infixr 2 _≈↑⟨_⟩_ 
--- a/cat-utility.agda	Thu Mar 02 20:22:42 2017 +0900
+++ b/cat-utility.agda	Fri Mar 03 12:12:06 2017 +0900
@@ -286,13 +286,15 @@
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
              limit-c :  ( Γ : Functor I A ) -> Obj A 
-             isLimit :  ( Γ : Functor I A ) -> (limit-u : NTrans I A ( K A I (limit-c Γ) ) Γ ) -> Limit A I Γ (limit-c Γ) limit-u
+             limit-u :  ( Γ : Functor I A ) ->  NTrans I A ( K A I (limit-c Γ )) Γ
+             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
 
         record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
              limit-c :  ( Γ : Functor I A ) -> Obj A 
-             isLimit :  ( Γ : Functor I A ) -> (limit-u : NTrans I A ( K A I (limit-c Γ) ) Γ) -> Limit A I Γ (limit-c Γ) limit-u 
+             limit-u :  ( Γ : Functor I A )  → NTrans I A ( K A I (limit-c Γ )) Γ
+             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
 
              product : (a b : Obj A) -> Obj A
              π1 : (a b : Obj A) -> Hom A (product a b ) a 
--- a/freyd.agda	Thu Mar 02 20:22:42 2017 +0900
+++ b/freyd.agda	Fri Mar 03 12:12:06 2017 +0900
@@ -60,10 +60,8 @@
       FMap←  = SFSFMap←  SFS
       a0 : Obj A
       a0 = limit-c comp F
-      uΓ : ( Γ : Functor A A ) →  NTrans A A (K A A (limit-c comp Γ)) Γ
-      uΓ Γ = {!!}
-      lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (uΓ Γ)
-      lim Γ =  isLimit comp Γ (uΓ Γ)
+      lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ)
+      lim Γ =  isLimit comp Γ 
       u : NTrans A A (K A A a0) F
       u = T0 ( lim F )
       equ : {a b : Obj A} → (f g : Hom A a b)  → IsEqualizer A (equalizer-e comp f g ) f g
--- a/limit-to.agda	Thu Mar 02 20:22:42 2017 +0900
+++ b/limit-to.agda	Fri Mar 03 12:12:06 2017 +0900
@@ -107,11 +107,10 @@
 open Functor
 
 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (comp : Complete A (TwoCat {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)
-IndexNat {c₁} {c₂} {ℓ} A comp {a} {b} f g d h fh=gh = record {
+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 
@@ -153,12 +152,16 @@
                 ∎
 
 
+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
+
 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 ) {e : Hom A (limit-c comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) a }
-        → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) 
-        → IsEqualizer A e f g
-lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g {e} fe=ge =  record {
+        →  {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
+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
@@ -167,31 +170,43 @@
          I = TwoCat {c₁} {c₂}
          Γ : Functor I A
          Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
+         e = equlimit A f g comp
          c = limit-c comp Γ
+         natL = limit-u comp Γ
+         eqlim =  isLimit comp  Γ 
+         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
-         nat0 = IndexNat A comp f g 
-         eqlim =  isLimit comp  Γ (nat0 c e fe=ge )
          k {d} h fh=gh  =  limit eqlim 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
-                ≈⟨ t0f=t eqlim {d} {nat0 d h fh=gh} {t0}  ⟩
+                ≈⟨⟩
+                    TMap (limit-u comp Γ) t0  o k h fh=gh
+                ≈⟨ t0f=t eqlim {d} {nat0 d h fh=gh } {t0}  ⟩
+                    TMap (nat0 d h fh=gh) t0
+                ≈⟨⟩
                     h
                 ∎
          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 (nat0 c e fe=ge ) i o k' ] ≈ TMap (nat0 d h fh=gh) i ]
+                       A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (nat0 d h fh=gh) i ]
          uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
-                    TMap (nat0 c e fe=ge ) t0 o k'
+                    TMap (limit-u comp Γ) t0 o k'
                 ≈⟨⟩
                     e o k'
                 ≈⟨ ek'=h ⟩
                     h
                 ≈⟨⟩
-                     TMap (nat0 d h fh=gh) t0  
+                    TMap (nat0 d h fh=gh) t0
                 ∎
          uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
-                    TMap (nat0 c e fe=ge ) t1 o k'
+                    TMap (limit-u comp Γ) t1 o k'
+                ≈↑⟨ car (idR) ⟩
+                    ( TMap (limit-u comp Γ) t1  o  id1 A 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 Γ) t0 ) o k'
                 ≈⟨⟩
                    (f o e ) o k'
                 ≈↑⟨ assoc ⟩