Product, Pullback and Limit
Menu Menutop : Agda による圏論入門 pullback.agda
Product
Product は、直積に相当する概念ですが、ここでは二つの射π1とπ2に対して定義します。
c
f | g
|f×g
v
a <-------- ab ---------→ b
π1 π2
与えるのは a,b,ab という三つの対象と、π1 : ab → a, π2 : ab → b という射です。 cat-utility.agda
record IsProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A)
( π1 : Hom A ab a )
( π2 : Hom A ab b )
: Set (ℓ ⊔ (c₁ ⊔ c₂)) where
field
_×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab
π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ]
π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ]
uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ]
×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ]
record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A )
: Set (ℓ ⊔ (c₁ ⊔ c₂)) where
field
product : Obj A
π1 : Hom A product a
π2 : Hom A product b
isProduct : IsProduct A a b product π1 π2
Prodcut は二つの射 f: c → a, g : c → b から f × g という射を作ることができます。a と b への射の組(f,g)でできることは、一つの射 f × g で代表できるみたいなものだと思います。c から a, b への二つの射があれば、f×g という射がただ一つ定まるという言い方になります。
f, g は、π1fxg=f と π2fxg=g の二つの等式で再現できます。これが射影になります。
任意の ab への射 h に対して、射影の直積が h になるというように uniquness を表しています。
直積の個々の要素が等しければ、直積も等しいというのが ×-cong です。
別な形の uniquness : π1 × π2 ≈ id1 A ab を示すこともできます。
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 ) →
A [ _×_ prod π1 π2 ≈ id1 A ab ]
lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin
_×_ prod π1 π2
≈↑⟨ ×-cong prod idR idR ⟩
_×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ])
≈⟨ Product.uniqueness prod ⟩
id1 A ab
∎
Pullback and Limit
Pullback は、
f
a ------→ c
^ ^
π1 | |g
| |
ab ------→ b
^ π2
|
d
Equalizer と Product を合わせたものになっていて、実際、Equalizer と Product が存在すれば、それらを組み合わせて構築することができます。定義は以下のようにしました。
a,b,c,ab という4つの対象と4つの射があります。ここで、a, b への任意の射に対して、ab への射がただ一つ定まり、可換図が成立するというわけです。
record IsPullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c ab : Obj A}
( f : Hom A a c ) ( g : Hom A b c )
( π1 : Hom A ab a ) ( π2 : Hom A ab b )
: Set (ℓ ⊔ (c₁ ⊔ c₂)) where
field
commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ]
pullback : { 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 ab
π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] }
→ A [ A [ π1 o pullback eq ] ≈ π1' ]
π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] }
→ A [ A [ π2 o pullback eq ] ≈ π2' ]
uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] }
→ { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] }
→ { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] }
→ A [ pullback eq ≈ p' ]
record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c : Obj A}
( f : Hom A a c ) ( g : Hom A b c )
: Set (ℓ ⊔ (c₁ ⊔ c₂)) where
field
ab : Obj A
π1 : Hom A ab a
π2 : Hom A ab b
isPullback : IsPullback A f g π1 π2
p が ab への射を提供する写像です。可換性は、π1p=π1 と π2p=π2 です。uniquness は Product とは異なり、ab への射p' に対する可換図が成立すれば、それはp と 等しいとう風に書いています。
可換性は、もともと f,g, π1, π2 に成立する commute と、与えられたπ1'とπ2' と Pullback p に対して成立するπ1p=π1 と π2p=π2 の二つです。
Equalizer と同じように、ab は前もって与えています。
Pullback を Prodcut とEqualizerから作る
f
a ------→ c
^ ^
π1 | |g
| |
ab ------→ b
^ π2
|
| e = equalizer (f π1) (g π1)
|
d <------------------ d'
k (π1' × π2' )
Pullback は Equalizer と Prodocut をつなぎあわせたような形をしているので、Pullback 射を、Equalizer と Product から作ることができます。
pullback-from : {a b c : Obj A}
( f : Hom A a c ) ( g : Hom A b c )
( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g )
( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g
pullback-from {a} {b} {c} f g eqa prod0 = record {
ab = d ;
π1 = A [ π1 o e ] ;
π2 = A [ π2 o e ] ;
isPullback = record {
commute = commute1 ;
pullback = p1 ;
π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ;
π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ;
uniqueness = uniqueness1
}
} where
axb : Obj A
axb = Product.product (prod0 a b)
π1 : Hom A axb a
π1 = Product.π1 (prod0 a b )
π2 : Hom A axb b
π2 = Product.π2 (prod0 a b )
d : Obj A
d = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ]))
commute1 : A [ A [ f o A [ π1 o ? ] ]
≈ A [ g o A [ π2 o ? ] ] ]
commute1 = ?
前もって、答えがわからないと証明も書きようがないので、pullback の e を見つけるのが問題になります。
Pullback 自体は record を作れば良いわけなので、e は取り敢えず ? にして置いて、要求される式を書いていきます。
commute1 : A [ A [ f o A [ π1 o ? ] ]
≈ A [ g o A [ π2 o ? ] ] ]
ということになります。これは、equalizer の
fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
に似ているので、? は、おそらく equalizer でしょう。だとすれば、d'からd への射 p1 は、equalizer の解 k でしょう。k には、条件があるので、それも示す必要があります。それは、とりあえず、lemma1 とでもしておいて。
lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
lemma1 {d'} { π1' } { π2' } eq = ?
p1 {d'} { π1' } { π2' } eq =
let open ≈-Reasoning (A) in k (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ))) (_×_ prod π1' π2' ) ( lemma1 eq )
としてみます。eqa は Equalizer を与える写像で、prod は Product を与える写像で、どちらも定理の仮定です。
( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g )
( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g
あとは頑張って証明すればよいだけです。
Pullback の元の可換性は、Equalizer の fe=ge から導出できます。
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 ])) ] ] ]
commute1 = let open ≈-Reasoning (A) in
begin
f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
≈⟨ assoc ⟩
( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
≈↑⟨ assoc ⟩
g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
∎
p1 の仮定 lemma1 、つまり Equalizer の filed ek=f は、
p1 {d'} { π1' } { π2' } eq =
let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ?
とすれば、
?0 : (A Category.≈ A [ A [ f o π1 ] o (prod × π1') π2' ])
(A [ A [ g o π2 ] o (prod × π1') π2' ])
だと Agda が教えてくれます。これをそのまま使って、使える仮定 (p1 の引数全部 ) を付け加えます。
lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
これが意味するところを理解しなくても、証明すれば良いわけです。(prod × π1') π2' は、infix operator がおかしなことになっていますが、π1'× π2' ということです。これは Agda の構文の良くないところ。
lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in
begin
( f o π1 ) o (prod × π1') π2'
≈↑⟨ assoc ⟩
f o ( π1 o (prod × π1') π2' )
≈⟨ cdr (π1fxg=f prod) ⟩
f o π1'
≈⟨ eq ⟩
g o π2'
≈↑⟨ cdr (π2fxg=g prod) ⟩
g o ( π2 o (prod × π1') π2' )
≈⟨ assoc ⟩
( g o π2 ) o (prod × π1') π2'
∎
π1fxg=f とかは、Product を作った時に、そんな変な名前にしてしまったのでした。こちらでは Equalizer の性質は使わずに、Product の射影だけを使っています。eq は、lemma の仮定
f o π1' ≈ g o π2'
です。これが成立する π1' , π2' の組に対して、pullback を作っていたのでした。
これで、pullback p1 が定義できました。あとは、要求される性質を証明していけばよいだけです。equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) は、 e のことなので、一直線に証明できます。
π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' ] ]} →
A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
begin
( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
≈⟨⟩
( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
≈↑⟨ assoc ⟩
π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
π1 o (_×_ prod π1' π2' )
≈⟨ π1fxg=f prod ⟩
π1'
∎
π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' ] ]} →
A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
begin
( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
≈⟨⟩
( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
≈↑⟨ assoc ⟩
π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
π2 o (_×_ prod π1' π2' )
≈⟨ π2fxg=g prod ⟩
π2'
∎
そして、uniquness を証明します。
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' ] ]} →
{eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
{eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
A [ p1 eq ≈ p' ]
uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
begin
p1 eq
≈⟨⟩
k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin
e o p'
≈⟨⟩
equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
≈↑⟨ Product.uniqueness prod ⟩
(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'))
≈⟨ ×-cong prod (assoc) (assoc) ⟩
(prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
(A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
≈⟨ ×-cong prod eq1 eq2 ⟩
((prod × π1') π2')
∎ ) ⟩
p'
∎
そのまま、Equalizer と Product の uniquness に対応しています。
Product
ここで作った Product はπ1とπ2の二つの積でした。これを任意個の射の積に拡張したいと思います。引数に相当する集合 I を考えて、A の対象 Obj A への射を作ります。
ai : I → Obj A
そして、Product の対象 p から、ai i への射を引数 I からの射で指し示します。
pi : (i : I ) → Hom A p ( ai i )
I が何かは規定してないので、要素二個だったり無限個だったり、あるいは可算個だったりします。
Product の行き先 p と ai, pi の写像を与えると、任意のAの対象 q に対して、
product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
q から p への射があって、さらに q から ai i への射の集合に対して、
qi : (i : I) → Hom A q (ai i)
以下の等式が成立します。
pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ]
qi i を必ず Product 経由にできるみたいな感じです。
そして、そういうものがあったとすると、それは唯一に決まります。
ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p )
→ ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] )
→ A [ product' ≈ product qi ]
これを直接要求せずに、要素二個に対する Product の uniquness
(π1 p ) × ( π2 p) = p
に相当する、
ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
こちらを要求します。これを使って、 ip-uniqueness1 を証明することができます。
ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin
product'
≈↑⟨ ip-uniqueness ⟩
product (λ i₁ → A [ pi i₁ o product' ])
≈⟨ ip-cong ( λ i → begin
pi i o product'
≈⟨ eq {i} ⟩
qi i
∎ ) ⟩
product qi
∎
あと、いつものように congを定義します。まとめると、
-----
--
-- product on arbitrary index
--
record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c)
( p : Obj A ) -- product
( ai : I → Obj A ) -- families
( pi : (i : I ) → Hom A p ( ai i ) ) -- projections
: Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
field
product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ]
ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
→ ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
-- another form of uniquness
ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p )
→ ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] )
→ A [ product' ≈ product qi ]
ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin
product'
≈↑⟨ ip-uniqueness ⟩
product (λ i₁ → A [ pi i₁ o product' ])
≈⟨ ip-cong ( λ i → begin
pi i o product'
≈⟨ eq {i} ⟩
qi i
∎ ) ⟩
product qi
∎
となります。
Limit
圏のLimit は、Equalizer や Product を汎用にしたものです。任意個の Product を作る時には写像を使いましたが、Equalizer とかの可換図を任意の有向グラフにします。有向グラフとは、
対象があり、それを結ぶ射がある
わけなので、これは圏そのものです。つまり、引数になる圏Iから、圏Aへの関手を定義すると、それはAの中のグラフを定義することになります。この関手を
Γ : Functor I A
とします。このグラフに対して 任意のAの対象 a から Limit である対象 a0 への射 limit が存在します。
Equalizer, Product などの条件になる可換性は、自然変換の可換性として定義します。Γは関手ですが、そこに自然変換 t を定義しますが、自然変換は関手から関手なので相手(Functor I A)を定義する必要があります。ただ一つの対象a と a 上の id だけを返す定数関手を使います。
-- Constancy Functor
K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' )
→ ( a : Obj A ) → Functor I A
K A I a = record {
FObj = λ i → a ;
FMap = λ f → id1 A a ;
isFunctor = let open ≈-Reasoning (A) in record {
≈-cong = λ f=g → refl-hom
; identity = refl-hom
; distr = sym idL
}
}
これが関手なのは自明です。この K からΓへの自然変換があると、
t0 : NTrans I A ( K A I a0 ) Γこのt0 の可換性 は i j : Obj I の射 f : Hom I i j に対して、
FMap Γ f o TMap t0 i ≈ TMap t0 j o FMap (K A I lim) f
つまり、
FMap Γ f o TMap t0 i ≈ TMap t0 j
になります。要素二つのProductだったら、
π1 o ( f × g ) ≈ f
に相当します。任意の個数のProductだったら、
pi i o product qi ≈ qi i
でした。圏I、Functor Γ、自然変換 t0 を工夫することにより、様々な Product や Equliazer に相当するものを作れることがわかります。
Limit が存在すると、こういう性質を満たす射と対象、つまり自然変換 t : K → Γ に対して、
t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
となります。まとめると、
record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
( a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
field
limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ]
となります。
Limit が存在すれば、up to iso に unique になります。つまり、iso-l, iso-r の二つの射があり、組み合わせると id になります。
iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' )
→ Hom A a0 a0'
iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' )
→ Hom A a0' a0
iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) → ∀{ i : Obj I } →
A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ]
iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin
limit lim' a0 t0 o limit lim a0' t0'
≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin
TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
≈⟨ assoc ⟩
( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0'
≈⟨ car ( t0f=t lim' ) ⟩
TMap t0 i o limit lim a0' t0'
≈⟨ t0f=t lim ⟩
TMap t0' i
∎) ) ⟩
limit lim' a0' t0'
≈⟨ limit-uniqueness lim' idR ⟩
id a0'
∎
Limit を随伴関手として定義することもできます。K を A から A^I への関手 KI に拡張します。
KI : A → A^I
が右随伴関手を持てば、Limit が存在します。
A^I は、I から A への関手圏ですから、射は自然変換です。
open import CatExponetial
open Functor
--------------------------------
--
-- Contancy Functor
KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I )
KI { c₁'} {c₂'} {ℓ'} I = record {
FObj = λ a → K A I a ;
FMap = λ f → record { -- NTrans I A (K A I a) (K A I b)
TMap = λ a → f ;
isNTrans = record {
commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
}
} ;
isFunctor = let open ≈-Reasoning (A) in record {
≈-cong = λ f=g {x} → f=g
; identity = refl-hom
; distr = refl-hom
}
} where
commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ]
commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin
FMap (K A I b') f₁ o f
≈⟨ idL ⟩
f
≈↑⟨ idR ⟩
f o FMap (K A I a') f₁
∎
A^Iの対象は関手なのでK A I a で良いのですが、射は自然変換を作らないといけません。でも、対象はa と id を返す K なので、KI の射の写像 FMap KI は f そのもので構いません。
まず Limit があれば、A → A^I の KI に対する co Universal Mapping の解があることを示します。
-- limit gives co universal mapping ( i.e. adjunction )
--
-- F = KI I : Functor A (A ^ I)
-- U = λ b → A0 (lim b {a0 b} {t0 b}
-- ε = λ b → T0 ( lim b {a0 b} {t0 b} )
--
-- a0 : Obj A and t0 : NTrans K Γ come from the limit
limit2couniv :
( lim : ( Γ : Functor I A ) → Limit I A Γ )
→ coUniversalMapping A ( A ^ I ) (KI I)
limit2couniv lim = record {
U = λ b → a0 ( lim b) ;
ε = λ b → t0 (lim b) ;
_*' = λ {b} {a} k → limit (isLimit (lim b )) a k ;
iscoUniversalMapping = record { couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
couniquness = couniquness2
}
} where
couniversalMapping1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
A ^ I [ A ^ I [ t0 (lim b) o FMap (KI I) (limit (isLimit (lim b)) a f) ] ≈ f ]
couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin
TMap (t0 (lim b )) i o TMap ( FMap (KI I) (limit (isLimit (lim b )) a f) ) i
≈⟨⟩
TMap (t0 (lim b)) i o (limit (isLimit (lim b)) a f)
≈⟨ t0f=t (isLimit (lim b)) ⟩
TMap f i -- i comes from ∀{i} → B [ TMap f i ≈ TMap g i ]
∎
couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (a0 (lim b ))} →
( ∀ { i : Obj I } → A [ A [ TMap (t0 (lim b )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] )
→ A [ limit (isLimit (lim b )) a f ≈ g ]
couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin
limit (isLimit (lim b )) a f
≈⟨ limit-uniqueness (isLimit ( lim b )) lim-g=f ⟩
g
∎
問題を書き下してみると、
TMap (t0 b) i o (limit (lim b) a f) ≈ TMap f i
が、そのまま解の条件になっていることがわかります。
逆に Universal mapping があれば、それから Limit を作ることができます。
univ2limit :
( univ : coUniversalMapping A (A ^ I) (KI I) ) →
( Γ : Functor I A ) → Limit I A Γ
univ2limit univ Γ = record {
a0 = (coUniversalMapping.U univ ) Γ ;
t0 = (coUniversalMapping.ε univ ) Γ ;
isLimit = record {
limit = λ a t → limit1 a t ;
t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
}
} where
U : Obj (A ^ I) → Obj A
U b = coUniversalMapping.U univ b
ε : ( b : Obj (A ^ I ) ) → NTrans I A (FObj (KI I) (U b)) b
ε b = coUniversalMapping.ε univ b
limit1 : (a : Obj A) → NTrans I A (FObj (KI I) a) Γ → Hom A a (U Γ)
limit1 a t = coUniversalMapping._*' univ {_} {a} t
t0f=t1 : {a : Obj A} {t : NTrans I A (K I A a) Γ} {i : Obj I} →
A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
TMap (ε Γ) i o limit1 a t
≈⟨⟩
TMap (ε Γ) i o coUniversalMapping._*' univ t
≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {a} {t} ⟩
TMap t i
∎
limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a (U Γ)}
→ ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin
coUniversalMapping._*' univ t
≈⟨ ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t ⟩
f
∎
直接、随伴関手を作るのは、可能ではありますが、煩雑ですし、普遍問題の解から随伴関手を作るのをなぞることになります。
limit from equalizer and product
Limit は pullback と同じように Equalizer と IProduct から作ることができます。IProduct は任意個の積を表します。
--
-- limit from equalizer and product
--
-- Γu
-- → Γj → Γk ←
-- / ↑ ↑ \
-- proj j / | | \ proj k
-- / μu| |μu \ Equalizer have to be independent from j and k
-- | | | | so we need products of Obj I and Hom I
-- |product of Hom I |
-- | ↑ ↑ | K u = id lim
-- | f(id)} | |
-- | | |g(Γ) | lim = K j -----------→ K k = lim
-- | | | | | u |
-- \ | | / proj j o e = ε j | | ε k = proj k o e
-- product of Obj I μ u o g o e | | μ u o f o e
-- ↑ | |
-- | e = equalizer f g | |
-- | ↓ ↓
-- lim ←---------------- d' Γ j ----------→ Γ k
-- k ( product pi ) Γ u
-- Γ u o ε j = ε k
--
Limit に出てくるたくさんの可換性を Equalize と IProductの可換性に帰着させる必要があります。
Limit のIndex圏の対象全部の積を作ります。
p0 : Obj A
p0 = iprod (prod (FObj Γ))
少しインチキなんですが、Index圏の射全体を record で積として表してしまいます。本当は IProduct で作る必要があります。
-- homprod should be written by IProduct
-- If I is locally small, this is iso to a set
record homprod {c : Level } : Set (suc c₁' ⊔ suc c₂' ) where
field
hom-j : Obj I
hom-k : Obj I
hom : Hom I hom-j hom-k
open homprod
Homprod : {j k : Obj I} (u : Hom I j k) → homprod {c₁}
Homprod {j} {k} u = record {hom-j = j ; hom-k = k ; hom = u}
Homprod がLimitのindex圏の射全体の積つまり、全体の代表です。Fcod は射を与えると Index凾手で射影された射のcodomain を取ってくる写像です。
Fcod : homprod {c₁} → Obj A
Fcod = λ u → FObj Γ ( hom-k u )
これで、Index圏から関手F通じて示された対象と射を一度に扱うことができるわけです。
limit-from :
( prod : {c : Level} { I : Set c } → ( ai : I → Obj A ) → IProduct I A ai )
( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g )
→ Limit I A Γ
limit-from prod eqa = record {
a0 = d ;
t0 = cone-ε ;
isLimit = record {
limit = λ a t → cone1 a t ;
t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
}
} where
p0 : Obj A
p0 = iprod (prod (FObj Γ))
Fcod : homprod {c₁} → Obj A
Fcod = λ u → FObj Γ ( hom-k u )
f : Hom A p0 (iprod (prod Fcod))
f = iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u ))
g : Hom A p0 (iprod (prod Fcod))
g = iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] )
equ-ε : Equalizer A g f
equ-ε = eqa g f
d : Obj A
d = equalizer-c equ-ε
e : Hom A d p0
e = equalizer equ-ε
equ = isEqualizer equ-ε
-- projection of the product of Obj I
proj : (i : Obj I) → Hom A p0 (FObj Γ i)
proj = pi ( prod (FObj Γ) )
prodΓ = isIProduct ( prod (FObj Γ) )
-- projection of the product of Hom I
μ : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u))
μ u = pi (prod Fcod ) (Homprod u)
f と g が equlizer を構成する二つの射です。
この equalizerを使って、 Γに対応する自然変換(cone)を作ります。これは Limit の可換性の条件をすべて含んでいる自然変換になります。
-- projection of the product of Obj I
proj : (i : Obj I) → Hom A p0 (FObj Γ i)
proj = pi ( prod (FObj Γ) )
prodΓ = isIProduct ( prod (FObj Γ) )
-- projection of the product of Hom I
μ : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u))
μ u = pi (prod Fcod ) (Homprod u)
cone-ε : NTrans I A (K I A (equalizer-c equ-ε ) ) Γ
cone-ε = record {
TMap = λ i → tmap i ;
isNTrans = record { commute = commute1 }
} where
tmap : (i : Obj I) → Hom A (FObj (K I A d) i) (FObj Γ i)
tmap i = A [ proj i o e ]
commute1 : {j k : Obj I} {u : Hom I j k} →
A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K I A d) u ] ]
commute1 {j} {k} {u} = let open ≈-Reasoning (A) in begin
FMap Γ u o tmap j
≈⟨⟩
FMap Γ u o ( proj j o e )
≈⟨ assoc ⟩
( FMap Γ u o pi (prod (FObj Γ)) j ) o e
≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩
( μ u o g ) o e
≈↑⟨ assoc ⟩
μ u o (g o e )
≈⟨ cdr ( fe=ge (isEqualizer equ-ε )) ⟩
μ u o (f o e )
≈⟨ assoc ⟩
(μ u o f ) o e
≈⟨ car ( pif=q (isIProduct (prod Fcod ))) ⟩
pi (prod (FObj Γ)) k o e
≈⟨⟩
proj k o e
≈↑⟨ idR ⟩
(proj k o e ) o id1 A d
≈⟨⟩
tmap k o FMap (K I A d) u
∎
作成する Limit の対象は d で、cone-ε がその自然変換です。
もし、Limit と同じ可換性を持つ対象aと自然変換tがあれば、それへんの unique な射と自然変換があるというのが Limit要請です。
-- an arrow to our product of Obj I ( is an equalizer because of commutativity of t )
h : {a : Obj A} → (t : NTrans I A (K I A a) Γ ) → Hom A a p0
h t = iproduct prodΓ (TMap t)
fh=gh : (a : Obj A) → (t : NTrans I A (K I A a) Γ ) →
A [ A [ g o h t ] ≈ A [ f o h t ] ]
fh=gh a t = ?
cone1 : (a : Obj A) → NTrans I A (K I A a) Γ → Hom A a d
cone1 a t = k equ (h t) ( fh=gh a t )
それは積と equalizer から作ることになります。そのためには equlizer の条件である二つの射の可換性を示す必要があります。これは、cone を作った時の計算を逆にたどるような感じで証明できます。
fh=gh : (a : Obj A) → (t : NTrans I A (K I A a) Γ ) →
A [ A [ g o h t ] ≈ A [ f o h t ] ]
fh=gh a t = let open ≈-Reasoning (A) in begin
g o h t
≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( g o h t ))
≈⟨ ip-cong (isIProduct (prod Fcod)) ( λ u → begin
pi (prod Fcod) u o ( g o h t )
≈⟨ assoc ⟩
( pi (prod Fcod) u o g ) o h t
≈⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩
(FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ) o h t
≈↑⟨ assoc ⟩
FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u) o h t )
≈⟨ cdr ( pif=q prodΓ ) ⟩
FMap Γ (hom u) o TMap t (hom-j u)
≈⟨ IsNTrans.commute (isNTrans t) ⟩
TMap t (hom-k u) o id1 A a
≈⟨ idR ⟩
TMap t (hom-k u)
≈↑⟨ pif=q prodΓ ⟩
pi (prod (FObj Γ)) (hom-k u) o h t
≈↑⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩
(pi (prod Fcod) u o f ) o h t
≈↑⟨ assoc ⟩
pi (prod Fcod) u o ( f o h t )
∎
) ⟩
iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( f o h t ))
≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
f o h t
∎
Adjoint functor preserves limits
随伴関手の重要な性質として Limit が保存されるというのがあります。Limit が存在する B から、随伴関手を使って、A のLimit を作ります。
Γは、向こう側(A)では U ○ Γ になります。
adjoint-preseve-limit :
{ c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit I B Γ ) →
( adj : Adjunction A B ) → Limit I A (Adjunction.U adj ○ Γ)
adjoint-preseve-limit B Γ limitb adj = record {
a0 = FObj U lim ;
t0 = ta1 B Γ lim tb U ;
isLimit = ? }
Limit は U で対応するに決まっているので、 問題は、自然変換 ta1 の構成です。
ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B )
( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) →
( U : Functor B A) → NTrans I A ( K I A (FObj U lim) ) (U ○ Γ)
ta1 B Γ lim tb U = record {
TMap = TMap (Functor*Nat I A U tb) ;
isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin
FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a
≈⟨ nat ( Functor*Nat I A U tb ) ⟩
TMap (Functor*Nat I A U tb) b o FMap (U ○ K I B lim) f
≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
TMap (Functor*Nat I A U tb) b o FMap (K I A (FObj U lim)) f
∎
} }
随伴関手には様々な関手と自然変換があるので、便利ですが、ここでは、tb の可換性のみで証明できます。
実際の証明は複雑で長いわけですが、証明自体は一直線に終わります。
adjoint-preseve-limit :
{ c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit I B Γ ) →
( adj : Adjunction A B ) → Limit I A (Adjunction.U adj ○ Γ)
adjoint-preseve-limit B Γ limitb adj = record {
a0 = FObj U lim ;
t0 = ta1 B Γ lim tb U ;
isLimit = record {
limit = λ a t → limit1 a t ;
t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
}
} where
U : Functor B A
U = Adjunction.U adj
F : Functor A B
F = Adjunction.F adj
η : NTrans A A identityFunctor ( U ○ F )
η = Adjunction.η adj
ε : NTrans B B ( F ○ U ) identityFunctor
ε = Adjunction.ε adj
ta = ta1 B Γ (a0 limitb) (t0 limitb) U
tb = t0 limitb
lim = a0 limitb
tfmap : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K I B (FObj F a)) i) (FObj Γ i)
tfmap a t i = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ]
tF : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → NTrans I B (K I B (FObj F a)) Γ
tF a t = record {
TMap = tfmap a t ;
isNTrans = record { commute = λ {a'} {b} {f} → let open ≈-Reasoning (B) in begin
FMap Γ f o tfmap a t a'
≈⟨⟩
FMap Γ f o ( TMap ε (FObj Γ a') o FMap F (TMap t a'))
≈⟨ assoc ⟩
(FMap Γ f o TMap ε (FObj Γ a') ) o FMap F (TMap t a')
≈⟨ car (nat ε) ⟩
(TMap ε (FObj Γ b) o FMap (F ○ U) (FMap Γ f) ) o FMap F (TMap t a')
≈↑⟨ assoc ⟩
TMap ε (FObj Γ b) o ( FMap (F ○ U) (FMap Γ f) o FMap F (TMap t a') )
≈↑⟨ cdr ( distr F ) ⟩
TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) )
≈⟨ cdr ( fcong F (nat t) ) ⟩
TMap ε (FObj Γ b) o FMap F (A [ TMap t b o FMap (K I A a) f ])
≈⟨⟩
TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K I A a) b) ])
≈⟨ cdr ( fcong F (idR1 A)) ⟩
TMap ε (FObj Γ b) o FMap F (TMap t b )
≈↑⟨ idR ⟩
( TMap ε (FObj Γ b) o FMap F (TMap t b)) o id1 B (FObj F (FObj (K I A a) b))
≈⟨⟩
tfmap a t b o FMap (K I B (FObj F a)) f
∎
} }
limit1 : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) )
limit1 a t = A [ FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a ]
t0f=t1 : {a : Obj A} {t : NTrans I A (K I A a) (U ○ Γ)} {i : Obj I} →
A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]
t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
TMap ta i o limit1 a t
≈⟨⟩
FMap U ( TMap tb i ) o ( FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a )
≈⟨ assoc ⟩
( FMap U ( TMap tb i ) o FMap U (limit (isLimit limitb) (FObj F a) (tF a t ))) o TMap η a
≈↑⟨ car ( distr U ) ⟩
FMap U ( B [ TMap tb i o limit (isLimit limitb) (FObj F a) (tF a t ) ] ) o TMap η a
≈⟨ car ( fcong U ( t0f=t (isLimit limitb) ) ) ⟩
FMap U (TMap (tF a t) i) o TMap η a
≈⟨⟩
FMap U ( B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] ) o TMap η a
≈⟨ car ( distr U ) ⟩
( FMap U ( TMap ε (FObj Γ i)) o FMap U ( FMap F (TMap t i) )) o TMap η a
≈↑⟨ assoc ⟩
FMap U ( TMap ε (FObj Γ i) ) o ( FMap U ( FMap F (TMap t i) ) o TMap η a )
≈⟨ cdr ( nat η ) ⟩
FMap U (TMap ε (FObj Γ i)) o ( TMap η (FObj U (FObj Γ i)) o FMap (identityFunctor {_} {_} {_} {A}) (TMap t i) )
≈⟨ assoc ⟩
( FMap U (TMap ε (FObj Γ i)) o TMap η (FObj U (FObj Γ i))) o TMap t i
≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ) ⟩
id1 A (FObj (U ○ Γ) i) o TMap t i
≈⟨ idL ⟩
TMap t i
∎
-- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i ) o f ≈ TMap t i
limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K I A a) (U ○ Γ)} {f : Hom A a (FObj U lim)}
→ ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) →
A [ limit1 a t ≈ f ]
limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin
limit1 a t
≈⟨⟩
FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a
≈⟨ car ( fcong U (limit-uniqueness (isLimit limitb) ( λ {i} → lemma1 i) )) ⟩
FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a -- Universal mapping
≈⟨ car (distr U ) ⟩
( (FMap U (TMap ε lim)) o (FMap U ( FMap F f )) ) o TMap η a
≈⟨ sym assoc ⟩
(FMap U (TMap ε lim)) o ((FMap U ( FMap F f )) o TMap η a )
≈⟨ cdr (nat η) ⟩
(FMap U (TMap ε lim)) o ((TMap η (FObj U lim )) o f )
≈⟨ assoc ⟩
((FMap U (TMap ε lim)) o (TMap η (FObj U lim))) o f
≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩
id (FObj U lim) o f
≈⟨ idL ⟩
f
∎ where
lemma1 : (i : Obj I) → B [ B [ TMap tb i o B [ TMap ε lim o FMap F f ] ] ≈ TMap (tF a t) i ]
lemma0 i = let open ≈-Reasoning (B) in begin
TMap tb i o (TMap ε lim o FMap F f)
≈⟨ assoc ⟩
( TMap tb i o TMap ε lim ) o FMap F f
≈⟨ car ( nat ε ) ⟩
( TMap ε (FObj Γ i) o FMap F ( FMap U ( TMap tb i ))) o FMap F f
≈↑⟨ assoc ⟩
TMap ε (FObj Γ i) o ( FMap F ( FMap U ( TMap tb i )) o FMap F f )
≈↑⟨ cdr ( distr F ) ⟩
TMap ε (FObj Γ i) o FMap F ( A [ FMap U ( TMap tb i ) o f ] )
≈⟨ cdr ( fcong F (lim=t {i}) ) ⟩
TMap ε (FObj Γ i) o FMap F (TMap t i)
≈⟨⟩
TMap (tF a t) i
∎
Next : system T