Mercurial > hg > Members > kono > Proof > category

changeset 580:c9361d23aa3a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
to case for equ lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 29 Apr 2017 22:22:20 +0900
parents 36d346a3d6fd
children 41ef69cd5871 cd65d5c9a54d
files SetsCompleteness.agda
diffstat 1 files changed, 24 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Apr 28 19:00:50 2017 +0900
+++ b/SetsCompleteness.agda	Sat Apr 29 22:22:20 2017 +0900
@@ -173,6 +173,8 @@
     {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 
 
+slid :   {  c₁  : Level}  { I :  Set  c₁ }  →   I → I
+slid x = x
 
 record slim  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
       :  Set   c₂  where
@@ -180,34 +182,32 @@
        slequ : { i j : OC } → ( f :  I → I ) →  sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
    ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj
    ipp {i} {j} f = equ ( slequ {i} {j} f )
-   -- 
-   -- slobj : OC →  Set  c₂ 
-   -- slobj i = sobj i
+   slobj : OC →  Set  c₂ 
+   slobj i = sobj i
+   llr :  {i j : OC } → ( f : I → I ) →  proj ( equ ( slequ {i} {i} slid )) i ≡ proj ( equ ( slequ {i} {j} f )) i 
+   llr {i} {j} f = ?
+   lll :  {i j  : OC } → ( f : I → I ) →  proj ( equ ( slequ {i} {j} f )) j ≡ proj ( equ ( slequ {j} {j} slid )) j 
+   lll  {i} {j} f  = {!!}
+   ll :  {x i j i' j' : OC } → ( f f' : I → I ) →  proj ( equ ( slequ {i} {j} f )) x ≡ proj ( equ ( slequ {i'} {j'} f' )) x 
+   ll {x} {i} {j} {i'} {j'} f f' = begin
+           proj ( equ {_} {sproduct OC sobj } {sobj j} ( slequ {i} {j} f )) x 
+        ≡⟨ {!!} ⟩
+           proj ( equ {_} {sproduct OC sobj } {sobj j'} ( slequ {i'} {j'} f' )) x 
+        ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
    -- slmap : {i j : OC } →  (f : I → I ) → sobj i → sobj j
    -- slmap f = smap f 
 
 open slim
 
 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 } 
+    {x i j i' j' : Obj C } →　 { f f' : I → I } 
     →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
-    →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i'} {j'} f' ) i
-lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se =   ≡cong ( λ p →  proj p i ) ( begin
-                 ipp se {i} {j} f 
-             ≡⟨⟩
-                 record { proj = λ x → proj (equ (slequ se 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 f')) x }
-             ≡⟨⟩
-                 ipp se {i'} {j'} f'  
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+    →  proj (ipp se {i} {j} f) x ≡ proj (ipp se {i'} {j'} f' ) x
+lemma-equ C I s Γ {x} {i} {j} {i'} {j'} {f} {f'} se =   ll se f f'
 
-slid :   {  c₁  : Level}  { I :  Set  c₁ }  →   I → I
-slid x = x
 
 open import HomReasoning
 open NTrans
@@ -227,11 +227,11 @@
                    FMap Γ f (proj ( ipp se {a} {a} slid ) a)
              ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} slid ) a))  (sym ( hom-iso s  ) ) ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} slid ) a)
-             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ   se ) ⟩
+             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ {a} se ) ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
              ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
                    proj (ipp se {a} {b} ( hom→ s f  )) b
-             ≡⟨ sym ( lemma-equ C I s Γ se ) ⟩
+             ≡⟨ sym ( lemma-equ C I s Γ {b} se ) ⟩
                    proj (ipp se {b} {b} (λ x → x)) b
              ≡⟨⟩
                   (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
@@ -270,7 +270,7 @@
                   record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
                   record { proj = λ i →   proj (ipp (f x) {i} {i} slid ) i }
-                ≡⟨ ≡cong ( λ g →   record { proj = λ i' →  g i' } ) ( extensionality Sets  ( λ  i''  → lemma-equ C I s Γ (f x)))  ⟩
+                ≡⟨ ≡cong ( λ g →   record { proj = λ i' →  g i' } ) ( extensionality Sets  ( λ  i''  → lemma-equ C I s Γ {i''} (f x)))  ⟩
                   record { proj = λ i →  proj (ipp (f x) f') i  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality
@@ -289,7 +289,7 @@
                   elm-cong (  elem ( record { proj = λ i → TMap t i x }  ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) )
                            )))
                      ) ⟩
-                   record { slequ = λ {i} {j} f' → slequ (f x ) f' }
+                   record { slequ = λ {i} {j} f' → slequ (f x ) f'  }
                 ≡⟨⟩
                   f x
                 ∎  ) where