Mercurial > hg > Members > kono > Proof > category

changeset 579:36d346a3d6fd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 28 Apr 2017 19:00:50 +0900
parents 6b9737d041b4
children c9361d23aa3a
files SetsCompleteness.agda
diffstat 1 files changed, 17 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Apr 28 18:50:13 2017 +0900
+++ b/SetsCompleteness.agda	Fri Apr 28 19:00:50 2017 +0900
@@ -165,12 +165,6 @@
 
 open Small 
 
-≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C ) 
-    →  a  ≡  a'
-    →  b  ≡  b'
-    →  f a b  ≡  f a' b'
-≡cong2 _ refl refl = refl
-
 ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
    (i : Obj C ) →　 Set c₁
 ΓObj s  Γ i = FObj Γ i
@@ -184,12 +178,13 @@
       :  Set   c₂  where
    field 
        slequ : { i j : OC } → ( f :  I → I ) →  sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
-   slobj : OC →  Set  c₂ 
-   slobj i = sobj i
-   slmap : {i j : OC } →  (f : I → I ) → sobj i → sobj j
-   slmap f = smap f 
    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
+   -- slmap : {i j : OC } →  (f : I → I ) → sobj i → sobj j
+   -- slmap f = smap f 
 
 open slim
 
@@ -197,15 +192,13 @@
     {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
+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'  
@@ -213,6 +206,8 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
+slid :   {  c₁  : Level}  { I :  Set  c₁ }  →   I → I
+slid x = x
 
 open import HomReasoning
 open NTrans
@@ -221,17 +216,17 @@
 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 {
-               TMap = λ i →  λ se → proj ( ipp se {i} {i} (\x -> x) ) i
+               TMap = λ i →  λ se → proj ( ipp se {i} {i} slid ) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  (\x -> x) ) a) ] ≈
-                Sets [ (λ se → proj ( ipp se  (\x -> x) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  slid ) a) ] ≈
+                Sets [ (λ se → proj ( ipp se  slid ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
          commute1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
-                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  (\x -> x) ) a) ]) se
+                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  slid ) a) ]) se
              ≡⟨⟩
-                   FMap Γ f (proj ( ipp se {a} {a} (\x -> x) ) a)
-             ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (\x -> x) ) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} (\x -> x) ) a)
+                   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 ) ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
              ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
@@ -274,8 +269,8 @@
                 ≡⟨   ≡cong ( λ g → record { proj = λ i → g i  } ) (  extensionality Sets  ( λ i →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
                   record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
-                  record { proj = λ i →   proj (ipp (f x) {i} {i} (\x -> x) ) i }
-                ≡⟨ ≡cong ( λ g →   record { proj = λ i' -> g i' } ) ( extensionality Sets  ( λ  i''  → lemma-equ C I s Γ (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)))  ⟩
                   record { proj = λ i →  proj (ipp (f x) f') i  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality