Mercurial > hg > Members > kono > Proof > category

changeset 541:505962017fd1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Mar 2017 10:28:34 +0900
parents 2373c11a93f1
children bc3802c5c8e4
files SetsCompleteness.agda
diffstat 1 files changed, 28 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 31 08:49:10 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 31 10:28:34 2017 +0900
@@ -106,6 +106,9 @@
      (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
 fe=ge0 (elem x eq )  =  eq
 
+irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
+irr refl refl = refl
+
 open sequ
 
 --           equalizer-c = sequ a b f g
@@ -124,8 +127,6 @@
            k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
            ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
            ek=h {d} {h} {eq} = refl 
-           irr : {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
-           irr refl refl = refl
            injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
            injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
            elm-cong :   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
@@ -175,8 +176,31 @@
 
 open snat
 
+≡cong2 : { c : Level } { A B 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
+
+snat-cong : { c₂ : Level }  { I OC :  Set  c₂ } { sobj :  OC →  Set  c₂ }
+     { smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j } →
+     ( s t :  snat sobj smap ) →
+     ( snmap s ≡ snmap t )  → s ≡ t
+snat-cong s t smt=sms =   begin
+                record { snmap = snmap s ; sncommute = λ f → sncommute s f }
+             ≡⟨  ≡cong2 ( λ sm sc → record { snmap = sm  ; sncommute = λ f →  ?  }  ) smt=sms  ( irr ? ? ) ⟩
+                record { snmap = snmap t ; sncommute = λ f → sncommute t f }
+             ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+snat1 :  { c₂ : Level }  { I OC :  Set  c₂ } { sobj :  OC →  Set  c₂ } 
+     { smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j } ( snmap0 : ( i : OC ) → sobj i )
+       { sncommute0 : { i j : OC } → ( f :  I ) →  smap f ( snmap0 i )  ≡ snmap0 j } 
+     → snat sobj smap
+snat1 snmap0 { sncommute0} = record { snmap = snmap0 ; sncommute = sncommute0 }
+
 open import HomReasoning
-
 open NTrans
 
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) ) 
@@ -201,7 +225,6 @@
                   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 { 
@@ -238,7 +261,7 @@
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
              ≡⟨ {!!} ⟩
-                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ f → ? }
+                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x
              ∎  ) where