Mercurial > hg > Members > kono > Proof > category
changeset 484:fcae3025d900
fix Limit pu a0 and t0 in record definition
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Mar 2017 16:38:08 +0900 |
| parents | 265f13adf93b |
| children | da4486523f73 |
| files | cat-utility.agda freyd.agda freyd1.agda limit-to.agda pullback.agda |
| diffstat | 5 files changed, 113 insertions(+), 134 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sat Mar 11 10:51:12 2017 +0900 +++ b/cat-utility.agda Sat Mar 11 16:38:08 2017 +0900 @@ -303,31 +303,25 @@ 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 + : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field + a0 : Obj A + t0 : NTrans I A ( K A I a0 ) Γ 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 ] - A0 : Obj A - A0 = a0 - T0 : NTrans I A ( K A I a0 ) Γ - T0 = t0 record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - limit-c : ( Γ : Functor I A ) -> Obj A - limit-u : ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ )) Γ - isLimit : ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ) + isLimit : ( Γ : Functor I A ) -> Limit A I Γ record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - limit-c : ( Γ : Functor I A ) -> Obj A - limit-u : ( Γ : Functor I A ) → NTrans I A ( K A I (limit-c Γ )) Γ - isLimit : ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ) + isLimit : ( Γ : Functor I A ) -> Limit A I Γ product : (a b : Obj A) -> Obj A π1 : (a b : Obj A) -> Hom A (product a b ) a @@ -337,3 +331,8 @@ equalizer-p : {a b : Obj A} (f g : Hom A a b) -> Obj A equalizer-e : {a b : Obj A} (f g : Hom A a b) -> Hom A (equalizer-p f g) a isEqualizer : {a b : Obj A} (f g : Hom A a b) -> IsEqualizer A (equalizer-e f g) f g + open Limit + limit-c : ( Γ : Functor I A ) -> Obj A + limit-c Γ = a0 ( isLimit Γ) + limit-u : ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ )) Γ + limit-u Γ = t0 ( isLimit Γ)
--- a/freyd.agda Sat Mar 11 10:51:12 2017 +0900 +++ b/freyd.agda Sat Mar 11 16:38:08 2017 +0900 @@ -49,7 +49,7 @@ initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A A) (SFS : SmallFullSubcategory A ) → - (PI : PreInitial A (SFSF SFS )) → { a0 : Obj A } → HasInitialObject A (limit-c comp (SFSF SFS)) + (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS)) initialFromPreInitialFullSubcategory A comp SFS PI = record { initial = initialArrow ; uniqueness = λ a f → lemma1 a f @@ -58,35 +58,35 @@ F = SFSF SFS FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b FMap← = SFSFMap← SFS - a0 : Obj A - a0 = limit-c comp F - lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ) + a00 : Obj A + a00 = limit-c comp F + lim : ( Γ : Functor A A ) → Limit A A Γ lim Γ = isLimit comp Γ - u : NTrans A A (K A A a0) F - u = T0 ( lim F ) + u : NTrans A A (K A A a00) F + u = t0 ( lim F ) equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g equ f g = Complete.isEqualizer comp f g ep : {a b : Obj A} → {f g : Hom A a b} → Obj A ep {a} {b} {f} {g} = equalizer-p comp f g ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a ee {a} {b} {f} {g} = equalizer-e comp f g - f : {a : Obj A} → Hom A a0 (FObj F (preinitialObj PI {a} ) ) + f : {a : Obj A} → Hom A a00 (FObj F (preinitialObj PI {a} ) ) f {a} = TMap u (preinitialObj PI {a} ) - initialArrow : ∀( a : Obj A ) → Hom A a0 a + initialArrow : ∀( a : Obj A ) → Hom A a00 a initialArrow a = A [ preinitialArrow PI {a} o f ] - equ-fi : { a : Obj A} → {f' : Hom A a0 a} → + equ-fi : { a : Obj A} → {f' : Hom A a00 a} → IsEqualizer A ee ( A [ preinitialArrow PI {a} o f ] ) f' equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f' - e=id : {e : Hom A a0 a0} → ( {c : Obj A} → A [ A [ TMap u c o e ] ≈ TMap u c ] ) → A [ e ≈ id1 A a0 ] + e=id : {e : Hom A a00 a00} → ( {c : Obj A} → A [ A [ TMap u c o e ] ≈ TMap u c ] ) → A [ e ≈ id1 A a00 ] e=id {e} uce=uc = let open ≈-Reasoning (A) in begin e ≈↑⟨ limit-uniqueness (lim F) e ( λ {i} → uce=uc ) ⟩ - limit (lim F) a0 u - ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( λ {i} → idR ) ⟩ - id1 A a0 + limit (lim F) a00 u + ≈⟨ limit-uniqueness (lim F) (id1 A a00) ( λ {i} → idR ) ⟩ + id1 A a00 ∎ - kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a0} → A [ A [ TMap u c o + kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ] ≈ TMap u c ] kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in @@ -99,13 +99,13 @@ ≈↑⟨ car ( full→ SFS ) ⟩ FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI) ≈⟨ nat u ⟩ - TMap u c o FMap (K A A a0) (FMap← (TMap u c o p o preinitialArrow PI)) + TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI)) ≈⟨⟩ - TMap u c o id1 A a0 + TMap u c o id1 A a00 ≈⟨ idR ⟩ TMap u c ∎ - kfuc=1 : {k1 : Obj A} → {p : Hom A k1 a0} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a0 ] + kfuc=1 : {k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ] kfuc=1 {k1} {p} = e=id ( kfuc=uc ) -- if equalizer has right inverse, f = g lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) @@ -129,14 +129,14 @@ ≈⟨ idR ⟩ g ∎ - lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ] + lemma1 : (a : Obj A) (f' : Hom A a00 a) → A [ f' ≈ initialArrow a ] lemma1 a f' = let open ≈-Reasoning (A) in sym ( begin initialArrow a ≈⟨⟩ preinitialArrow PI {a} o f - ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a0} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi ) + ≈⟨ lemma2 a00 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a00} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi ) (kfuc=1 {ep} {ee} ) ⟩ f' ∎ )
--- a/freyd1.agda Sat Mar 11 10:51:12 2017 +0900 +++ b/freyd1.agda Sat Mar 11 16:38:08 2017 +0900 @@ -17,20 +17,6 @@ open NTrans -tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B ) - ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → - ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ) -tb B I Γ lim tb U = record { - TMap = TMap (Functor*Nat I C U tb) ; - isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin - FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a - ≈⟨ nat ( Functor*Nat I C U tb ) ⟩ - TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f - ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ - TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f - ∎ - } } - open Complete open CommaObj open CommaHom @@ -66,55 +52,42 @@ A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ] comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) +tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B ) + ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → + ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ) +tb B I Γ lim tb U = record { + TMap = TMap (Functor*Nat I C U tb) ; + isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin + FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a + ≈⟨ nat ( Functor*Nat I C U tb ) ⟩ + TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f + ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ + TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f + ∎ + } } + +FIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C +FIC {I} Γ = G ○ (FIA Γ) + NIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I C ( K C I (FObj G (obj c)) ) (G ○ ( FIA Γ) ) -NIC {I} Γ c ta = record { - TMap = λ x → FMap G (TMap ta x ) - ; isNTrans = record { commute = comm1 } - } where - comm1 : {a b : Obj I} {f : Hom I a b} → - C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ] - comm1 {a} {b} {f} = let open ≈-Reasoning (C) in begin - FMap (G ○ FIA Γ) f o FMap G (TMap ta a) - ≈↑⟨ distr G ⟩ - FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] ) - ≈⟨ fcong G ( nat ta ) ⟩ - FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] ) - ≈⟨ distr G ⟩ - FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f ) - ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩ - FMap G (TMap ta b) o id1 C (FObj G (obj c)) - ≈⟨⟩ - FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f - ∎ +NIC {I} Γ c ta = tb A I (FIA Γ) (obj c) ta G - -NIComma : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) - (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I CommaCategory ( K CommaCategory I c ) Γ -NIComma {I} Γ c ta = record { - TMap = λ x → record { - arrow = TMap ta x - ; comm = comm1 x - } - ; isNTrans = record { commute = {!!} } - } where - comm1 : ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ] - comm1 x = let open ≈-Reasoning (C) in begin - FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) - ≈⟨ {!!} ⟩ - hom (FObj Γ x) o FMap F (TMap ta x) - ∎ - - +LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) + → ( Glimit : ( Γ : Functor I A ) (lim : Obj A ) + → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G ) ) + → ( lim : Obj CommaCategory ) → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I ? ) Γ ) + → Limit C I (FIC Γ) {!!} ( NIC Γ {!!} (NIA Γ {!!} ta) ) +LimitC {I} comp Glimit lim Γ ta = Glimit (FIA Γ) {!!} (NIA Γ {!!} ta ) (isLimit comp (FIA Γ)) commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) → Obj CommaCategory commaLimit {I} comp Γ = record { obj = limit-c comp (FIA Γ) ; hom = limitHom } where - ll = ( limit (isLimit comp (FIA Γ)) (limit-c comp (FIA Γ)) {!!}) + ll = ( limit (isLimit comp (FIA Γ)) (limit-c comp (FIA Γ)) (NIA Γ {!!} {!!} )) limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) - limitHom = C [ FMap G ll o C [ {!!} o FMap F ll ] ] + limitHom = {!!} commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) @@ -127,7 +100,7 @@ } where tmap : (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i) tmap i = record { - arrow = A [ arrow ( TMap ta i) o A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ] + arrow = A [ arrow ( TMap ta i) o A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ] ; comm = {!!} } commute : {a b : Obj I} {f : Hom I a b} →
--- a/limit-to.agda Sat Mar 11 10:51:12 2017 +0900 +++ b/limit-to.agda Sat Mar 11 16:38:08 2017 +0900 @@ -154,7 +154,7 @@ equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A TwoCat ) -> Hom A ( limit-c comp (IndexFunctor A a b f g)) a -equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) t0 +equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) discrete.t0 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A TwoCat ) @@ -175,7 +175,7 @@ e = equlimit A f g comp c : Obj A c = limit-c comp Γ - lim : Limit A I Γ c ( limit-u comp Γ ) + lim : Limit A I Γ lim = isLimit comp Γ inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ inat = IndexNat A f g @@ -185,9 +185,9 @@ ek=h d h fh=gh = let open ≈-Reasoning A in begin e o k h fh=gh ≈⟨⟩ - TMap (limit-u comp Γ) t0 o k h fh=gh - ≈⟨ t0f=t lim {d} {inat d h fh=gh } {t0} ⟩ - TMap (inat d h fh=gh) t0 + TMap (limit-u comp Γ) discrete.t0 o k h fh=gh + ≈⟨ t0f=t lim {d} {inat d h fh=gh } {discrete.t0} ⟩ + TMap (inat d h fh=gh) discrete.t0 ≈⟨⟩ h ∎ @@ -195,13 +195,13 @@ ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ] uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin - TMap (limit-u comp Γ) t0 o k' + TMap (limit-u comp Γ) discrete.t0 o k' ≈⟨⟩ e o k' ≈⟨ ek'=h ⟩ h ≈⟨⟩ - TMap (inat d h fh=gh) t0 + TMap (inat d h fh=gh) discrete.t0 ∎ uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) t1 o k' @@ -210,7 +210,7 @@ ≈⟨⟩ ( TMap (limit-u comp Γ) t1 o FMap (K A I c) arrow-f ) o k' ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩ - ( FMap Γ arrow-f o TMap (limit-u comp Γ) t0 ) o k' + ( FMap Γ arrow-f o TMap (limit-u comp Γ) discrete.t0 ) o k' ≈⟨⟩ (f o e ) o k' ≈↑⟨ assoc ⟩
--- a/pullback.agda Sat Mar 11 10:51:12 2017 +0900 +++ b/pullback.agda Sat Mar 11 16:38:08 2017 +0900 @@ -137,39 +137,39 @@ 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 + ( lim : Limit A I Γ ) → ( lim' : Limit A I Γ ) + → Hom A (a0 lim )(a0 lim') +iso-l I Γ lim lim' = limit lim' (a0 lim) ( t0 lim) 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' + ( lim : Limit A I Γ ) → ( lim' : Limit A I Γ ) + → Hom A (a0 lim') (a0 lim) +iso-r I Γ lim lim' = limit lim (a0 lim') (t0 lim') 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' ) + ( lim : Limit A I Γ ) → ( lim' : Limit A I Γ ) → + ∀{ i : Obj I } → A [ A [ iso-l I Γ lim lim' o iso-r I Γ lim lim' ] ≈ id1 A (a0 lim') ] +iso-lr I Γ lim lim' {i} = let open ≈-Reasoning (A) in begin + iso-l I Γ lim lim' o iso-r I Γ lim lim' + ≈⟨⟩ + limit lim' (a0 lim) ( t0 lim) o limit lim (a0 lim') (t0 lim') + ≈↑⟨ limit-uniqueness lim' ( limit lim' (a0 lim) (t0 lim) o limit lim (a0 lim') (t0 lim') )( λ {i} → ( begin + TMap (t0 lim') i o ( limit lim' (a0 lim) (t0 lim) o limit lim (a0 lim') (t0 lim') ) ≈⟨ assoc ⟩ - ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0' + ( TMap (t0 lim') i o limit lim' (a0 lim) (t0 lim) ) o limit lim (a0 lim') (t0 lim') ≈⟨ car ( t0f=t lim' ) ⟩ - TMap t0 i o limit lim a0' t0' + TMap (t0 lim) i o limit lim (a0 lim') (t0 lim') ≈⟨ t0f=t lim ⟩ - TMap t0' i + TMap (t0 lim') i ∎) ) ⟩ - limit lim' a0' t0' - ≈⟨ limit-uniqueness lim' (id a0') idR ⟩ - id a0' + limit lim' (a0 lim') (t0 lim') + ≈⟨ limit-uniqueness lim' (id (a0 lim')) idR ⟩ + id (a0 lim' ) ∎ + open import CatExponetial open Functor @@ -221,31 +221,31 @@ -- a0 : Obj A and t0 : NTrans K Γ come from the limit limit2couniv : - ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) - → ( a0 : ( Γ : Functor I A ) → Obj A ) ( t0 : ( Γ : Functor I A ) → NTrans I A ( K A I (a0 Γ) ) Γ ) - → 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 ; -- η + ( lim : ( Γ : Functor I A ) → Limit A I Γ ) + → ( aΓ : ( Γ : Functor I A ) → Obj A ) ( tΓ : ( Γ : Functor I A ) → NTrans I A ( K A I (aΓ Γ) ) Γ ) + → coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ( lim b) ) ( λ b → t0 (lim b) ) +limit2couniv lim aΓ tΓ = record { -- F U ε + _*' = λ {b} {a} k → limit (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 {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ] + A ^ I [ A ^ I [ t0 (lim b) o FMap (KI I) (limit (lim 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 (lim b )) i o TMap ( FMap (KI I) (limit (lim b ) a f) ) i ≈⟨⟩ - TMap (t0 b) i o (limit (lim b) a f) + TMap (t0 (lim 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 : 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 (lim 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 ⟩ + limit (lim b ) a f + ≈⟨ limit-uniqueness ( lim b ) g lim-g=f ⟩ g ∎ @@ -258,8 +258,10 @@ ( 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 Γ) (ε Γ) + ( Γ : Functor I A ) → Limit A I Γ univ2limit U ε univ Γ = record { + a0 = U Γ ; + t0 = ε Γ ; 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 @@ -350,8 +352,10 @@ ( 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 A I Γ limit-from prod eqa lim p e proj = record { + a0 = lim ; + t0 = limit-ε eqa lim p e proj ; 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 @@ -417,18 +421,21 @@ } } 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 ) → + { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit B I Γ ) → { 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 { + ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) +adjoint-preseve-limit B Γ limitb {U} {F} {η} {ε} adj = record { + a0 = FObj U lim ; + t0 = ta1 B Γ lim tb U ; 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 + ta = ta1 B Γ (a0 limitb) (t0 limitb) U + tb = t0 limitb + lim = a0 limitb 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)) Γ @@ -458,7 +465,7 @@ 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 : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) ) 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 ]