Mercurial > hg > Members > kono > Proof > category

changeset 312:702adc45704f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is this right direction?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jan 2014 23:37:12 +0900
parents cf278f4d0b32
children d72730946ba5
files cat-utility.agda freyd.agda pullback.agda
diffstat 3 files changed, 60 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sun Jan 05 19:34:11 2014 +0900
+++ b/cat-utility.agda	Sun Jan 05 23:37:12 2014 +0900
@@ -231,3 +231,37 @@
            pi1  = π1 
            pi2 : Hom A ab b 
            pi2  = π2 
+
+        --
+        -- Limit
+        --
+        -----
+
+        -- Constancy Functor
+
+        K : { c₁' c₂' ℓ' : Level}  (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) 
+            → ( a : Obj A ) → Functor I A
+        K A I a = record {
+              FObj = λ i → a ;
+              FMap = λ f → id1 A a ;
+                isFunctor = let  open ≈-Reasoning (A) in record {
+                       ≈-cong   = λ f=g → refl-hom
+                     ; identity = refl-hom
+                     ; distr    = sym idL
+                }
+          }
+
+
+        record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+             ( a0 : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+          field
+             limit :  ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
+             t0f=t :  { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
+                 A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
+             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
+                 A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
+          A0 : Obj A
+          A0 = a0
+          T0 : NTrans I A ( K A I a0 ) Γ
+          T0 = t0
+
--- a/freyd.agda	Sun Jan 05 19:34:11 2014 +0900
+++ b/freyd.agda	Sun Jan 05 23:37:12 2014 +0900
@@ -1,11 +1,11 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
-open import Category.Sets
 
 module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
   where
 
 open import cat-utility
+open import HomReasoning
 open import Relation.Binary.Core
 open Functor
 
@@ -39,12 +39,30 @@
 
 -- A has initial object if it has PreInitial-SmallFullSubcategory
 
+open NTrans
+open Limit
+
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
-      -- ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) -- completeness
+      (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
       (SFS : SmallFullSubcategory A F FMap← ) → 
-      (PreInitial A F ) → { i : Obj A } → HasInitialObject A i
-initialFromPreInitialFullSubcategory A F  FMap← SFS PI {i} = record {
-      initial = {!!} ; 
-      uniqueness  = {!!}
-    }
+      (PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
+          → HasInitialObject A a0
+initialFromPreInitialFullSubcategory A F  FMap← lim SFS PI {a0} {u} = record {
+      initial = λ a → limit (lim F {a} {u a} ) a0 (u a0) ; 
+      uniqueness  = λ a f → lemma1 a f
+    } where
+      lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ limit (lim F) a0 (u a0) ]
+      lemma1 a f = let open ≈-Reasoning (A) in 
+             begin
+                 f
+             ≈↑⟨ limit-uniqueness (lim F) ( λ {i} →
+             begin
+                  TMap (u a) i o f 
+             ≈⟨ ? ⟩
+                  TMap (u a0) i
+             ∎ 
+             )⟩
+                 limit (lim F) a0 (u a0)
+             ∎ 
+
--- a/pullback.agda	Sun Jan 05 19:34:11 2014 +0900
+++ b/pullback.agda	Sun Jan 05 23:37:12 2014 +0900
@@ -128,46 +128,12 @@
                  p'
              ∎
 
-------
---
--- Limit
---
------
-
--- Constancy Functor
-
-K : { c₁' c₂' ℓ' : Level}  (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) 
-    → ( a : Obj A ) → Functor I A
-K A I a = record {
-      FObj = λ i → a ;
-      FMap = λ f → id1 A a ;
-        isFunctor = let  open ≈-Reasoning (A) in record {
-               ≈-cong   = λ f=g → refl-hom
-             ; identity = refl-hom
-             ; distr    = sym idL
-        }
-  }
-
-open NTrans
-
-record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-     ( a0 : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
-  field
-     limit :  ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
-     t0f=t :  { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
-         A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
-     limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
-         A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
-  A0 : Obj A
-  A0 = a0
-  T0 : NTrans I A ( K A I a0 ) Γ
-  T0 = t0
-
 --------------------------------
 --
 -- If we have two limits on c and c', there are isomorphic pair h, h'
 
 open Limit
+open NTrans
 
 iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
      ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) (  t0' : NTrans I A ( K A I a0' ) Γ )