Mercurial > hg > Members > kono > Proof > category

changeset 500:6c993c1fe9de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try to make prodcut and equalizer in Sets
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Mar 2017 19:26:51 +0900
parents 511fd37d90ec
children 61daa68a70c4
files SetsCompleteness.agda
diffstat 1 files changed, 59 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SetsCompleteness.agda	Wed Mar 15 19:26:51 2017 +0900
@@ -0,0 +1,59 @@
+
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+open import Category.Sets
+
+module SetsCompleteness where
+
+
+open import HomReasoning
+open import cat-utility
+open import Relation.Binary.Core
+open import Function
+open import Data.Product
+
+
+SetsProduct :  {  c₂ : Level} → CreateProduct ( Sets  {  c₂} )
+SetsProduct { c₂ } = record { 
+         product =  λ a b →  a × b
+       ; π1 = λ a b → λ ab → (proj₁ ab)
+       ; π2 = λ a b → λ ab → (proj₂ ab)
+       ; isProduct =  λ a b → record {
+              _×_  = λ f g  x →  ( f x , g x )
+              ; π1fxg=f = refl
+              ; π2fxg=g  = refl
+              ; uniqueness = refl
+              ; ×-cong   =  λ {c} {f} {f'} {g} {g'} f=f g=g →  prod-cong a b f=f g=g
+          }
+      } where
+          prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
+              → Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
+              → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
+          prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl
+
+
+SetsEqualizer :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
+SetsEqualizer f g = record { 
+           equalizer-c = {!!} 
+         ; equalizer = {!!}
+         ; isEqualizer = record {
+               fe=ge  = {!!}
+             ; k = {!!}
+             ; ek=h = {!!}
+             ; uniqueness  = {!!}
+           }
+       }
+
+
+SetsLimit : { c₁' c₂' ℓ' : Level} {  c₂ : Level}  ( I : Category c₁' c₂' ℓ' ) → ( Γ : Functor I (Sets { c₂}) ) →  Limit Sets I Γ
+SetsLimit I Γ = record { 
+           a0 = {!!} 
+         ; t0 = {!!}
+         ; isLimit = record {
+               limit  = {!!}
+             ; t0f=t = {!!}
+             ; limit-uniqueness  = {!!}
+           }
+       }
+
+