annotate pullback.agda @ 496:5c7908202d5a

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