Mercurial > hg > Members > kono > Proof > category

annotate SetsCompleteness.agda @ 537:2f261a3836bc

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 Thu, 30 Mar 2017 18:11:11 +0900
parents 09beac05a0fb
children d22c93dca806
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Category -- https://github.com/konn/category-agda
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
4 open import Category.Sets renaming ( _o_ to _*_ )
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 module SetsCompleteness where
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import cat-utility
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary.Core
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Function
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
12 import Relation.Binary.PropositionalEquality
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
13 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
14 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
15
520
5b4a794f3784 k-cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 519
diff changeset
16 ≡cong = Relation.Binary.PropositionalEquality.cong
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
17
524
d6739779b4ac on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 523
diff changeset
18 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} →
d6739779b4ac on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 523
diff changeset
19 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x
d6739779b4ac on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 523
diff changeset
20 lemma1 refl x = refl
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
21
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
22 record Σ {a} (A : Set a) (B : Set a) : Set a where
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
23 constructor _,_
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
24 field
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
25 proj₁ : A
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
26 proj₂ : B
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
27
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
28 open Σ public
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 SetsProduct : { c₂ : Level} → CreateProduct ( Sets { c₂} )
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 SetsProduct { c₂ } = record {
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
33 product = λ a b → Σ a b
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 ; π1 = λ a b → λ ab → (proj₁ ab)
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 ; π2 = λ a b → λ ab → (proj₂ ab)
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ; isProduct = λ a b → record {
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
37 _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x )
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ; π1fxg=f = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ; π2fxg=g = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ; uniqueness = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 }
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 } where
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 → Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
50 record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
51 field
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
52 pi1 : ( i : I ) → pi0 i
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
53
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
54 open iproduct
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
55
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
56 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
57 → IProduct ( Sets { c₂} ) I
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
58 SetsIProduct I fi = record {
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
59 ai = fi
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
60 ; iprod = iproduct I fi
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
61 ; pi = λ i prod → pi1 prod i
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
62 ; isIProduct = record {
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
63 iproduct = iproduct1
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
64 ; pif=q = pif=q
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
65 ; ip-uniqueness = ip-uniqueness
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
66 ; ip-cong = ip-cong
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
67 }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
68 } where
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
69 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
70 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
71 pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ]
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
72 pif=q {q} qi {i} = refl
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
73 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
74 ip-uniqueness = refl
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
75 ipcx : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
76 ipcx {q} {qi} {qi'} qi=qi x =
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
77 begin
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
78 record { pi1 = λ i → (qi i) x }
520
5b4a794f3784 k-cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 519
diff changeset
79 ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
80 record { pi1 = λ i → (qi' i) x }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
81 ∎ where
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
82 open import Relation.Binary.PropositionalEquality
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
83 open ≡-Reasoning
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
84 ip-cong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1 qi' ]
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
85 ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi )
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
86
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
87
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
88 --
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
89 -- e f
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
90 -- c -------→ a ---------→ b f ( f'
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
91 -- ^ . ---------→
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
92 -- | . g
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
93 -- |k .
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
94 -- | . h
514
1fca61019bdf on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 513
diff changeset
95 --y : d
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
96
522
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
97 -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
98
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
99 data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
100 elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
101
532
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
102 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
103 equ (elem x eq) = x
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
104
533
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
105 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
106 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
107 fe=ge0 (elem x eq ) = eq
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
108
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
109 open sequ
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
110
532
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
111 -- equalizer-c = sequ a b f g
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
112 -- ; equalizer = λ e → equ e
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
113
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
114 SetsIsEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
115 SetsIsEqualizer {c₂} a b f g = record {
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
116 fe=ge = fe=ge
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
117 ; k = k
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
118 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
119 ; uniqueness = uniqueness
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
120 } where
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
121 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
122 fe=ge = extensionality Sets (fe=ge0 )
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
123 k : {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
520
5b4a794f3784 k-cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 519
diff changeset
124 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq )
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
125 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 ]
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
126 ek=h {d} {h} {eq} = refl
520
5b4a794f3784 k-cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 519
diff changeset
127 irr : {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq'
5b4a794f3784 k-cong done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 519
diff changeset
128 irr refl refl = refl
523
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
129 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
130 injection f = ∀ x y → f x ≡ f y → x ≡ y
522
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
131 elm-cong : (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
132 elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' )
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
133 lemma5 : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
134 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
135 lemma5 refl x = refl -- somehow this is not equal to lemma1
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
136 uniqueness : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
137 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ]
525
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
138 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
139 k h fh=gh x
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
140 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
141 k' x
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
142 ∎ ) where
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
143 open import Relation.Binary.PropositionalEquality
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
144 open ≡-Reasoning
cb35d6b25559 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 524
diff changeset
145
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146
501
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
147 open Functor
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
149 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ )
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
150 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
151 field
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
152 small→ : Obj C → I
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
153 small← : I → Obj C
527
beac7b0786cb fix ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
154 small-iso : { x : Obj C } → Hom C (small← ( small→ x )) x
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
155 shom→ : {i j : Obj C } → Hom C i j → I → I
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
156 shom← : {i j : I } → ( f : I → I ) → Hom C ( small← i ) ( small← j )
536
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
157 iso1 : {a b : Obj C} {f : Hom C a b} → C [ f o small-iso ] ≡ C [ small-iso o shom← (shom→ f) ]
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
158
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
159 -- iso1 should be proved by these ...
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
160 -- small-≡ : { x : Obj C } → (small← ( small→ x )) ≡ x
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
161 -- shom-iso : {i j : I } → ( f : Hom C ( small← i ) ( small← j ) ) → C [ shom← ( shom→ f ) ≈ f ]
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
162 -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
163
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
164 open Small
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
165
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
166 ≡subst : {c : Level } { x y : Set c } { f : Set c → Set c } → ( x ≡ y ) → f x ≡ f y
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
167 ≡subst {c} {x} {.x} {f} refl = ≡cong ( λ x → f x ) refl
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
168
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
169 iid : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {I : Set c₁} ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ){i : Obj C } →
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
170 Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
171 iid s Γ = FMap Γ ( small-iso s )
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
172
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
173
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
174 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
175 (i : I ) →　 Set c₁
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
176 ΓObj s Γ i = FObj Γ (small← s i )
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
177
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
178 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
179 {i j : I } →　 ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
180 ΓMap s Γ {i} {j} f = FMap Γ ( shom← s f )
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
181
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
182 record snat { c₂ } { I : Set c₂ } ( sobj : I → Set c₂ )
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
183 ( smap : { i j : I } → (f : I → I )→ sobj i → sobj j ) : Set c₂ where
527
beac7b0786cb fix ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
184 field
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
185 snmap : ( i : I ) → sobj i
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
186 sncommute : { i j : I } → ( f : I → I ) → smap f ( snmap i ) ≡ snmap j
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
187
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
188 open snat
501
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
189
530
89af55191ec6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 529
diff changeset
190 open import HomReasoning
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
191
530
89af55191ec6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 529
diff changeset
192 open NTrans
533
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
193
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
194 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
195 → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
196 Cone C I s Γ = record {
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
197 TMap = λ i → λ sn → iid s Γ ( snmap sn (small→ s i ) )
531
66cad3cb3a66 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 530
diff changeset
198 ; isNTrans = record { commute = comm1 }
530
89af55191ec6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 529
diff changeset
199 } where
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
200 comm1 : {a b : Obj C} {f : Hom C a b} →
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
201 Sets [ Sets [ FMap Γ f o (λ sn → iid s Γ (snmap sn (small→ s a))) ] ≈
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
202 Sets [ (λ sn → iid s Γ (snmap sn (small→ s b))) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
203 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
204 FMap Γ f ( ( FMap Γ ( small-iso s ) ) (snmap sn (small→ s a)) )
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
205 ≡⟨⟩
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
206 ( Sets [ FMap Γ f o FMap Γ ( small-iso s ) ] ) (snmap sn (small→ s a))
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
207 ≡⟨ ≡cong (λ z → z (snmap sn (small→ s a)) ) (sym ( IsFunctor.distr (isFunctor Γ ) )) ⟩
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
208 FMap Γ ( C [ f o (small-iso s) ] ) (snmap sn (small→ s a) )
536
09beac05a0fb add iso1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 535
diff changeset
209 ≡⟨ ≡cong (λ z → ( FMap Γ z ) (snmap sn (small→ s a))) (iso1 s) ⟩
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
210 FMap Γ ( C [ (small-iso s) o shom← s (shom→ s f) ] ) ( snmap sn ( small→ s a ))
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
211 ≡⟨ ≡cong (λ z → z (snmap sn (small→ s a)) ) ( IsFunctor.distr (isFunctor Γ ) ) ⟩
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
212 ( Sets [ FMap Γ (small-iso s) o FMap Γ (shom← s (shom→ s f)) ] ) ( snmap sn ( small→ s a ))
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
213 ≡⟨⟩
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
214 ( Sets [ FMap Γ (small-iso s) o (ΓMap s Γ (shom→ s f)) ] ) ( snmap sn ( small→ s a ))
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
215 ≡⟨⟩
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
216 FMap Γ (small-iso s) ((ΓMap s Γ (shom→ s f)) ( snmap sn ( small→ s a )) )
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
217 ≡⟨ ≡cong ( λ y → iid s Γ y ) ( sncommute sn (shom→ s f) ) ⟩
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
218 FMap Γ (small-iso s) (snmap sn (small→ s b))
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
219 ∎ ) where
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
220 open import Relation.Binary.PropositionalEquality
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
221 open ≡-Reasoning
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
222
530
89af55191ec6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 529
diff changeset
223
89af55191ec6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 529
diff changeset
224
526
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
225 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
226 → Limit Sets C Γ
b035cd3be525 Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 525
diff changeset
227 SetsLimit { c₂} C I s Γ = record {
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
228 a0 = snat (ΓObj s Γ) (ΓMap s Γ)
535
5d7f8921bac0 on going ....
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 534
diff changeset
229 ; t0 = Cone C I s Γ
523
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
230 ; isLimit = record {
530
89af55191ec6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 529
diff changeset
231 limit = limit1
523
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
232 ; t0f=t = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
233 ; limit-uniqueness = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
234 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
235 } where
527
beac7b0786cb fix ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 526
diff changeset
236 a0 : Obj Sets
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
237 a0 = snat (ΓObj s Γ) (ΓMap s Γ)
537
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
238 comm2 : { a : Obj Sets } {x : a } {i j : I} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
239 → ΓMap s Γ f (TMap t (small← s i) x) ≡ TMap t (small← s j) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
240 comm2 = {!!}
534
a90889cc2988 introducing snat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 533
diff changeset
241 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
537
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
242 limit1 a t = λ x → record { snmap = λ i → ( TMap t ( small← s i ) ) x ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
243 sncommute = λ f → comm2 t f }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
244
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
246
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
247
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
248
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
249
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 536
diff changeset
250