Mercurial > hg > Members > kono > Proof > category
changeset 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 | 56cf6581c5f6 |
| children | 016087cfa75a |
| files | cat-utility.agda freyd.agda freyd1.agda limit-to.agda pullback.agda |
| diffstat | 5 files changed, 121 insertions(+), 171 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sun Mar 12 14:48:14 2017 +0900 +++ b/cat-utility.agda Sun Mar 12 19:46:07 2017 +0900 @@ -302,26 +302,60 @@ } - record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) - : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where + record IsLimit { 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 - 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 ] + record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) + : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where + field + a0 : Obj A + t0 : NTrans I A ( K A I a0 ) Γ + isLimit : IsLimit A I Γ a0 t0 + + LimitNat : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} + ( C : 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 ○ Γ) + LimitNat B I C Γ 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 Limit + record LimitPreserve { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) + { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' ) + (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where + field + preserve : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → + IsLimit C I (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat A I C Γ (a0 limita ) (t0 limita) G ) + plimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ ) + plimit Γ limita = record { a0 = (FObj G (a0 limita )) + ; t0 = LimitNat A I C Γ (a0 limita ) (t0 limita) G + ; isLimit = preserve Γ limita } + record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - isLimit : ( Γ : Functor I A ) -> Limit A I Γ + climit : ( Γ : 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 - isLimit : ( Γ : Functor I A ) -> Limit A I Γ + climit : ( Γ : Functor I A ) -> Limit A I Γ + alimit : ( Γ : Functor I A ) (a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) -> IsLimit A I Γ a0 t0 product : (a b : Obj A) -> Obj A π1 : (a b : Obj A) -> Hom A (product a b ) a @@ -333,6 +367,6 @@ 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-c Γ = a0 ( climit Γ) limit-u : ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ )) Γ - limit-u Γ = t0 ( isLimit Γ) + limit-u Γ = t0 ( climit Γ)
--- a/freyd.agda Sun Mar 12 14:48:14 2017 +0900 +++ b/freyd.agda Sun Mar 12 19:46:07 2017 +0900 @@ -40,6 +40,7 @@ open NTrans open Limit +open IsLimit open SmallFullSubcategory open PreInitial open Complete @@ -61,7 +62,7 @@ a00 : Obj A a00 = limit-c comp F lim : ( Γ : Functor A A ) → Limit A A Γ - lim Γ = isLimit comp Γ + lim Γ = climit comp Γ 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 @@ -81,9 +82,9 @@ e=id {e} uce=uc = let open ≈-Reasoning (A) in begin e - ≈↑⟨ limit-uniqueness (lim F) e ( λ {i} → uce=uc ) ⟩ - limit (lim F) a00 u - ≈⟨ limit-uniqueness (lim F) (id1 A a00) ( λ {i} → idR ) ⟩ + ≈↑⟨ limit-uniqueness (isLimit (lim F)) e ( λ {i} → uce=uc ) ⟩ + limit (isLimit (lim F)) a00 u + ≈⟨ limit-uniqueness (isLimit (lim F)) (id1 A a00) ( λ {i} → idR ) ⟩ id1 A a00 ∎ kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o
--- a/freyd1.agda Sun Mar 12 14:48:14 2017 +0900 +++ b/freyd1.agda Sun Mar 12 19:46:07 2017 +0900 @@ -21,6 +21,7 @@ open CommaObj open CommaHom open Limit +open IsLimit -- F : A → C -- G : A → C @@ -42,138 +43,42 @@ id1 A (obj (FObj Γ x)) ∎ -NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) - (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) → NTrans I A ( K A I (obj c) ) (FIA Γ) -NIA {I} Γ c ta = record { - TMap = λ x → arrow (TMap ta x ) - ; isNTrans = record { commute = comm1 } - } where - comm1 : {a b : Obj I} {f : Hom I a b} → - 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 - ∎ - } } - FICG : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C FICG {I} Γ = G ○ (FIA Γ) FICF : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I C FICF {I} Γ = F ○ (FIA Γ) -FINAT : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → NTrans I C (FICF Γ) (FICG Γ) -FINAT {I} Γ = record { - TMap = λ i → tmap i - ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } - } where - tmap : (i : Obj I ) → Hom C (FObj (FICF Γ) i) (FObj (FICG Γ) i) - tmap i = hom (FObj Γ i ) - commute : {a b : Obj I} → {f : Hom I a b} → C [ C [ FMap (FICG Γ) f o tmap a ] ≈ C [ tmap b o FMap (FICF Γ) f ] ] - commute {a} {b} {f} = comm ( FMap Γ f ) - -revΓ : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I CommaCategory -revΓ {I} Γ = record { - FObj = λ x → record { - obj = obj ( FObj Γ x ) - ; hom = TMap (FINAT Γ) x - } - ; FMap = λ {a} {b} f → record { - arrow = arrow ( FMap Γ f ) - ; comm = IsNTrans.commute ( isNTrans (FINAT Γ) ) - } - ; isFunctor = record { - identity = IsFunctor.identity ( isFunctor Γ ) - ; distr = IsFunctor.distr ( isFunctor Γ ) - ; ≈-cong = IsFunctor.≈-cong ( isFunctor Γ ) - }} where - -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 = tb A I (FIA Γ) (obj c) ta G +open LimitPreserve LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) - → ( glimit : ( Γ : Functor I A ) - → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) ) → ( Γ : Functor I CommaCategory ) + → ( glimit : LimitPreserve A I C G ) → Limit C I (FICG Γ) -LimitC {I} comp glimit Γ = glimit (FIA Γ) (isLimit comp (FIA Γ)) - -revLimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) - → ( glimit : ( Γ : Functor I A ) - → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) ) - → ( Γ : Functor I CommaCategory ) - → Limit C I ( G ○ (FIA (revΓ Γ) )) -revLimitC {I} comp glimit Γ = glimit (FIA (revΓ Γ)) (isLimit comp (FIA (revΓ Γ ))) - - -a0F : ( I : Category c₁ c₂ ℓ ) → (a1 : Obj A) → Functor I A -a0F I a1 = record { - FObj = λ x → a1 - ; FMap = λ {a} {b} f → id1 A a1 - ; isFunctor = record { - identity = let open ≈-Reasoning (A) in refl-hom - ; distr = let open ≈-Reasoning (A) in ( sym idL ) - ; ≈-cong = λ _ → let open ≈-Reasoning (A) in refl-hom - }} where - -t0F : ( I : Category c₁ c₂ ℓ ) → (a1 : Obj A ) - → NTrans I A (K A I a1 ) (a0F I a1 ) -t0F I a1 = record { - TMap = λ i → id1 A a1 - ; isNTrans = record { commute = λ {a b f} → commute {a} {b} {f} } - } where - commute : {a b : Obj I} {f : Hom I a b} → A [ - A [ FMap (a0F I a1 ) f o id1 A a1 ] ≈ - A [ id1 A a1 o FMap (K A I a1) f ] ] - commute {a} {b} {f} = let open ≈-Reasoning (A) in begin - FMap (a0F I a1 ) f o id1 A a1 - ≈⟨ idR ⟩ - FMap (a0F I a1 ) f - ≈⟨⟩ - id1 A a1 - ≈⟨⟩ - FMap (K A I a1) f - ≈↑⟨ idL ⟩ - id1 A a1 o FMap (K A I a1) f - ∎ - -hoge : ( a : Obj A ) → ( I : Category c₁ c₂ ℓ ) → (comp : Complete A I ) → ∀ { i : Obj I } → - A [ A [ TMap ( limit-u comp (a0F I a)) i o limit (isLimit comp (a0F I a)) a (t0F I a) ] ≈ id1 A a ] -hoge a I comp {i} = t0f=t (isLimit comp (a0F I a)) - +LimitC {I} comp Γ glimit = plimit glimit (FIA Γ) (climit comp (FIA Γ)) commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) ) - → Obj CommaCategory + → ( glimit : LimitPreserve A I C G ) + → Obj CommaCategory commaLimit {I} comp Γ glimit = record { obj = limit-c comp (FIA Γ) ; hom = limitHom } where frev : {i : Obj I } → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i)) - frev {i} = TMap (t0 ( isLimit comp (FIA Γ))) i + frev {i} = TMap (t0 ( climit comp (FIA Γ))) i + commute : {a b : Obj I} {f : Hom I a b} → + C [ C [ FMap (FICG Γ) f o C [ hom (FObj Γ a) o FMap F frev ] ] + ≈ C [ C [ hom (FObj Γ b) o FMap F frev ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] + commute {a} {b} {f} = ? tu : NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ) tu = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F frev ] - ; isNTrans = {!!} + ; isNTrans = record { commute = λ {a} {b} {f}→ commute {a} {b} {f} } } - forward : Hom C (FObj G (limit-c comp (FIA Γ))) (a0 (LimitC comp glimit Γ)) - forward = limit (LimitC comp glimit Γ) (FObj G (limit-c comp (FIA Γ))) - ( record { TMap = λ i → C [ FMap G frev o {!!} ] ; isNTrans = {!!} } ) - rev : Hom C (a0 (LimitC comp glimit Γ)) (FObj G (limit-c comp (FIA Γ))) - rev = C [ FMap G {!!} o TMap (t0 (LimitC comp glimit Γ)) {!!} ] + uHomF : Hom C ( FObj F ( limit-c comp (FIA Γ) ) ) (FObj G ( (a0 (climit comp (FIA Γ) )))) + uHomF = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) tu limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) - limitHom = C [ rev o limit (LimitC comp glimit Γ) (FObj F (limit-c comp (FIA Γ))) tu ] + limitHom = uHomF commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) @@ -192,7 +97,9 @@ hasLimit {I} comp glimit Γ = record { a0 = {!!} ; t0 = {!!} ; - limit = λ a t → {!!} ; - t0f=t = λ {a t i } → {!!} ; - limit-uniqueness = λ {a} {t} f t=f → {!!} + isLimit = record { + limit = λ a t → {!!} ; + t0f=t = λ {a t i } → {!!} ; + limit-uniqueness = λ {a} {t} f t=f → {!!} + } }
--- a/limit-to.agda Sun Mar 12 14:48:14 2017 +0900 +++ b/limit-to.agda Sun Mar 12 19:46:07 2017 +0900 @@ -34,6 +34,7 @@ open Complete open Limit +open IsLimit open NTrans -- Functor Γ : TwoCat -> A @@ -176,17 +177,17 @@ c : Obj A c = limit-c comp Γ lim : Limit A I Γ - lim = isLimit comp Γ + lim = climit 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 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - k {d} h fh=gh = limit lim d (inat d h fh=gh ) + k {d} h fh=gh = limit (isLimit lim) d (inat d h fh=gh ) ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] ek=h d h fh=gh = let open ≈-Reasoning A in begin e o k h fh=gh ≈⟨⟩ TMap (limit-u comp Γ) discrete.t0 o k h fh=gh - ≈⟨ t0f=t lim {d} {inat d h fh=gh } {discrete.t0} ⟩ + ≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {discrete.t0} ⟩ TMap (inat d h fh=gh) discrete.t0 ≈⟨⟩ h @@ -225,7 +226,7 @@ → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin k h fh=gh - ≈⟨ limit-uniqueness lim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ + ≈⟨ limit-uniqueness (isLimit lim) k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ k' ∎ @@ -278,26 +279,26 @@ } where D = DiscreteCat S I = Obj ( DiscreteCat S ) - lim = isLimit comp Γ + lim = climit comp Γ ai = λ i → FObj Γ i p = limit-c comp Γ pi = λ i → TMap (limit-u comp Γ) i iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p - iproduct {q} qi = limit lim q (pnat A S Γ qi ) + iproduct {q} qi = limit (isLimit lim) q (pnat A S Γ qi ) pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] - pif=q {q} qi {i} = t0f=t lim {q} {pnat A S Γ qi } {i} + pif=q {q} qi {i} = t0f=t (isLimit lim) {q} {pnat A S Γ qi } {i} ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ] ipu {i} q h = let open ≈-Reasoning A in refl-hom ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] - ip-uniqueness {q} {h} = limit-uniqueness lim {q} {pnat A S Γ (λ i → A [ pi i o h ] )} h (ipu q h) + ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} h (ipu q h) ipc : {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 [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ] ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) i o iproduct qi' ≈⟨⟩ - TMap (limit-u comp Γ) i o limit lim q (pnat A S Γ qi' ) - ≈⟨ t0f=t lim {q} {pnat A S Γ qi'} {i} ⟩ + TMap (limit-u comp Γ) i o limit (isLimit lim) q (pnat A S Γ qi' ) + ≈⟨ t0f=t (isLimit lim) {q} {pnat A S Γ qi'} {i} ⟩ TMap (pnat A S Γ qi') i ≈⟨⟩ qi' i @@ -308,4 +309,4 @@ ∎ 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 [ iproduct qi ≈ iproduct qi' ] - ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness lim {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i)) + ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))
--- 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