Mercurial > hg > Members > kono > Proof > category

changeset 456:4d97955ea419

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit with nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 17:41:20 +0900
parents 55a9b6177ed4
children 0ba86e29f492
files cat-utility.agda discrete.agda
diffstat 2 files changed, 82 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Thu Mar 02 14:58:40 2017 +0900
+++ b/cat-utility.agda	Thu Mar 02 17:41:20 2017 +0900
@@ -286,15 +286,13 @@
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
              limit-c :  ( Γ : Functor I A ) -> Obj A 
-             limit-u :  ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ) ) Γ 
-             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
+             isLimit :  ( Γ : Functor I A ) -> (limit-u : NTrans I A ( K A I (limit-c Γ) ) Γ ) -> 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 
-             limit-u :  ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ) ) Γ 
-             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
+             isLimit :  ( Γ : Functor I A ) -> (limit-u : NTrans I A ( K A I (limit-c Γ) ) Γ) -> 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/discrete.agda	Thu Mar 02 14:58:40 2017 +0900
+++ b/discrete.agda	Thu Mar 02 17:41:20 2017 +0900
@@ -204,7 +204,7 @@
 
 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 = {!!}
+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₂} ) )
@@ -220,16 +220,86 @@
          I = TwoCat {c₁} {c₂}
          Γ : Functor I A
          Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g
-         eqlim = isLimit comp Γ
          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  = {!!}
+         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 x 
+         ... | t0 = h
+         ... | t1 = A [ f o  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 f'
+         commute1  {t0} {t1} {f'}  d h fh=gh | arrow-f =  let open  ≈-Reasoning A in begin
+                    f o h
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
+                ∎
+         commute1  {t0} {t1} {f'}  d h fh=gh | arrow-g =  let open  ≈-Reasoning A in begin
+                    g o h
+                ≈↑⟨ fh=gh ⟩
+                    f o h
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
+                ∎
+         commute1  {t0} {t0} {f'}  d h fh=gh | id-t0 =   let open  ≈-Reasoning A in begin
+                    id1 A a o h
+                ≈⟨ idL ⟩
+                    h
+                ≈↑⟨ idR ⟩
+                    h o id1 A d
+                ∎
+         commute1  {t1} {t1} {f'}  d h fh=gh | id-t1 =   let open  ≈-Reasoning A in begin
+                    id1 A b o  ( f o  h  )
+                ≈⟨ idL ⟩
+                     f o  h
+                ≈↑⟨ idR ⟩
+                    ( f o  h ) o id1 A d 
+                ∎
+         nat1 : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
+         nat1 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 
+            }
+          }
+         e =  equlimit A f g comp
+         eqlim =  isLimit comp  Γ (nat1 c e fe=ge )
+         k {d} h fh=gh  =  limit eqlim d (nat1 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  = {!!}
-         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ?　→ -- ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
+         ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
+                    e o k h fh=gh
+                ≈⟨ t0f=t eqlim {d} {nat1 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 (nat1 c e fe=ge ) i o k' ] ≈ TMap (nat1 d h fh=gh) i ]
+         uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
+                    (nmap t0 c e ) o k'
+                ≈⟨⟩
+                    e o k'
+                ≈⟨ ek'=h ⟩
+                    h
+                ≈⟨⟩
+                    nmap t0 d h
+                ∎
+         uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
+                   (nmap t1 c e ) o k'
+                ≈⟨⟩
+                   (f o e ) o k'
+                ≈↑⟨ assoc ⟩
+                   f o ( e o k' )
+                ≈⟨ cdr  ek'=h ⟩
+                    f o h
+                ≈⟨⟩
+                    TMap (nat1 d h fh=gh) t1
+                ∎
+         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 {!!} ≈ k' ]
-         uniquness = {!!}
+                → 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 ) ⟩
+                    k'
+                ∎
+