Mercurial > hg > Members > kono > Proof > category

changeset 569:25c18786fbdc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lemma-equ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Apr 2017 12:17:41 +0900
parents f3fb9061a8ca
children 3d6d8fea3e09
files SetsCompleteness.agda
diffstat 1 files changed, 11 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 24 12:01:03 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 12:17:41 2017 +0900
@@ -121,10 +121,6 @@
 ek=h : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ {_} {a} {b} {f} {g} e )  o k h eq ] ≈ h ]
 ek=h {_} {_} {_} {_} {_} {d} {h} {eq} = refl 
 
-lemma-equ : {  c₂ : Level} {a b b' : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } { f' g' : Hom (Sets {c₂}) a b' }
-          (s : sequ a b f g )  ( t : sequ a b' f' g' )    →   equ s ≡ equ t
-lemma-equ ( elem x eq ) ( elem y eq')  =  {!!}
-
 open sequ
 
 --           equalizer-c = sequ a b f g
@@ -196,9 +192,14 @@
 
 open snequ
 
-
 open import HomReasoning
 open NTrans
+
+lemma-equ : {  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 : snequ (ΓObj s Γ) (ΓMap s Γ)  }
+          → snmap (equ (snequ1 se {a} {a} (λ x → x))) a ≡ snmap (equ (snequ1 se {a} {b} f )) a 
+lemma-equ = {!!}
+
 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 (snequ (ΓObj s Γ) (ΓMap s Γ) )) Γ
 Cone C I s  Γ =  record {
@@ -211,13 +212,13 @@
                    (Sets [ FMap Γ f o (λ se₁ → snmap (equ (snequ1 se₁ (λ x → x))) a) ]) se
              ≡⟨⟩
                    FMap Γ f (snmap (equ (snequ1 se (λ x → x))) a)
-             ≡⟨ {!!} ⟩
+             ≡⟨  ≡cong ( λ g → FMap Γ g (snmap (equ (snequ1 se (λ x → x))) a))  (sym ( hom-iso s  ) ) ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (snequ1 se {a} {a} (λ x → x))) a)
-             ≡⟨ {!!} ⟩
+             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ C I s Γ  )   ⟩
                    FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (snequ1 se (hom→ s f ))) a)
              ≡⟨  fe=ge0 ( snequ1 se (hom→ s f ) ) ⟩
                    snmap (equ (snequ1 se ( hom→ s f ) )) b
-             ≡⟨ {!!} ⟩
+             ≡⟨ sym ( lemma-equ C I s Γ )  ⟩
                    snmap (equ (snequ1 se (λ x → x))) b
              ≡⟨⟩
                   (Sets [ (λ se₁ → snmap (equ (snequ1 se₁ (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ]) se
@@ -234,7 +235,7 @@
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
                limit  =  limit1 
-             ; t0f=t = λ {a t i } → {!!}
+             ; t0f=t = λ {a t i } → refl
              ; limit-uniqueness  =  λ {a} {t} {f} → uniquness1 {a} {t} {f}
           }
        }  where
@@ -254,7 +255,7 @@
                   record { snmap = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
                   record { snmap = λ i →   snmap (equ (snequ1 (f x) {i} {i} (λ x → x )) ) i }
-                ≡⟨ {!!}  ⟩
+                ≡⟨ ≡cong ( λ g →   record { snmap = λ i →  g i  } ) (  extensionality Sets  ( λ  i  → lemma-equ C I s Γ ))  ⟩
                   record { snmap = λ i₁ →  snmap (equ (snequ1 (f x) f')) i₁  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality