Mercurial > hg > Members > kono > Proof > category

changeset 265:367e8fde93ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 11:08:41 +0900
parents 78ce12f8e6b6
children 9e9f1e27e89f
files cat-utility.agda pullback.agda
diffstat 2 files changed, 30 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Fri Sep 20 21:21:48 2013 +0900
+++ b/cat-utility.agda	Sun Sep 22 11:08:41 2013 +0900
@@ -172,8 +172,11 @@
               ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] 
            axb : Obj A
            axb = ab
+           pi1 : Hom A ab a 
+           pi1  = π1 
+           pi2 : Hom A ab b 
+           pi2  = π2 
 
-        -- 
         -- Pullback
         --         f
         --     a -------> c
@@ -202,3 +205,7 @@
                      →  A [ p eq  ≈ p' ]
            axb : Obj A
            axb = ab
+           pi1 : Hom A ab a 
+           pi1  = π1 
+           pi2 : Hom A ab b 
+           pi2  = π2 
--- a/pullback.agda	Fri Sep 20 21:21:48 2013 +0900
+++ b/pullback.agda	Sun Sep 22 11:08:41 2013 +0900
@@ -126,3 +126,25 @@
                  p'
              ∎
 
+K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A
+K 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} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 
+     ( a0 : Obj A ) (  t0 : NTrans I A ( K I Γ a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+  field
+     limit :  ( a : Obj A ) → ( t : NTrans I A ( K I Γ a ) Γ ) → Hom A a a0
+     t0f=t :  { a : Obj A } → { t : NTrans I A ( K 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 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 ]
+