Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 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
children 61daa68a70c4
comparison
equal deleted inserted replaced
499:511fd37d90ec 500:6c993c1fe9de
1
2 open import Category -- https://github.com/konn/category-agda
3 open import Level
4 open import Category.Sets
5
6 module SetsCompleteness where
7
8
9 open import HomReasoning
10 open import cat-utility
11 open import Relation.Binary.Core
12 open import Function
13 open import Data.Product
14
15
16 SetsProduct : { c₂ : Level} → CreateProduct ( Sets { c₂} )
17 SetsProduct { c₂ } = record {
18 product = λ a b → a × b
19 ; π1 = λ a b → λ ab → (proj₁ ab)
20 ; π2 = λ a b → λ ab → (proj₂ ab)
21 ; isProduct = λ a b → record {
22 _×_ = λ f g x → ( f x , g x )
23 ; π1fxg=f = refl
24 ; π2fxg=g = refl
25 ; uniqueness = refl
26 ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g
27 }
28 } where
29 prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
30 → Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
31 → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
32 prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl
33
34
35 SetsEqualizer : { c₂ : Level} → {a b : Obj (Sets {c₂}) } (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
36 SetsEqualizer f g = record {
37 equalizer-c = {!!}
38 ; equalizer = {!!}
39 ; isEqualizer = record {
40 fe=ge = {!!}
41 ; k = {!!}
42 ; ek=h = {!!}
43 ; uniqueness = {!!}
44 }
45 }
46
47
48 SetsLimit : { c₁' c₂' ℓ' : Level} { c₂ : Level} ( I : Category c₁' c₂' ℓ' ) → ( Γ : Functor I (Sets { c₂}) ) → Limit Sets I Γ
49 SetsLimit I Γ = record {
50 a0 = {!!}
51 ; t0 = {!!}
52 ; isLimit = record {
53 limit = {!!}
54 ; t0f=t = {!!}
55 ; limit-uniqueness = {!!}
56 }
57 }
58
59