Mercurial > hg > Members > kono > Proof > category

changeset 267:b1b728559d89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constancy Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 17:26:47 +0900
parents 9e9f1e27e89f
children 2ff44ee3cb32
files CatExponetial.agda pullback.agda
diffstat 2 files changed, 64 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/CatExponetial.agda	Sun Sep 22 13:19:01 2013 +0900
+++ b/CatExponetial.agda	Sun Sep 22 17:26:47 2013 +0900
@@ -6,7 +6,9 @@
 
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
-module CatExponetial {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') where
+module CatExponetial where 
+
+--  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' }
 
 open import HomReasoning
 open import cat-utility
@@ -17,13 +19,13 @@
 
 open Functor
 
-CObj = Functor A B
-CHom = λ (f : CObj ) → λ (g : CObj ) → NTrans A B f g
+CObj = λ {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')  → Functor A B
+CHom = λ {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (f g : CObj A B )  → NTrans A B f g
 
 open NTrans 
-Cid : {a : CObj} → CHom a a
-Cid {a} = record { TMap = \x -> id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where
-   commute : {a : CObj} {a₁ b : Obj A} {f : Hom A a₁ b} →
+Cid : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) {a : CObj A B } → CHom A B a a
+Cid {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B {a} = record { TMap = \x -> id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where
+   commute : {a : CObj A B } {a₁ b : Obj A} {f : Hom A a₁ b} →
         B [ B [ FMap a f o id1 B (FObj a a₁) ] ≈
         B [ id1 B (FObj a b) o FMap a f ] ]
    commute {a} {a₁} {b} {f} = let open ≈-Reasoning B in begin
@@ -33,12 +35,13 @@
              ≈↑⟨ idL ⟩
                  id1 B (FObj a b) o FMap a f
              ∎
-   isNTrans1 : {a : CObj } → IsNTrans A B a a (\x -> id1 B (FObj a x))
+   isNTrans1 : {a : CObj A B } → IsNTrans A B a a (\x -> id1 B (FObj a x))
    isNTrans1 {a} = record { commute = \{a₁ b f} -> commute {a} {a₁} {b} {f} }
 
-_+_ : {a b c : CObj} → CHom b c → CHom a b → CHom a c
-_+_{a} {b} {c} f g  = record { TMap = λ x → B [ TMap f x o TMap g x ] ; isNTrans = isNTrans1  } where
-   commute1 :  (a b c : CObj ) (f : CHom  b c)  (g : CHom a b ) 
+_+_ :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' }  {a b c : CObj A B } 
+     → CHom A B b c → CHom A B a b → CHom A B a c
+_+_  {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {A} {B}  {a} {b} {c} f g  = record { TMap = λ x → B [ TMap f x o TMap g x ] ; isNTrans = isNTrans1  } where
+   commute1 :  (a b c : CObj A B ) (f : CHom  A B b c)  (g : CHom A B a b ) 
             (a₁ b₁ : Obj A) (h : Hom A a₁ b₁) →
                         B [ B [ FMap c h o B [ TMap f a₁ o TMap g a₁ ] ] ≈
                         B [ B [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
@@ -58,14 +61,15 @@
    isNTrans1 : IsNTrans A B a c (λ x → B [ TMap f x o TMap g x ]) 
    isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
 
-_==_  :  {a b : CObj} → CHom a b → CHom a b  → Set (ℓ' ⊔ c₁)
-_==_  {a} {b} f g =  ∀{x} → B [ TMap f x  ≈  TMap g x  ]
+_==_  :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' } {a b : CObj A B } → 
+    CHom A B a b → CHom A B a b  → Set (ℓ' ⊔ c₁)
+_==_  {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {A} {B} {a} {b} f g =  ∀{x} → B [ TMap f x  ≈  TMap g x  ]
 
 infix  4 _==_
 
 open import Relation.Binary.Core  
-isB^A :  IsCategory CObj CHom _==_ _+_ Cid
-isB^A  = 
+isB^A :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) → IsCategory (CObj A B) (CHom A B) _==_ _+_ (Cid A B)
+isB^A  {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B =
   record  { isEquivalence =  record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B )); 
                   sym = \{i j} → sym1 {_} {_} {i} {j} ;
                   trans = \{i j k} → trans1 {_} {_} {i} {j} {k} }  
@@ -74,13 +78,13 @@
         ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈1      {a} {b} {c} {f} {g} {h} {i}
         ; associative = IsCategory.associative ( Category.isCategory B )
         } where
-            sym1 : {a b : CObj } {i j : CHom a b } → i == j → j == i
+            sym1 : {a b : CObj A B } {i j : CHom A B a b } → i == j → j == i
             sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning B in begin
                  TMap j x
              ≈⟨ sym eq ⟩
                  TMap i x
              ∎ 
-            trans1 : {a b : CObj } {i j k : CHom a b} → i == j → j == k → i == k
+            trans1 : {a b : CObj A B } {i j k : CHom A B a b} → i == j → j == k → i == k
             trans1 {a} {b} {i} {j} {k} i=j j=k {x} =  let open ≈-Reasoning B in begin
                  TMap i x
              ≈⟨ i=j ⟩
@@ -88,7 +92,7 @@
              ≈⟨ j=k ⟩
                  TMap k x
              ∎
-            o-resp-≈1 : {a b c : CObj} {f g : CHom a b} {h i : CHom b c } → 
+            o-resp-≈1 : {a b c : CObj A B } {f g : CHom A B a b} {h i : CHom A B b c } → 
                 f == g → h == i → h + f == i + g
             o-resp-≈1 {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning B in begin
                  TMap h x  o TMap f x
@@ -96,13 +100,16 @@
                  TMap i x  o TMap g x
              ∎
 
-B^A : Category (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁))))) (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁)))))   (ℓ' ⊔ c₁)
-B^A =
-  record { Obj = CObj
-         ; Hom = CHom
+_^_ :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level}  (A : Category c₁' c₂' ℓ' ) (B : Category c₁ c₂ ℓ) →  
+     Category (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁))))) 
+              (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ (suc ℓ ⊔ (suc c₂ ⊔ suc c₁)))))   
+              (ℓ' ⊔ c₁)
+_^_ {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} B A =
+  record { Obj = CObj A B
+         ; Hom = CHom A B
          ; _o_ = _+_
          ; _≈_ = _==_
-         ; Id  = Cid
-         ; isCategory = isB^A
+         ; Id  = Cid A B
+         ; isCategory = isB^A A B
          }
 
--- a/pullback.agda	Sun Sep 22 13:19:01 2013 +0900
+++ b/pullback.agda	Sun Sep 22 17:26:47 2013 +0900
@@ -196,15 +196,41 @@
       ∎
 
 
-open import CatExponetial I A
+open import CatExponetial 
+
+open Functor
+
+--------------------------------
+--
+-- Contancy Functor
 
-KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A
-KI I Γ a = record {
-      FObj = λ i → a ;
-      FMap = λ f → id1 A a ;
+KI :  Functor A ( A ^ I )
+KI  = record {
+      FObj = λ a → K I a ;
+      FMap = λ f → record { --  NTrans I A (K I a)  (K I b)
+            TMap = λ a → f ;
+            isNTrans = record { 
+                 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
+            }
+        }  ; 
         isFunctor = let  open ≈-Reasoning (A) in record {
-               ≈-cong   = λ f=g → refl-hom
+               ≈-cong   = λ f=g {x} → f=g
              ; identity = refl-hom
-             ; distr    = sym idL
+             ; distr    = refl-hom
         }
-  }
+  } where
+     commute1 :  {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
+        A [ A [ FMap (K I b') f₁ o f ] ≈ A [ f o FMap (K I a') f₁ ] ]
+     commute1 {a} {b} {f₁} {a'} {b'} f = let  open ≈-Reasoning (A) in begin 
+            FMap (K I b') f₁ o f 
+        ≈⟨ idL ⟩
+           f
+        ≈↑⟨ idR ⟩
+            f o FMap (K I a') f₁ 
+        ∎
+
+
+--limit2adjoint : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+--     ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) 
+--       ( lim : Limit I Γ a0 t0 ) → 
+