Mercurial > hg > Members > kono > Proof > category
diff pullback.agda @ 487:c257347a27f3
found limit in freyd
isLimit introduced
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Mar 2017 19:46:07 +0900 |
| parents | fcae3025d900 |
| children | 633df882db86 |
line wrap: on
line diff
--- a/pullback.agda Sun Mar 12 14:48:14 2017 +0900 +++ b/pullback.agda Sun Mar 12 19:46:07 2017 +0900 @@ -134,17 +134,18 @@ -- If we have two limits on c and c', there are isomorphic pair h, h' open Limit +open IsLimit open NTrans iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) ( 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-l I Γ lim lim' = limit (isLimit lim') (a0 lim) ( t0 lim) iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) ( 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-r I Γ lim lim' = limit (isLimit lim) (a0 lim') (t0 lim') iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) @@ -153,18 +154,18 @@ 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') ) + limit (isLimit lim') (a0 lim) ( t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') + ≈↑⟨ limit-uniqueness (isLimit lim') ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim )(a0 lim') (t0 lim') )( λ {i} → ( begin + TMap (t0 lim') i o ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') ) ≈⟨ assoc ⟩ - ( TMap (t0 lim') i o limit lim' (a0 lim) (t0 lim) ) o limit lim (a0 lim') (t0 lim') - ≈⟨ car ( t0f=t lim' ) ⟩ - TMap (t0 lim) i o limit lim (a0 lim') (t0 lim') - ≈⟨ t0f=t lim ⟩ + ( TMap (t0 lim') i o limit (isLimit lim') (a0 lim) (t0 lim) ) o limit (isLimit lim) (a0 lim') (t0 lim') + ≈⟨ car ( t0f=t (isLimit lim') ) ⟩ + TMap (t0 lim) i o limit (isLimit lim) (a0 lim') (t0 lim') + ≈⟨ t0f=t (isLimit lim) ⟩ TMap (t0 lim') i ∎) ) ⟩ - limit lim' (a0 lim') (t0 lim') - ≈⟨ limit-uniqueness lim' (id (a0 lim')) idR ⟩ + limit (isLimit lim') (a0 lim') (t0 lim') + ≈⟨ limit-uniqueness (isLimit lim') (id (a0 lim')) idR ⟩ id (a0 lim' ) ∎ @@ -225,27 +226,27 @@ → ( 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 ; -- η + _*' = λ {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 (lim b) a f) ] ≈ f ] + 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 (lim b ) a f) ) i + TMap (t0 (lim b )) i o TMap ( FMap (KI I) (limit (isLimit (lim b )) a f) ) i ≈⟨⟩ - TMap (t0 (lim b)) i o (limit (lim b) a f) - ≈⟨ t0f=t (lim b) ⟩ + 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 (lim b ) a f ≈ g ] + → A [ limit (isLimit (lim b )) a f ≈ g ] couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin - limit (lim b ) a f - ≈⟨ limit-uniqueness ( lim b ) g lim-g=f ⟩ + limit (isLimit (lim b )) a f + ≈⟨ limit-uniqueness (isLimit ( lim b )) g lim-g=f ⟩ g ∎ @@ -262,9 +263,11 @@ 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 + 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 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ) limit1 a t = _*' univ {_} {a} t @@ -356,9 +359,11 @@ 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 + 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 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 )) (iproduct ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom @@ -429,9 +434,11 @@ 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 + 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 ta = ta1 B Γ (a0 limitb) (t0 limitb) U tb = t0 limitb @@ -466,18 +473,18 @@ ∎ } } 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 ] + 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 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 ) + 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 limitb (FObj F a) (tF a t ))) o TMap η a + ( 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 limitb (FObj F a) (tF a t ) ] ) o TMap η a - ≈⟨ car ( fcong U ( t0f=t limitb ) ) ⟩ + 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 @@ -501,8 +508,8 @@ 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 (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a + ≈⟨ car ( fcong U (limit-uniqueness (isLimit 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