Mercurial > hg > Members > kono > Proof > category

changeset 590:2c5d8c3c9086

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 Sun, 14 May 2017 13:53:26 +0900
parents 6584db867bd0
children 9676a75c3010
files SetsCompleteness.agda
diffstat 1 files changed, 55 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun May 14 09:55:10 2017 +0900
+++ b/SetsCompleteness.agda	Sun May 14 13:53:26 2017 +0900
@@ -161,6 +161,7 @@
      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 
@@ -183,25 +184,64 @@
        slequ : (i j : OC) (f :  I → I  ) → sequ (sproduct OC sobj) (sobj j) (λ x →  smap f (proj x i) ) (λ x → proj x j )
    slprod :  {i : OC } → sproduct OC  sobj 
    slprod {i} = equ ( slequ i i slid )
+   slmap  :  { i j :  OC  }  → (f : I → I ) → sobj i → sobj j
+   slmap f x = smap f x
 
 open slim
 
 open import HomReasoning
 open NTrans
 
-cone-equ :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+llid :  {  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 Γ)  ) 
-    → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x →  FMap Γ (hom← s f) (proj (slprod x {a}) a) ) (λ x → proj (slprod x {b}) b )
-cone-equ C I s Γ a b f se = elem se {!!} -- (( fe=ge0 (slequ se  a b f  )) )
+    → ( x : FObj Γ a )
+    → slmap se slid x ≡ x
+llid C I s Γ a b f se x = begin
+        slmap se slid x 
+       ≡⟨  ≡cong ( λ g → slmap se g x )  (sym ( iso-hom s  ) ) ⟩
+        slmap se ((hom→ s (hom← s slid)) ) x 
+       ≡⟨⟩
+         FMap Γ (hom← s (hom→ s (hom← s slid))) x
+       ≡⟨  ≡cong ( λ g → FMap Γ g  x )  (hom-iso s ) ⟩
+         FMap Γ (hom← s slid) x
+       ≡⟨ {!!} ⟩
+         FMap Γ (id1 C a) x
+       ≡⟨ ≡cong ( λ g →  g x ) ( IsFunctor.identity (isFunctor  Γ ) ) ⟩
+         x
+       ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
 
-cone-equ' :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+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 Γ)  ) 
+    → ( 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 =  {!!}
+
+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 Γ)  ) 
-    →    FMap Γ (hom← s f) (proj (equ (slequ se a b f )) a) ≡  proj (equ (slequ se a b f)) b 
-cone-equ' C I s Γ a b f se  = fe=ge0 (slequ se  a b f ) 
+    → proj ( equ ( slequ se a b f)) a ≡ proj (slprod se {a}) 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)) a 
+       ≡⟨⟩
+          proj (slprod se {a}) a
+       ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+
+llb :  {  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)) b ≡ proj (slprod se {b}) b 
+llb C I s Γ a b f se = {!!}
+
 
 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 I s  Γ =  record {
+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 se) refl )) i
              ; isNTrans = record { commute = commute1 }
@@ -213,8 +253,12 @@
              ≡⟨⟩
                   FMap Γ f (proj (slprod se) a )
              ≡⟨  ≡cong ( λ g → FMap Γ g (proj (slprod se) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj (slprod se {a}) a)
-             ≡⟨  fe=ge0 (cone-equ  C I s Γ a b ( hom→ s f) se ) ⟩
+                  FMap Γ  (hom← s ( hom→ s f))  (proj (slprod se {a}) a)
+             ≡⟨  ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g ) (sym (lla C I s Γ a b ( hom→ s f)  se ) ) ⟩
+                  FMap Γ  (hom← s ( hom→ s f))  (proj (equ ( slequ se a b ( hom→ s f))) a)
+             ≡⟨  fe=ge0 (slequ se a b ( hom→ s f) ) ⟩
+                  proj (equ (slequ se a b ( hom→ s f))) b
+             ≡⟨  llb C I s Γ a b ( hom→ s f)  se ⟩
                   proj (slprod se {b}) b 
              ≡⟨⟩
                   (Sets [ (λ se → proj (slprod se {b}) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
@@ -223,6 +267,7 @@
                   open ≡-Reasoning
 
 
+
 SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
@@ -237,11 +282,4 @@
           --    ( e : Obj C  → sproduct (Obj C) sobj  )
           --    sequ (Obj C) (ΓObj s Γ j) (λ x₁ → ΓMap s Γ f (proj (e x₁) i)) (λ x₁ → proj (e x₁) j)
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
-          limit1 a t = λ x →  record { slequ = λ i j f →  k (λ p → 
-                iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) ( begin
-                         (λ x₁ → ΓMap s Γ f (proj x₁ i)) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
-                      ≈⟨ car  (nat t)  ⟩
-                         (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
-                      ∎ 
-                    ) x }
-                        where open ≈-Reasoning (Sets { c₂})
+          limit1 a t = λ x →  record { slequ = λ i j f →  elem (record { proj = λ i → TMap t i x   }) ( ≡cong ( λ g → g x)  (IsNTrans.commute (isNTrans t )))    }