annotate pullback.agda @ 297:537570f6a44f

limit preservation proved.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 25 Sep 2013 21:12:29 +0900
parents bba60d843462
children 61669ac03e7d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -- Pullback from product and equalizer
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 --
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 --
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 ----
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Category -- https://github.com/konn/category-agda
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Level
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
9 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import HomReasoning
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import cat-utility
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
14 --
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
15 -- Pullback from equalizer and product
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 -- f
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 -- a -------> c
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
18 -- ^ ^
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 -- π1 | |g
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 -- | |
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 -- ab -------> b
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 -- ^ π2
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 -- |
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
24 -- | e = equalizer (f π1) (g π1)
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
25 -- |
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
26 -- d <------------------ d'
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
27 -- k (π1' × π2' )
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
29 open Equalizer
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
30 open Product
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
31 open Pullback
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
32
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
33 pullback-from : (a b c ab d : Obj A)
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 ( f : Hom A a c ) ( g : Hom A b c )
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
35 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab )
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
36 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
37 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
38 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
39 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
40 pullback-from a b c ab d f g π1 π2 e eqa prod = record {
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 commute = commute1 ;
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
42 p = p1 ;
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
43 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ;
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
44 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ;
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 uniqueness = uniqueness1
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
46 } where
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
47 commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
48 commute1 = let open ≈-Reasoning (A) in
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
49 begin
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
50 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
51 ≈⟨ assoc ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
52 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
53 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
54 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
55 ≈↑⟨ assoc ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
56 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
57
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
58 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
59 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
60 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
61 begin
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
62 ( f o π1 ) o (prod × π1') π2'
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
63 ≈↑⟨ assoc ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
64 f o ( π1 o (prod × π1') π2' )
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
65 ≈⟨ cdr (π1fxg=f prod) ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
66 f o π1'
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
67 ≈⟨ eq ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
68 g o π2'
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
69 ≈↑⟨ cdr (π2fxg=g prod) ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
70 g o ( π2 o (prod × π1') π2' )
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
71 ≈⟨ assoc ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
72 ( g o π2 ) o (prod × π1') π2'
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
73
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
74 p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
75 p1 {d'} { π1' } { π2' } eq =
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
76 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq )
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
77 π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
78 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
79 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
80 begin
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
81 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
82 ≈⟨⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
83 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
84 ≈↑⟨ assoc ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
85 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
86 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
87 π1 o (_×_ prod π1' π2' )
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
88 ≈⟨ π1fxg=f prod ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
89 π1'
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
90
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
91 π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
263
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
92 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
93 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
94 begin
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
95 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
96 ≈⟨⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
97 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
98 ≈↑⟨ assoc ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
99 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
100 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
101 π2 o (_×_ prod π1' π2' )
262
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
102 ≈⟨ π2fxg=g prod ⟩
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
103 π2'
e1b08c5e4d2e uniqueness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 261
diff changeset
104
261
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
105 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
106 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
107 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
a2477147dfec pull back continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
108 A [ p1 eq ≈ p' ]
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
109 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
263
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
110 begin
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
111 p1 eq
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
112 ≈⟨⟩
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
113 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
114 ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
115 e o p'
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
116 ≈⟨⟩
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
117 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
118 ≈↑⟨ Product.uniqueness prod ⟩
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
119 (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'))
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
120 ≈⟨ ×-cong prod (assoc) (assoc) ⟩
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
121 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
122 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
264
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
123 ≈⟨ ×-cong prod eq1 eq2 ⟩
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
124 ((prod × π1') π2')
78ce12f8e6b6 pullback done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 263
diff changeset
125 ∎ ) ⟩
263
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
126 p'
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
127
c1b3193097ce on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
128
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
129 ------
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
130 --
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
131 -- Limit
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
132 --
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
133 -----
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
134
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
135 -- Constancy Functor
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
136
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
137 K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
138 → ( a : Obj A ) → Functor I A
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
139 K A I a = record {
265
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
140 FObj = λ i → a ;
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
141 FMap = λ f → id1 A a ;
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
142 isFunctor = let open ≈-Reasoning (A) in record {
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
143 ≈-cong = λ f=g → refl-hom
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
144 ; identity = refl-hom
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
145 ; distr = sym idL
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
146 }
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
147 }
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
148
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
149 open NTrans
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
150
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
151 record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
152 ( a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
265
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
153 field
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
154 limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
155 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
265
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
156 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
157 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
158 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ]
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
159 A0 : Obj A
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
160 A0 = a0
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
161 T0 : NTrans I A ( K A I a0 ) Γ
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
162 T0 = t0
265
367e8fde93ee add limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
163
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
164 --------------------------------
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
165 --
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
166 -- If we have two limits on c and c', there are isomorphic pair h, h'
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
167
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
168 open Limit
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
169
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
170 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
171 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
172 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' )
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
173 → Hom A a0 a0'
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
174 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
175
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
176 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
177 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
178 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' )
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
179 → Hom A a0' a0
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
180 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
181
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
182
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
183 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
184 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
185 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) → ∀{ i : Obj I } →
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
186 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ]
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
187 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
188 limit lim' a0 t0 o limit lim a0' t0'
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
189 ≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
190 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
191 ≈⟨ assoc ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
192 ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0'
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
193 ≈⟨ car ( t0f=t lim' ) ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
194 TMap t0 i o limit lim a0' t0'
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
195 ≈⟨ t0f=t lim ⟩
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
196 TMap t0' i
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
197 ∎) ) ⟩
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
198 limit lim' a0' t0'
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
199 ≈⟨ limit-uniqueness lim' idR ⟩
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
200 id a0'
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
201
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
202
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
203
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
204 open import CatExponetial
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
205
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
206 open Functor
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
207
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
208 --------------------------------
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
209 --
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
210 -- Contancy Functor
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
211
268
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
212 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I )
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
213 KI { c₁'} {c₂'} {ℓ'} I = record {
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
214 FObj = λ a → K A I a ;
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
215 FMap = λ f → record { -- NTrans I A (K A I a) (K A I b)
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
216 TMap = λ a → f ;
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
217 isNTrans = record {
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
218 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
219 }
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
220 } ;
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
221 isFunctor = let open ≈-Reasoning (A) in record {
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
222 ≈-cong = λ f=g {x} → f=g
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
223 ; identity = refl-hom
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
224 ; distr = refl-hom
266
9e9f1e27e89f iso on limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
225 }
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
226 } where
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
227 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
228 A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ]
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
229 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
230 FMap (K A I b') f₁ o f
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
231 ≈⟨ idL ⟩
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
232 f
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
233 ≈↑⟨ idR ⟩
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
234 f o FMap (K A I a') f₁
267
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
235
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
236
b1b728559d89 Constancy Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
237
272
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
238 ---------
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
239 --
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
240 -- limit gives co universal mapping ( i.e. adjunction )
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
241 --
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
242 -- F = KI I : Functor A (A ^ I)
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
243 -- U = λ b → A0 (lim b {a0 b} {t0 b}
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
244 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} )
272
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
245
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
246 limit2couniv :
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
247 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
248 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K A I (a0 b) ) b )
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
249 → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
277
21ef5ba54458 2 yellow remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
250 limit2couniv lim a0 t0 = record { -- F U ε
274
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
251 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
252 iscoUniversalMapping = record {
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
253 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
254 couniquness = couniquness2
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
255 }
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
256 } where
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
257 couniversalMapping1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
258 A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ]
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
259 couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
260 TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
261 ≈⟨⟩
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
262 TMap (t0 b) i o (limit (lim b) a f)
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
263 ≈⟨ t0f=t (lim b) ⟩
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
264 TMap f i -- i comes from ∀{i} → B [ TMap f i ≈ TMap g i ]
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
265
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
266 couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} →
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
267 ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] )
272
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
268 → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
269 couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
270 limit (lim b {a0 b} {t0 b} ) a f
271
28278175d696 limit2adjoint done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
271 ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩
270
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
272 g
8ba03259a177 one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
273
268
2ff44ee3cb32 co universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 267
diff changeset
274
272
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
275 open import Category.Cat
275
62e84bea7b29 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
276
62e84bea7b29 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
277
278
9fafe4a53f89 univ2limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
278 open coUniversalMapping
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
279
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
280 univ2limit :
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
281 ( U : Obj (A ^ I ) → Obj A )
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
282 ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b )
279
8df8e74e6316 limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
283 ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) →
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
284 ( Γ : Functor I A ) → Limit A I Γ (U Γ) (ε Γ)
278
9fafe4a53f89 univ2limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
285 univ2limit U ε univ Γ = record {
272
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
286 limit = λ a t → limit1 a t ;
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
287 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
288 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
272
5f2b8a5cc115 adjunction to limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 271
diff changeset
289 } where
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
290 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
291 limit1 a t = _*' univ {_} {a} t
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
292 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
279
8df8e74e6316 limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
293 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
274
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
294 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
279
8df8e74e6316 limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
295 TMap (ε Γ) i o limit1 a t
274
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
296 ≈⟨⟩
280
7ae58263d45b univ2limit done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
297 TMap (ε Γ) i o _*' univ {Γ} {a} t
7ae58263d45b univ2limit done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
298 ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
274
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
299 TMap t i
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
300
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
301 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)}
279
8df8e74e6316 limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
302 → ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
274
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
303 limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin
278
9fafe4a53f89 univ2limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
304 _*' univ t
9fafe4a53f89 univ2limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
305 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩
274
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
306 f
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
307
1b651faa2391 adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 273
diff changeset
308
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
309 -----
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
310 --
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
311 -- product on arbitrary index
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
312 --
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
313
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
314 record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c)
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
315 ( p : Obj A ) -- product
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
316 ( ai : I → Obj A ) -- families
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
317 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
318 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
319 field
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
320 product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
321 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ]
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
322 -- special case of product ( qi = pi ) ( should b proved from pif=q )
289
7dc163c026b7 move to iProduct axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 288
diff changeset
323 pif=q1 : { i : I } → { qi : Hom A p (ai i) } → A [ pi i ≈ qi ]
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
324 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
325 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
326 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
327
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
328 open IProduct
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
329 open Equalizer
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
330
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
331 --
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
332 -- limit from equalizer and product
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
333 --
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
334 --
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
335 -- ai
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
336 -- ^ K f = id lim
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
337 -- | pi lim = K i ------------> K j = lim
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
338 -- | | |
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
339 -- p | |
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
340 -- ^ ε i | | ε j
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
341 -- | | |
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
342 -- | e = equalizer (id p) (id p) | |
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
343 -- | v v
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
344 -- lim <------------------ d' a i = Γ i ------------> Γ j = a j
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
345 -- k ( product pi ) Γ f
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
346 -- Γ f o ε i = ε j
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
347 --
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
348 --
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
349
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
350 -- pi-ε -- : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
351 -- → IProduct {c₁'} A (Obj I) p ai pi )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
352 -- ( lim p : Obj A ) ( e : Hom A lim p )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
353 -- ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
354 -- { i : Obj I } → { q : ( i : Obj I ) → Hom A p (FObj Γ i) } → A [ proj i ≈ q i ]
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
355 -- pi-ε prod lim p e proj {i} {q} = let open ≈-Reasoning (A) in begin
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
356 -- proj i
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
357 -- ≈↑⟨ idR ⟩
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
358 -- proj i o id1 A p
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
359 -- ≈⟨ cdr {!!} ⟩
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
360 -- proj i o product (prod p (FObj Γ) proj) q
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
361 -- ≈⟨ pif=q (prod p (FObj Γ) proj) q ⟩
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
362 -- q i
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
363 -- ∎
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
364
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
365
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
366 limit-ε :
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
367 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
368 → IProduct {c₁'} A (Obj I) p ai pi )
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
369 ( lim p : Obj A ) ( e : Hom A lim p )
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
370 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
371 NTrans I A (K A I lim) Γ
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
372 limit-ε prod lim p e proj = record {
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
373 TMap = tmap ;
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
374 isNTrans = record {
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
375 commute = commute1
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
376 }
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
377 } where
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
378 tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
379 tmap i = A [ proj i o e ]
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
380 commute1 : {i j : Obj I} {f : Hom I i j} →
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
381 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
382 commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
383 FMap Γ f o tmap i
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
384 ≈⟨⟩
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
385 FMap Γ f o ( proj i o e )
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
386 ≈⟨ assoc ⟩
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
387 ( FMap Γ f o proj i ) o e
289
7dc163c026b7 move to iProduct axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 288
diff changeset
388 ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ) proj ) {j} ) ⟩
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
389 proj j o e
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
390 ≈↑⟨ idR ⟩
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
391 (proj j o e ) o id1 A lim
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
392 ≈⟨⟩
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
393 tmap j o FMap (K A I lim) f
288
04f598e500de give up ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 287
diff changeset
394
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
395
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
396 limit-from :
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
397 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
281
dbd2044add2a limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
398 → IProduct {c₁'} A (Obj I) p ai pi )
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
399 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g )
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
400 ( lim p : Obj A ) -- limit to be made
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
401 ( e : Hom A lim p ) -- existing of equalizer
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
402 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually )
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
403 → Limit A I Γ lim ( limit-ε prod lim p e proj )
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
404 limit-from prod eqa lim p e proj = record {
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
405 limit = λ a t → limit1 a t ;
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
406 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
407 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
408 } where
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
409 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
410 limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
411 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
412 A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
413 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
414 TMap (limit-ε prod lim p e proj ) i o limit1 a t
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
415 ≈⟨⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
416 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
417 ≈↑⟨ assoc ⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
418 proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom )
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
419 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
420 proj i o product (prod p (FObj Γ) proj) (TMap t)
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
421 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
422 TMap t i
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
423
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
424 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim}
290
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 289
diff changeset
425 → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) →
282
c831abfa9bf4 limit on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
426 A [ limit1 a t ≈ f ]
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
427 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
428 limit1 a t
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
429 ≈⟨⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
430 k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
431 ≈⟨ Equalizer.uniqueness (eqa e (id1 A p) (id1 A p )) ( begin
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
432 e o f
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
433 ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
434 product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e o f ) ) )
284
4be696e3fd94 comutativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
435 ≈⟨ ip-cong (prod p (FObj Γ) proj) ( λ i → begin
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
436 proj i o ( e o f )
284
4be696e3fd94 comutativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
437 ≈⟨ assoc ⟩
285
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
438 ( proj i o e ) o f
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
439 ≈⟨ lim=t {i} ⟩
46d4ad55b948 commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 284
diff changeset
440 TMap t i
284
4be696e3fd94 comutativity remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 283
diff changeset
441 ∎ ) ⟩
283
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
442 product (prod p (FObj Γ) proj) (TMap t)
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
443 ∎ ) ⟩
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
444 f
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
445
5492a0681f55 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
446
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
447 ----
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
448 --
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
449 -- Adjoint functor preserves limits
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
450 --
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
451 --
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
452
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
453 open import Category.Cat
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
454
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
455 ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
456 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) →
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
457 ( U : Functor B A) → NTrans I A ( K A I (FObj U lim) ) (U ○ Γ)
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
458 ta1 B Γ lim tb limit U = record {
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
459 TMap = TMap (Functor*Nat I A U tb) ;
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
460 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
461 FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
462 ≈⟨ nat ( Functor*Nat I A U tb ) ⟩
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
463 TMap (Functor*Nat I A U tb) b o FMap (U ○ K B I lim) f
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
464 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
465 TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
466
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
467 } }
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
468
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
469 adjoint-preseve-limit :
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
470 { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B )
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
471 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) →
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
472 { U : Functor B A } { F : Functor A B }
293
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
473 { η : NTrans A A identityFunctor ( U ○ F ) }
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
474 { ε : NTrans B B ( F ○ U ) identityFunctor } →
293
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
475 ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb limit U )
292
a84fab7cf46a on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
476 adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record {
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
477 limit = λ a t → limit1 a t ;
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
478 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
479 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
480 } where
292
a84fab7cf46a on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
481 ta = ta1 B Γ lim tb limitb U
293
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
482 tfmap : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K B I (FObj F a)) i) (FObj Γ i)
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
483 tfmap a t i = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ]
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
484 tF : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → NTrans I B (K B I (FObj F a)) Γ
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
485 tF a t = record {
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
486 TMap = tfmap a t ;
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
487 isNTrans = record { commute = λ {a'} {b} {f} → let open ≈-Reasoning (B) in begin
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
488 FMap Γ f o tfmap a t a'
294
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
489 ≈⟨⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
490 FMap Γ f o ( TMap ε (FObj Γ a') o FMap F (TMap t a'))
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
491 ≈⟨ assoc ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
492 (FMap Γ f o TMap ε (FObj Γ a') ) o FMap F (TMap t a')
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
493 ≈⟨ car (nat ε) ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
494 (TMap ε (FObj Γ b) o FMap (F ○ U) (FMap Γ f) ) o FMap F (TMap t a')
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
495 ≈↑⟨ assoc ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
496 TMap ε (FObj Γ b) o ( FMap (F ○ U) (FMap Γ f) o FMap F (TMap t a') )
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
497 ≈↑⟨ cdr ( distr F ) ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
498 TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) )
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
499 ≈⟨ cdr ( fcong F (nat t) ) ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
500 TMap ε (FObj Γ b) o FMap F (A [ TMap t b o FMap (K A I a) f ])
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
501 ≈⟨⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
502 TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K A I a) b) ])
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
503 ≈⟨ cdr ( fcong F (IsCategory.identityR (Category.isCategory A))) ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
504 TMap ε (FObj Γ b) o FMap F (TMap t b )
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
505 ≈↑⟨ idR ⟩
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
506 ( TMap ε (FObj Γ b) o FMap F (TMap t b)) o id1 B (FObj F (FObj (K A I a) b))
db4ecbdbf9e9 limit1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
507 ≈⟨⟩
293
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
508 tfmap a t b o FMap (K B I (FObj F a)) f
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
509
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
510 } }
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
511 limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim)
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
512 limit1 a t = A [ FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a ]
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
513 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} →
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
514 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]
295
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
515 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
516 TMap ta i o limit1 a t
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
517 ≈⟨⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
518 FMap U ( TMap tb i ) o ( FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a )
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
519 ≈⟨ assoc ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
520 ( FMap U ( TMap tb i ) o FMap U (limit limitb (FObj F a) (tF a t ))) o TMap η a
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
521 ≈↑⟨ car ( distr U ) ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
522 FMap U ( B [ TMap tb i o limit limitb (FObj F a) (tF a t ) ] ) o TMap η a
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
523 ≈⟨ car ( fcong U ( t0f=t limitb ) ) ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
524 FMap U (TMap (tF a t) i) o TMap η a
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
525 ≈⟨⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
526 FMap U ( B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] ) o TMap η a
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
527 ≈⟨ car ( distr U ) ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
528 ( FMap U ( TMap ε (FObj Γ i)) o FMap U ( FMap F (TMap t i) )) o TMap η a
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
529 ≈↑⟨ assoc ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
530 FMap U ( TMap ε (FObj Γ i) ) o ( FMap U ( FMap F (TMap t i) ) o TMap η a )
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
531 ≈⟨ cdr ( nat η ) ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
532 FMap U (TMap ε (FObj Γ i)) o ( TMap η (FObj U (FObj Γ i)) o FMap (identityFunctor {_} {_} {_} {A}) (TMap t i) )
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
533 ≈⟨ assoc ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
534 ( FMap U (TMap ε (FObj Γ i)) o TMap η (FObj U (FObj Γ i))) o TMap t i
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
535 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ) ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
536 id1 A (FObj (U ○ Γ) i) o TMap t i
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
537 ≈⟨ idL ⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
538 TMap t i
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
539
296
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
540 -- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i ) o f ≈ TMap t i
293
fb0ab8c72e15 limit defined.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
541 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)}
291
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
542 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) →
c8e26650ddf9 limit preserving ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 290
diff changeset
543 A [ limit1 a t ≈ f ]
295
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
544 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
545 limit1 a t
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
546 ≈⟨⟩
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
547 FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a
296
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
548 ≈⟨ car ( fcong U (limit-uniqueness limitb ( λ {i} → lemma1 i) )) ⟩
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
549 FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a
297
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
550 ≈⟨ car (distr U ) ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
551 ( (FMap U (TMap ε lim)) o (FMap U ( FMap F f )) ) o TMap η a
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
552 ≈⟨ sym assoc ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
553 (FMap U (TMap ε lim)) o ((FMap U ( FMap F f )) o TMap η a )
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
554 ≈⟨ cdr (nat η) ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
555 (FMap U (TMap ε lim)) o ((TMap η (FObj U lim )) o f )
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
556 ≈⟨ assoc ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
557 ((FMap U (TMap ε lim)) o (TMap η (FObj U lim))) o f
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
558 ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
559 id (FObj U lim) o f
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
560 ≈⟨ idL ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
561 f
296
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
562 ∎ where
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
563 lemma1 : (i : Obj I) → B [ B [ TMap tb i o B [ TMap ε lim o FMap F f ] ] ≈ TMap (tF a t) i ]
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
564 lemma1 i = let open ≈-Reasoning (B) in begin
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
565 TMap tb i o (TMap ε lim o FMap F f)
297
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
566 ≈⟨ assoc ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
567 ( TMap tb i o TMap ε lim ) o FMap F f
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
568 ≈⟨ car ( nat ε ) ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
569 ( TMap ε (FObj Γ i) o FMap F ( FMap U ( TMap tb i ))) o FMap F f
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
570 ≈↑⟨ assoc ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
571 TMap ε (FObj Γ i) o ( FMap F ( FMap U ( TMap tb i )) o FMap F f )
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
572 ≈↑⟨ cdr ( distr F ) ⟩
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
573 TMap ε (FObj Γ i) o FMap F ( A [ FMap U ( TMap tb i ) o f ] )
537570f6a44f limit preservation proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
574 ≈⟨ cdr ( fcong F (lim=t {i}) ) ⟩
296
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
575 TMap ε (FObj Γ i) o FMap F (TMap t i)
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
576 ≈⟨⟩
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
577 TMap (tF a t) i
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
578
295
26e8f0227ebd limit equation done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
579
296
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
580
bba60d843462 lemma1 will be proved
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
581