Mercurial > hg > Members > kono > Proof > category

changeset 611:b1b5c6b4c570

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
natural transformation in representable functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 12 Jun 2017 23:25:39 +0900
parents 3fb4d834c349
children f924056bf08a
files freyd2.agda
diffstat 1 files changed, 38 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Mon Jun 12 18:11:23 2017 +0900
+++ b/freyd2.agda	Mon Jun 12 23:25:39 2017 +0900
@@ -1,6 +1,6 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
-open import Category.Sets
+open import Category.Sets renaming ( _o_ to _*_ )
 
 module freyd2 
    where
@@ -29,7 +29,7 @@
 
 open Small
 
-postulate ≈-≡ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
+postulate ≈-≡ :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
@@ -49,7 +49,7 @@
 open import Category.Cat
 
 HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
-HomA  {c₁} {c₂} {ℓ} A  a = record {
+HomA  {c₁} {c₂} {ℓ} A a = record {
     FObj = λ b → Hom A a b
   ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
   ; isFunctor = record {
@@ -59,10 +59,10 @@
         } 
     }  where
         lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) →  A [ id1 A b o x ] ≡ x
-        lemma-y-obj1 {b} x = let open ≈-Reasoning A  in ≈-≡ {_} {_} {_} {A} idL
+        lemma-y-obj1 {b} x = let open ≈-Reasoning A  in ≈-≡ A idL
         lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ 
                A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
-        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A} ( begin
+        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin
                A [ A [ g o f ] o x ]
              ≈↑⟨ assoc ⟩
                A [ g o A [ f o x ] ]
@@ -70,7 +70,7 @@
                ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
              ∎ )
         lemma-y-obj3 :  {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] →   A [ f o x ] ≡ A [ g o x ]
-        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning A in ≈-≡ {_} {_} {_} {A}   ( begin
+        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning A in ≈-≡ A ( begin
                 A [ f o x ]
              ≈⟨ resp refl-hom eq ⟩
                 A [ g o x ]
@@ -117,16 +117,40 @@
       (comp : Complete A A) (b : Obj A ) 
       (Γ : Functor I A) (limita : Limit A I Γ) →
         IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b))
-UpreserveLimit0 A I comp b Γ lim = record {
-         limit = λ a t → limit1 a t
-       ; t0f=t = λ {a t i} → {!!}
+UpreserveLimit0 {c₁} {c₂} {ℓ} A I comp b Γ lim = record {
+         limit = λ a t → ψ a t
+       ; t0f=t = λ {a t i} → t0f=t0 a t i
        ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!}
     } where 
-      ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) → NTrans I A (K A I {!!}) Γ
-      ta a t = {!!}
-      limit1 :  (a : Obj Sets)  ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ))
-          →  Hom Sets a (FObj (HomA A b) (a0 lim))
-      limit1 a t = Sets [ FMap (HomA A b) (limit (isLimit lim) (FObj {!!} b) (ta a t )) o TMap {!!} b ]
+      hat0 :  NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ)
+      hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)
+      haa0 : Obj Sets
+      haa0 = FObj (HomA A b) (a0 lim)
+      ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) → NTrans I A (K A I b ) Γ
+      ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where
+         commute1 :  {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} →
+                A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ]  ]
+         commute1  {a₁} {b₁} {f} = let open ≈-Reasoning A in begin
+                 FMap Γ f o TMap t a₁ x
+             ≈⟨⟩
+                 ( ( FMap (HomA A b  ○ Γ ) f )  *  TMap t a₁ ) x
+             ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
+                 ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x
+             ≈⟨⟩
+                 ( TMap t b₁ * id1 Sets a ) x
+             ≈⟨⟩
+                 TMap t b₁ x 
+             ≈↑⟨ idR ⟩
+                 TMap t b₁ x o id1 A b
+             ≈⟨⟩
+                 TMap t b₁ x o FMap (K A I b) f 
+             ∎ 
+      ψ  :  (X : Obj Sets)  ( t : NTrans I Sets (K Sets I X) (HomA A b ○ Γ))
+          →  Hom Sets X (FObj (HomA A b) (a0 lim))
+      ψ X t x = FMap (HomA A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
+      t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I)
+           → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ]
+      t0f=t0 = {!!}
 
 
 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)