Mercurial > hg > Members > kono > Proof > category

changeset 592:0448a74c0a03

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 May 2017 18:09:33 +0900
parents 9676a75c3010
children a158ebb391f2
files SetsCompleteness.agda
diffstat 1 files changed, 52 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun May 14 16:46:54 2017 +0900
+++ b/SetsCompleteness.agda	Mon May 15 18:09:33 2017 +0900
@@ -161,7 +161,6 @@
      hom→ : {i j : Obj C } →    Hom C i j →  I → I 
      hom← : {i j : Obj C } →  ( f : I → I  ) →  Hom C i j 
      hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f 
-     iso-hom : {i j : Obj C } →  { f : I → I } →   hom→ ( hom← {i} {j} f )  ≡ f 
      -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
 open Small 
@@ -211,20 +210,65 @@
 
 
 lldistr :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
-    →  (a b : Obj C) (f g : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
+    →  (a b c : Obj C) (f g : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
     → ( x : FObj Γ a )
-    → slmap se ( λ y → f ( g y )) x ≡ slmap se f ( ( slmap se g ) x )
-lldistr C I s Γ a b f g se x =  {!!}
+    → slmap se {a} {c} ( λ y → f ( g y )) x ≡ slmap se {b} {c} f ( ( slmap se {a} {b} g ) x )
+lldistr C I s Γ a b c f g se x =   begin
+          slmap se {a} {c} ( λ y → f ( g y )) x
+       ≡⟨⟩
+           FMap Γ (hom← s (λ y → f (g y)))  x
+       ≡⟨ ?  ⟩
+           FMap Γ (hom← s (λ y → f ( hom→ s ( hom← s  g) y )))  x
+       ≡⟨ {!!} ⟩
+           FMap Γ  (C [ hom← s f o hom← s g ]) x
+       ≡⟨  ≡cong ( λ g →  g x ) ( IsFunctor.distr (isFunctor  Γ ) )  ⟩
+           (Sets [ FMap Γ (hom← s f) o FMap Γ (hom← s g ) ]) x
+       ≡⟨⟩
+          slmap se {b} {c} f ( ( slmap se {a} {b} g ) x )
+       ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+
+lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
+    {i j i' j' : Obj C } →　 { f f' : I → I }
+    →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
+    →  proj (equ (slequ se i j f)) i ≡ proj (equ (slequ se i' j' f' )) i
+lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se =   ≡cong ( λ p -> proj p i ) ( begin
+                 equ (slequ se i j f )
+             ≡⟨⟩
+                 record { proj = λ x → proj (equ (slequ se i j f)) x }
+             ≡⟨ ≡cong ( λ p → record { proj =  proj p i })  (  ≡cong ( λ QIX → record { proj = QIX } ) (
+                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  ) refl
+              ) )) ⟩
+                 record { proj = λ x → proj (equ (slequ se i' j' f')) x }
+             ≡⟨⟩
+                 equ (slequ  se i' j' f' )
+             ∎  ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+llcomm :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+    →  (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
+    → proj ( equ ( slequ se a b f)) a ≡  slmap se f (proj (slprod C I s Γ {a} se ) a )
+llcomm C I s Γ a b f se  =  begin
+          proj ( equ ( slequ se a b f)) a
+       ≡⟨ {!!} ⟩
+          slmap se f (proj (equ ( slequ se a a (slid C I s a))) a )
+       ≡⟨⟩
+          slmap se f (proj (slprod C I s Γ {a} se ) a )
+       ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
 
 lla :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
     →  (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
     → proj ( equ ( slequ se a b f)) a ≡ proj (slprod C I s Γ {a} se ) a 
 lla C I s Γ a b f se = begin
           proj ( equ ( slequ se a b f)) a 
-       ≡⟨ fe=ge0 {!!} ⟩
+       ≡⟨ {!!} ⟩
           proj ( equ ( slequ se a a (slid C I s a))) a 
-       ≡⟨⟩
-          proj (slprod C I s Γ {a} se ) a
        ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -239,8 +283,7 @@
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
     → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
 Cone {c₁} C I s  Γ =  record {
-               TMap = λ i →  λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s  Γ)}  {FObj Γ i}
-                     {λ x → proj x i} {λ x → proj x i} (elem  (slprod C I s Γ {i} se ) refl )) i
+               TMap = λ i →  λ se → proj (slprod C I s Γ {i} se ) i
              ; isNTrans = record { commute = commute1 }
       } where
          commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj  (slprod C I s Γ {a} se ) a) ]