Mercurial > hg > Members > kono > Proof > category

changeset 603:e548f8f2b9b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
two field again ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Jun 2017 20:52:22 +0900
parents b7659ad60a69
children 75112154faf0
files SetsCompleteness.agda
diffstat 1 files changed, 0 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Jun 05 18:57:15 2017 +0900
+++ b/SetsCompleteness.agda	Mon Jun 05 20:52:22 2017 +0900
@@ -148,40 +148,6 @@
                   open ≡-Reasoning
 
 
---  
---     
-        --
-        --         equ            f
-        --  elem -------→ a ---------→ b        
-        --    ^        .    ---------→
-        --    |      .            g
-        --    |k   .
-        --    |  . e
-        --    c
-
---  
-makeEqu :  { c₂ : Level}  →  {a b c : Obj  (Sets {c₂})} → (e : Hom  (Sets {c₂}) c a )  → (f g : Hom  (Sets {c₂}) a b)  → IsEqualizer  (Sets {c₂}) e f g
-makeEqu {c₂} {a} {b} {c} e f g =  record {
-               fe=ge  = {!!}
-             ; k = λ {d} h eq → {!!}
-             ; ek=h = λ {d} {h} {eq} → {!!}
-             ; uniqueness  = {!!}
-       } where
-           equ0 : IsEqualizer Sets (λ e → equ e ) f g
-           equ0 = SetsIsEqualizer a b f g
-           c→equ0 : Hom Sets c ( sequ a b f g )
-           c→equ0 x = elem (e x)  {!!} -- (  ≡cong ( λ y → y {!!} ) ( IsEqualizer.fe=ge equ0 ) )
-
-makeProd :  { c₂ : Level} → ( I :  Obj (Sets {c₂}) ) 
-    → (p : Obj (Sets {c₂})) ( ai : I → Obj (Sets {c₂}) )  ( pi : (i : I) → Hom (Sets {c₂}) p ( ai i ) )
-                  →  IsIProduct (Sets {c₂}) I p ai pi 
-makeProd I p fi pi = record {
-              iproduct = λ {q} qi x → ?
-            ; pif=q = {!!}
-            ; ip-uniqueness = {!!}
-            ; ip-cong  = {!!}
-       }
-
 open Functor
 
 ----
@@ -247,24 +213,18 @@
     →  (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
 
-
 open import HomReasoning
 open NTrans
 
-
 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 {