Mercurial > hg > Members > kono > Proof > category
view pullback.agda @ 444:59e47e75188f
complete connection for finite category
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 14 Oct 2016 19:12:01 +0900 |
| parents | f526f4b68565 |
| children | c375d8f93a2c |
line wrap: on
line source
-- Pullback from product and equalizer -- -- -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> ---- open import Category -- https://github.com/konn/category-agda open import Level module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where open import HomReasoning open import cat-utility -- -- Pullback from equalizer and product -- f -- a ------→ c -- ^ ^ -- π1 | |g -- | | -- ab ------→ b -- ^ π2 -- | -- | e = equalizer (f π1) (g π1) -- | -- d <------------------ d' -- k (π1' × π2' ) open Equalizer open IsEqualizer open Product open Pullback pullback-from : (a b c ab d : Obj A) ( f : Hom A a c ) ( g : Hom A b c ) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g ) ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) pullback-from a b c ab d f g π1 π2 e eqa prod = record { commute = commute1 ; p = 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 commute1 : A [ A [ f o A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] commute1 = let open ≈-Reasoning (A) in begin f o ( π1 o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ) ≈⟨ assoc ⟩ ( f o π1 ) o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ ( g o π2 ) o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ≈↑⟨ assoc ⟩ g o ( π2 o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ) ∎ 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' ∎ 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 p1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) π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 equalizer1 (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 equalizer1 (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 equalizer1 (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 equalizer1 (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' ∎ 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 equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → {eq2 : A [ A [ A [ π2 o equalizer1 (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) ≈⟨ IsEqualizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin e o p' ≈⟨⟩ equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' ≈↑⟨ Product.uniqueness prod ⟩ (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')) ≈⟨ ×-cong prod (assoc) (assoc) ⟩ (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) (A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) ≈⟨ ×-cong prod eq1 eq2 ⟩ ((prod × π1') π2') ∎ ) ⟩ p' ∎ -------------------------------- -- -- If we have two limits on c and c', there are isomorphic pair h, h' open Limit open NTrans 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' ( limit lim' a0 t0 o limit lim a0' t0' )( λ {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' (id a0') idR ⟩ id a0' ∎ open import CatExponetial open Functor -------------------------------- -- -- Constancy 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₁ ∎ --------- -- -- Limit Constancy Functor F : A → A^I has right adjoint -- -- we are going to prove 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} ) limit2couniv : ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K A I (a0 b) ) b ) → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) ) limit2couniv lim a0 t0 = record { -- F U ε _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 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 {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ] couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i ≈⟨⟩ TMap (t0 b) i o (limit (lim b) a f) ≈⟨ t0f=t (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 {a0 b} {t0 b} ))} → ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] ) → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ] couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin limit (lim b {a0 b} {t0 b} ) a f ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) g lim-g=f ⟩ g ∎ open import Category.Cat open coUniversalMapping univ2limit : ( U : Obj (A ^ I ) → Obj A ) ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b ) ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) → ( Γ : Functor I A ) → Limit A I Γ (U Γ) (ε Γ) univ2limit U ε univ Γ = 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 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ) limit1 a t = _*' univ {_} {a} t t0f=t1 : {a : Obj A} {t : NTrans I A (K A I 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 _*' univ {Γ} {a} t ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩ TMap t i ∎ limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K A I 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 _*' univ t ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩ f ∎ 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 ∎ ----- -- -- 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 ∎ open IProduct open Equalizer -- -- limit from equalizer and product -- -- -- ai -- ^ K f = id lim -- | pi lim = K i -----------→ K j = lim -- | | | -- p | | -- ^ proj i o e = ε i | | ε j = proj j o e -- | | | -- | e = equalizer (id p) (id p) | | -- | v v -- lim <------------------ d' a i = Γ i -----------→ Γ j = a j -- k ( product pi ) Γ f -- Γ f o ε i = ε j -- limit-ε : ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → IsEqualizer A e f g ) ( lim p : Obj A ) ( e : Hom A lim p ) ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → NTrans I A (K A I lim) Γ limit-ε eqa lim p e proj = record { TMap = tmap ; isNTrans = record { commute = commute1 } } where tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i) tmap i = A [ proj i o e ] commute1 : {i j : Obj I} {f : Hom I i j} → A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ] commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin FMap Γ f o tmap i ≈⟨⟩ FMap Γ f o ( proj i o e ) ≈⟨ assoc ⟩ ( FMap Γ f o proj i ) o e ≈⟨ fe=ge ( eqa e (FMap Γ f o proj i) ( proj j )) ⟩ proj j o e ≈↑⟨ idR ⟩ (proj j o e ) o id1 A lim ≈⟨⟩ tmap j o FMap (K A I lim) f ∎ limit-from : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) → IProduct {c₁'} A (Obj I) p ai pi ) ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → IsEqualizer A e f g ) ( lim p : Obj A ) -- limit to be made ( e : Hom A lim p ) -- existing of equalizer ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) → Limit A I Γ lim ( limit-ε eqa lim p e proj ) limit-from prod eqa lim p e proj = 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 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) i o limit1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin TMap (limit-ε eqa lim p e proj ) i o limit1 a t ≈⟨⟩ ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ≈↑⟨ assoc ⟩ proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ) ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩ proj i o product (prod p (FObj Γ) proj) (TMap t) ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ TMap t i ∎ limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} → ({i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) 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 ≈⟨⟩ k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ≈⟨ IsEqualizer.uniqueness (eqa e (id1 A p) (id1 A p )) ( begin e o f ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩ product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e o f ) ) ) ≈⟨ ip-cong (prod p (FObj Γ) proj) ( λ i → begin proj i o ( e o f ) ≈⟨ assoc ⟩ ( proj i o e ) o f ≈⟨ lim=t {i} ⟩ TMap t i ∎ ) ⟩ product (prod p (FObj Γ) proj) (TMap t) ∎ ) ⟩ f ∎ ---- -- -- Adjoint functor preserves limits -- -- open import Category.Cat ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( U : Functor B A) → NTrans I A ( K A I (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 B I lim) f ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f ∎ } } adjoint-preseve-limit : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limitb : Limit B I Γ lim tb ) → { U : Functor B A } { F : Functor A B } { η : NTrans A A identityFunctor ( U ○ F ) } { ε : NTrans B B ( F ○ U ) identityFunctor } → ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb U ) adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = 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 ta = ta1 B Γ lim tb U 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) tfmap a t i = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] tF : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → NTrans I B (K B I (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 A I a) f ]) ≈⟨⟩ TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K A I 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 A I a) b)) ≈⟨⟩ tfmap a t b o FMap (K B I (FObj F a)) f ∎ } } limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim) limit1 a t = A [ FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a ] t0f=t1 : {a : Obj A} {t : NTrans I A (K A I 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 limitb (FObj F a) (tF a t )) o TMap η a ) ≈⟨ assoc ⟩ ( FMap U ( TMap tb i ) o FMap U (limit limitb (FObj F a) (tF a t ))) o TMap η a ≈↑⟨ car ( distr U ) ⟩ FMap U ( B [ TMap tb i o limit limitb (FObj F a) (tF a t ) ] ) o TMap η a ≈⟨ car ( fcong U ( t0f=t 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 A I 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 limitb (FObj F a) (tF a t )) o TMap η a ≈⟨ car ( fcong U (limit-uniqueness limitb (B [ TMap ε lim o FMap F f ] ) ( λ {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 ] lemma1 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 ∎