Mercurial > hg > Members > kono > Proof > category
changeset 691:917e51be9bbf
change argument of Limit and K
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Nov 2017 09:56:40 +0900 |
| parents | 3d41a8edbf63 |
| children | 3ca3b5a4ab45 |
| files | SetsCompleteness.agda cat-utility.agda freyd.agda freyd1.agda freyd2.agda limit-to.agda pullback.agda |
| diffstat | 7 files changed, 165 insertions(+), 166 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/SetsCompleteness.agda Sun Nov 12 09:56:40 2017 +0900 @@ -52,7 +52,7 @@ open iproduct SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) - → IProduct ( Sets { c₂} ) I ai + → IProduct I ( Sets { c₂} ) ai SetsIProduct I fi = record { iprod = iproduct I fi ; pi = λ i prod → pi1 prod i @@ -193,14 +193,14 @@ open NTrans Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ + → NTrans C Sets (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ Cone C I s Γ = record { TMap = λ i → λ sn → snmap sn i ; isNTrans = record { commute = comm1 } } where comm1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ - Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] + Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin FMap Γ f (snmap sn a ) ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩ @@ -214,9 +214,9 @@ open ≡-Reasoning -SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → Limit Sets C Γ -SetsLimit {c₁} C I s Γ = record { +SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) + → Limit C Sets Γ +SetsLimit {c₁} I C s Γ = record { a0 = snat (ΓObj s Γ) (ΓMap s Γ) ; t0 = Cone C I s Γ ; isLimit = record { @@ -225,13 +225,13 @@ ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} } } where - comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) + comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x comm2 {a} {x} t f = ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) ) - limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) + limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } - t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ] + t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ] t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x ≡⟨⟩ @@ -239,7 +239,7 @@ ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning - limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → + limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin limit1 a t x @@ -277,7 +277,7 @@ SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C SetsCompleteness {c₁} {c₂} C I s = record { - climit = λ Γ → SetsLimit {c₁} C I s Γ + climit = λ Γ → SetsLimit {c₁} I C s Γ ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ; equalizer = ( λ e → equ e ) ; isEqualizer = SetsIsEqualizer a b f g }
--- a/cat-utility.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/cat-utility.agda Sun Nov 12 09:56:40 2017 +0900 @@ -221,7 +221,7 @@ -- product on arbitrary index -- - record IsIProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) + record IsIProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) ( p : Obj A ) -- product ( ai : I → Obj A ) -- families ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections @@ -249,11 +249,11 @@ iproduct qi ∎ - record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + record IProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where field iprod : Obj A pi : (i : I ) → Hom A iprod ( ai i ) - isIProduct : IsIProduct A I iprod ai pi + isIProduct : IsIProduct I A iprod ai pi -- Pullback @@ -299,9 +299,9 @@ -- Constancy Functor - K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) + K : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( A : Category c₁'' c₂'' ℓ'' ) → ( a : Obj A ) → Functor I A - K A I a = record { + K I A a = record { FObj = λ i → a ; FMap = λ f → id1 A a ; isFunctor = let open ≈-Reasoning (A) in record { @@ -312,65 +312,65 @@ } - 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 + record IsLimit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) + (a0 : Obj A ) (t0 : NTrans I A ( K I A 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 } → + limit : ( a : Obj A ) → ( t : NTrans I A ( K I A a ) Γ ) → Hom A a a0 + t0f=t : { a : Obj A } → { t : NTrans I A ( K I A 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 } → + limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I A 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 ) + record Limit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : 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 + t0 : NTrans I A ( K I A a0 ) Γ + isLimit : IsLimit I A Γ a0 t0 - LimitNat : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} + LimitNat : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( B : 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 { + ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) → + ( U : Functor B C) → NTrans I C ( K I C (FObj U lim) ) (U ○ Γ) + LimitNat I B 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 + TMap (Functor*Nat I C U tb) b o FMap (U ○ K I B lim) f ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ - TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f + TMap (Functor*Nat I C U tb) b o FMap (K I C (FObj U lim)) f ∎ } } open Limit - record LimitPreserve { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) + record LimitPreserve { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : 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 ○ Γ ) + preserve : ( Γ : Functor I A ) → ( limita : Limit I A Γ ) → + IsLimit I C (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat I A C Γ (a0 limita ) (t0 limita) G ) + plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ ) plimit {Γ} limita = record { a0 = (FObj G (a0 limita )) - ; t0 = LimitNat A I C Γ (a0 limita ) (t0 limita) G + ; t0 = LimitNat I A 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₂' ℓ' ) + record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - climit : ( Γ : Functor I A ) → Limit A I Γ + climit : ( Γ : Functor I A ) → Limit I A Γ record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - climit : ( Γ : Functor I A ) → Limit A I Γ - cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct A I fi -- c₁ should be a free level + climit : ( Γ : Functor I A ) → Limit I A Γ + cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g open Limit limit-c : ( Γ : Functor I A ) → Obj A limit-c Γ = a0 ( climit Γ) - limit-u : ( Γ : Functor I A ) → NTrans I A ( K A I (limit-c Γ )) Γ + limit-u : ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ limit-u Γ = t0 ( climit Γ) open Equalizer equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A
--- a/freyd.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/freyd.agda Sun Nov 12 09:56:40 2017 +0900 @@ -50,7 +50,7 @@ initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A A) (SFS : SmallFullSubcategory A ) → - (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS)) + (PI : PreInitial A (SFSF SFS )) → IsInitialObject A (limit-c comp (SFSF SFS)) initialFromPreInitialFullSubcategory A comp SFS PI = record { initial = initialArrow ; uniqueness = λ {a} f → lemma1 a f
--- a/freyd1.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/freyd1.agda Sun Nov 12 09:56:40 2017 +0900 @@ -51,13 +51,13 @@ --- Get a nat on A from a nat on CommaCategory -- 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 Γ) + (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K I CommaCategory c ) Γ ) → NTrans I A ( K I A (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 ] ] + A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K I A (obj c)) f ] ] comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) @@ -67,19 +67,19 @@ -- LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) - → Limit C I (G ○ (FIA Γ)) + → ( glimit : LimitPreserve I A C G ) + → Limit I C (G ○ (FIA Γ)) LimitC {I} comp Γ glimit = plimit glimit (climit comp (FIA Γ)) tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) + → NTrans I C (K I C (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) tu {I} comp Γ = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ] ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } } where commute : {a b : Obj I} {f : Hom I a b} → C [ C [ FMap (G ○ (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a) ] ] - ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] + ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ] ] commute {a} {b} {f} = let open ≈-Reasoning (C) in begin FMap (G ○ (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a )) ≈⟨⟩ @@ -95,7 +95,7 @@ ≈⟨⟩ hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ) f o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ))) ))) ⟩ - hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] )) + hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K I A (a0 (climit comp (FIA Γ)))) f ] )) ≈⟨⟩ hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] )) ≈⟨ cdr ( distr F ) ⟩ @@ -103,14 +103,14 @@ ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩ hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ)))) ≈⟨ assoc ⟩ - ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f + ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ∎ limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) + → ( glimit : LimitPreserve I A C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) + → ( glimit : LimitPreserve I A C G ) → Obj CommaCategory commaLimit {I} comp Γ glimit = record { obj = limit-c comp (FIA Γ) @@ -119,8 +119,8 @@ commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) - → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit)) Γ + → ( glimit : LimitPreserve I A C G ) + → NTrans I CommaCategory (K I CommaCategory (commaLimit {I} comp Γ glimit)) Γ commaNat {I} comp Γ glimit = record { TMap = λ x → record { arrow = TMap ( limit-u comp (FIA Γ ) ) x @@ -129,10 +129,10 @@ ; isNTrans = record { commute = comm2 } } where comm1 : (x : Obj I ) → - C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] + C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] comm1 x = let open ≈-Reasoning (C) in begin - FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) + FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x) ≈⟨⟩ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) ≈⟨⟩ @@ -146,23 +146,23 @@ ∎ comm2 : {a b : Obj I} {f : Hom I a b} → CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ] - ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ] + ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K I CommaCategory (commaLimit comp Γ glimit)) f ] ] comm2 {a} {b} {f} = let open ≈-Reasoning (A) in begin FMap (FIA Γ) f o TMap (limit-u comp (FIA Γ)) a ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ))) ⟩ - TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f + TMap (limit-u comp (FIA Γ)) b o FMap (K I A (limit-c comp (FIA Γ))) f ∎ gnat : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) - → (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → - NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) + → (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → + NTrans I C (K I C (FObj F (obj a))) (G ○ FIA Γ) gnat {I} Γ a t = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ] ; isNTrans = record { commute = λ {x y f} → comm1 x y f } } where comm1 : (x y : Obj I) (f : Hom I x y ) → C [ C [ FMap (G ○ FIA Γ) f o C [ hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x) ] ] - ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K C I (FObj F (obj a))) f ] ] + ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K I C (FObj F (obj a))) f ] ] comm1 x y f = let open ≈-Reasoning (C) in begin FMap (G ○ FIA Γ) f o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x )) ≈⟨⟩ @@ -180,12 +180,12 @@ ≈⟨ cdr ( fcong F ( IsCategory.identityR (Category.isCategory A))) ⟩ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ≈↑⟨ idR ⟩ - ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K C I (FObj F (obj a))) f + ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K I C (FObj F (obj a))) f ∎ comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) + → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) comma-a0 {I} comp Γ glimit a t = record { arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) ; comm = comm1 @@ -243,7 +243,7 @@ ∎ comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) (i : Obj I ) + → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) (i : Obj I ) → CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ] comma-t0f=t {I} comp Γ glimit a t i = let open ≈-Reasoning (A) in begin TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) @@ -252,7 +252,7 @@ ∎ comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) + → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → ( f : Hom CommaCategory a (commaLimit comp Γ glimit)) → ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat { I} comp Γ glimit ) i o f ] ≈ TMap t i ] ) → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ] @@ -263,9 +263,9 @@ ∎ hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) - → ( glimit : LimitPreserve A I C G ) + → ( glimit : LimitPreserve I A C G ) → ( Γ : Functor I CommaCategory ) - → Limit CommaCategory I Γ + → Limit I CommaCategory Γ hasLimit {I} comp glimit Γ = record { a0 = commaLimit {I} comp Γ glimit ; t0 = commaNat { I} comp Γ glimit ;
--- a/freyd2.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/freyd2.agda Sun Nov 12 09:56:40 2017 +0900 @@ -100,27 +100,27 @@ YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) - (Γ : Functor I A) (limita : Limit A I Γ) → - IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) + (Γ : Functor I A) (limita : Limit I A Γ) → + IsLimit I Sets (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat I A Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t } where - hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) - hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b) + hat0 : NTrans I Sets (K I Sets (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) + hat0 = LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b) haa0 : Obj Sets haa0 = FObj (Yoneda A b) (a0 lim) - ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ + ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) → NTrans I A (K I A b ) Γ ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → - A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ] + A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K I A b) f ] ] commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin FMap Γ f o TMap t a₁ x ≈⟨⟩ ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ - ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x + ( TMap t b₁ * ( FMap (K I Sets a) f ) ) x ≈⟨⟩ ( TMap t b₁ * id1 Sets a ) x ≈⟨⟩ @@ -128,15 +128,15 @@ ≈↑⟨ idR ⟩ TMap t b₁ x o id1 A b ≈⟨⟩ - TMap t b₁ x o FMap (K A I b) f + TMap t b₁ x o FMap (K I A b) f ∎ - ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ)) + ψ : (X : Obj Sets) ( t : NTrans I Sets (K I Sets X) (Yoneda A b ○ Γ)) → Hom Sets X (FObj (Yoneda A b) (a0 lim)) ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) - t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I) - → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] + t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) (i : Obj I) + → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin - ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x + ( Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x ≈⟨⟩ FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] @@ -148,8 +148,8 @@ ≈⟨⟩ TMap t i x ∎ )) - limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → - ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → + limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → + ({i : Obj I} → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → Sets [ ψ a t ≈ f ] limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin ψ a t x @@ -164,9 +164,9 @@ ∎ )) -YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) - (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) -YonedaFpreserveLimit A I b = record { +YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) + (b : Obj A ) → LimitPreserve I A Sets (Yoneda A b) +YonedaFpreserveLimit I A b = record { preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim } @@ -181,14 +181,14 @@ KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) - → IsInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) + → IsInitialObject ( K A Sets * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { initial = λ b → initial0 b ; uniqueness = λ f → unique f } where commaCat : Category (c₂ ⊔ c₁) c₂ ℓ - commaCat = K Sets A * ↓ Yoneda A a - initObj : Obj (K Sets A * ↓ Yoneda A a) + commaCat = K A Sets * ↓ Yoneda A a + initObj : Obj (K A Sets * ↓ Yoneda A a) initObj = record { obj = a ; hom = λ x → id1 A a } comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x comm2 b OneObj = let open ≈-Reasoning A in ≈-≡ A ( begin @@ -200,13 +200,13 @@ ≈⟨ idR ⟩ hom b OneObj ∎ ) - comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ] + comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K A Sets *) (hom b OneObj) ] ] comm1 b = let open ≈-Reasoning Sets in begin FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a ) ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩ hom b ≈⟨⟩ - hom b o FMap (K Sets A *) (hom b OneObj) + hom b o FMap (K A Sets *) (hom b OneObj) ∎ initial0 : (b : Obj commaCat) → Hom commaCat initObj b @@ -214,12 +214,12 @@ arrow = hom b OneObj ; comm = comm1 b } -- what is comm f ? - comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) + comm-f : (b : Obj (K A Sets * ↓ (Yoneda A a))) (f : Hom (K A Sets * ↓ Yoneda A a) initObj b) → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] - ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ] + ≈ Sets [ hom b o FMap (K A Sets *) (arrow f) ] ] comm-f b f = comm f - unique : {b : Obj (K Sets A * ↓ Yoneda A a)} (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) - → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ] + unique : {b : Obj (K A Sets * ↓ Yoneda A a)} (f : Hom (K A Sets * ↓ Yoneda A a) initObj b) + → (K A Sets * ↓ Yoneda A a) [ f ≈ initial0 b ] unique {b} f = let open ≈-Reasoning A in begin arrow f ≈↑⟨ idR ⟩ @@ -229,7 +229,7 @@ ≈⟨⟩ ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩ - ( Sets [ hom b o FMap (K Sets A *) (arrow f) ] ) OneObj + ( Sets [ hom b o FMap (K A Sets *) (arrow f) ] ) OneObj ≈⟨⟩ hom b OneObj ∎ @@ -244,19 +244,19 @@ ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) - → Hom Sets (FObj (K Sets A *) b) (FObj U b) + → Hom Sets (FObj (K A Sets *) b) (FObj U b) ub A U b x OneObj = x ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) - → Obj ( K Sets A * ↓ U) + → Obj ( K A Sets * ↓ U) ob A U b x = record { obj = b ; hom = ub A U b x} fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a ) - → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) + → Hom ( K A Sets * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x } where fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y fArrowComm1 a b f x OneObj = refl fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → - Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ] + Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K A Sets *) f ] ] fArrowComm a b f x = extensionality Sets ( λ y → begin ( Sets [ FMap U f o hom (ob A U a x) ] ) y ≡⟨⟩ @@ -276,8 +276,8 @@ UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) - ( i : Obj ( K (Sets) A * ↓ U) ) - (In : IsInitialObject ( K (Sets) A * ↓ U) i ) + ( i : Obj ( K A Sets * ↓ U) ) + (In : IsInitialObject ( K A Sets * ↓ U) i ) → Representable A U (obj i) UisRepresentable A U i In = record { repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } @@ -294,7 +294,7 @@ A [ f o arrow (initial In (ob A U a y)) ] ≡⟨⟩ A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ] - ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ + ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K A Sets * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ arrow (initial In (ob A U b (FMap U f y) )) ≡⟨⟩ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y @@ -339,7 +339,7 @@ tmap2 b o FMap (Yoneda A (obj i)) f ∎ iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) - → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z + → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K A Sets *) y ] ) z iso0 x y OneObj = refl iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin @@ -368,19 +368,19 @@ module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) (U : Functor A B ) - (i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → IsInitialObject ( K B A b ↓ U) (i b) ) + (i : (b : Obj B) → Obj ( K A B b ↓ U) ) + (In : (b : Obj B) → IsInitialObject ( K A B b ↓ U) (i b) ) where tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y))) tmap-η y = hom (i y) - sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U + sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K A B a) U sobj {a} {b} f = record {obj = b; hom = f } - solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f) + solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K A B a) U (i a) (sobj f) solution {a} {b} f = initial (In a) (sobj f) - ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) + ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K A B a ↓ U) ηf a b f = sobj ( B [ tmap-η b o f ] ) univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b)) @@ -388,7 +388,7 @@ univ {a} {b} f = let open ≈-Reasoning B in begin FMap U (arrow (solution f)) o tmap-η a ≈⟨ comm (initial (In a) (sobj f)) ⟩ - hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f))) + hom (sobj f) o FMap (K A B a) (arrow (initial (In a) (sobj f))) ≈⟨ idR ⟩ f ∎ @@ -402,7 +402,7 @@ ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ g ∎ where - comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ] + comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K A B a) g ] ] comm1 = let open ≈-Reasoning B in sym idR UM : UniversalMapping B A U
--- a/limit-to.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/limit-to.agda Sun Nov 12 09:56:40 2017 +0900 @@ -110,7 +110,7 @@ IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → {a b : Obj A} (f g : Hom A a b ) (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → - NTrans TwoCat A (K A TwoCat d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g) + NTrans TwoCat A (K TwoCat A d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g) IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record { TMap = λ x → nmap x d h ; isNTrans = record { @@ -120,11 +120,11 @@ I = TwoCat {c₁} {c₂} Γ : Functor I A Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g - nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x) + nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K I A d) x) (FObj Γ x) nmap t0 d h = h nmap t1 d h = A [ f o h ] commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] - → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] + → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K I A d) f' ] ] commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin f o h ≈↑⟨ idR ⟩ @@ -153,13 +153,13 @@ ∎ -equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} → (f g : Hom A a b) (lim : Limit A TwoCat (IndexFunctor A a b f g) ) → +equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} → (f g : Hom A a b) (lim : Limit TwoCat A (IndexFunctor A a b f g) ) → Hom A (a0 lim) a equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) discrete.t0 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → {a b : Obj A} (f g : Hom A a b ) - (lim : Limit A TwoCat (IndexFunctor A a b f g) ) + (lim : Limit TwoCat A (IndexFunctor A a b f g) ) → IsEqualizer A (equlimit A f g lim) f g lim-to-equ {c₁} {c₂} {ℓ} A {a} {b} f g lim = record { fe=ge = fe=ge0 @@ -175,7 +175,7 @@ e = equlimit A f g lim c : Obj A c = a0 lim - 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 : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K I A d) Γ inat = IndexNat A f g fe=ge0 : A [ A [ f o (equlimit A f g lim ) ] ≈ A [ g o (equlimit A f g lim ) ] ] fe=ge0 = let open ≈-Reasoning A in begin @@ -183,7 +183,7 @@ ≈⟨⟩ FMap Γ arrow-f o TMap (Limit.t0 lim) discrete.t0 ≈⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-f} ⟩ - TMap (Limit.t0 lim) discrete.t1 o FMap (K A (TwoCat {c₁} {c₂} ) (a0 lim)) id-t0 + TMap (Limit.t0 lim) discrete.t1 o FMap (K (TwoCat {c₁} {c₂} ) A (a0 lim)) id-t0 ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-g} ⟩ FMap Γ arrow-g o TMap (Limit.t0 lim) discrete.t0 ≈⟨⟩ @@ -218,7 +218,7 @@ ≈↑⟨ car (idR) ⟩ ( TMap (Limit.t0 lim) t1 o id c ) o k' ≈⟨⟩ - ( TMap (Limit.t0 lim) t1 o FMap (K A I c) arrow-f ) o k' + ( TMap (Limit.t0 lim) t1 o FMap (K I A c) arrow-f ) o k' ≈↑⟨ car ( nat1 (Limit.t0 lim) arrow-f ) ⟩ ( FMap Γ arrow-f o TMap (Limit.t0 lim) discrete.t0 ) o k' ≈⟨⟩ @@ -245,22 +245,22 @@ open DiscreteHom plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) - → ( Γ : Functor (DiscreteCat S ) A ) → (lim : Limit A ( DiscreteCat S ) Γ ) → Obj A + → ( Γ : Functor (DiscreteCat S ) A ) → (lim : Limit ( DiscreteCat S ) A Γ ) → Obj A plimit A S Γ lim = a0 lim discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ] discrete-identity f = refl pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) - → (Γ : Functor (DiscreteCat S ) A ) + → (Γ : Functor (DiscreteCat S) A ) → {q : Obj A } ( qi : (i : Obj ( DiscreteCat S)) → Hom A q (FObj Γ i) ) - → NTrans (DiscreteCat S )A (K A (DiscreteCat S) q) Γ + → NTrans (DiscreteCat S )A (K (DiscreteCat S) A q) Γ pnat A S Γ {q} qi = record { TMap = qi ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } } where - commute : {a b : Obj (DiscreteCat S) } {f : Hom ( DiscreteCat S) a b} → - A [ A [ FMap Γ f o qi a ] ≈ A [ qi b o FMap (K A (DiscreteCat S )q) f ] ] + commute : {a b : Obj (DiscreteCat S) } {f : Hom (DiscreteCat S) a b} → + A [ A [ FMap Γ f o qi a ] ≈ A [ qi b o FMap (K (DiscreteCat S) A q) f ] ] commute {a} {b} {f} with discrete f commute {a} {.a} {f} | refl = let open ≈-Reasoning A in begin FMap Γ f o qi a @@ -273,20 +273,19 @@ ≈↑⟨ idR ⟩ qi a o id q ≈⟨⟩ - qi a o FMap (K A (DiscreteCat S) q) f + qi a o FMap (K (DiscreteCat S) A q) f ∎ lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ ) - → ( Γ : Functor (DiscreteCat S ) A ) - → (lim : Limit A ( DiscreteCat S ) Γ ) - → IProduct A (Obj ( DiscreteCat S ) ) + → ( Γ : Functor (DiscreteCat S) A ) + → (lim : Limit (DiscreteCat S) A Γ ) + → IProduct (Obj (DiscreteCat S)) A (FObj Γ) lim-to-product A S Γ lim = record { - ai = λ i → FObj Γ i - ; iprod = plimit A S Γ lim + iprod = plimit A S Γ lim ; pi = λ i → TMap (Limit.t0 lim) i ; isIProduct = record { iproduct = λ {q} qi → iproduct {q} qi ; - pif=q = λ {q } qi { i } → pif=q {q} qi {i} ; + pif=q = λ {q} {qi} {i} → pif=q {q} qi {i} ; ip-uniqueness = λ {q } { h } → ip-uniqueness {q} {h} ; ip-cong = λ {q } { qi } { qi' } qi=qi' → ip-cong {q} {qi} {qi'} qi=qi' }
--- a/pullback.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/pullback.agda Sun Nov 12 09:56:40 2017 +0900 @@ -150,18 +150,18 @@ open NTrans iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) - ( lim : Limit A I Γ ) → ( lim' : Limit A I Γ ) + ( lim : Limit I A Γ ) → ( lim' : Limit I A Γ ) → Hom A (a0 lim )(a0 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 Γ ) + ( lim : Limit I A Γ ) → ( lim' : Limit I A Γ ) → Hom A (a0 lim') (a0 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 ) - ( lim : Limit A I Γ ) → ( lim' : Limit A I Γ ) → + ( lim : Limit I A Γ ) → ( lim' : Limit I A Γ ) → ∀{ 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' @@ -193,8 +193,8 @@ 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) + FObj = λ a → K I A a ; + FMap = λ f → record { -- NTrans I A (K I A a) (K I A b) TMap = λ a → f ; isNTrans = record { commute = λ {a b f₁} → commute1 {a} {b} {f₁} f @@ -207,13 +207,13 @@ } } 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₁ ] ] + A [ A [ FMap (K I A b') f₁ o f ] ≈ A [ f o FMap (K I A a') f₁ ] ] commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin - FMap (K A I b') f₁ o f + FMap (K I A b') f₁ o f ≈⟨ idL ⟩ f ≈↑⟨ idR ⟩ - f o FMap (K A I a') f₁ + f o FMap (K I A a') f₁ ∎ @@ -234,7 +234,7 @@ -- a0 : Obj A and t0 : NTrans K Γ come from the limit limit2couniv : - ( lim : ( Γ : Functor I A ) → Limit A I Γ ) + ( lim : ( Γ : Functor I A ) → Limit I A Γ ) → coUniversalMapping A ( A ^ I ) (KI I) limit2couniv lim = record { U = λ b → a0 ( lim b) ; @@ -267,7 +267,7 @@ univ2limit : ( univ : coUniversalMapping A (A ^ I) (KI I) ) → - ( Γ : Functor I A ) → Limit A I Γ + ( Γ : Functor I A ) → Limit I A Γ univ2limit univ Γ = record { a0 = (coUniversalMapping.U univ ) Γ ; t0 = (coUniversalMapping.ε univ ) Γ ; @@ -283,7 +283,7 @@ ε 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 A I a) Γ} {i : Obj I} → + 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 @@ -292,7 +292,7 @@ ≈⟨ coIsUniversalMapping.couniversalMapping ( 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 Γ)} + 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 @@ -355,9 +355,9 @@ Homprod {j} {k} u = record {hom-j = j ; hom-k = k ; hom = u} limit-from : - ( prod : {c : Level} { I : Set c } → ( ai : I → Obj A ) → IProduct A I ai ) + ( 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 A I Γ + → Limit I A Γ limit-from prod eqa = record { a0 = d ; t0 = cone-ε ; @@ -389,15 +389,15 @@ -- 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 A I (equalizer-c equ-ε ) ) Γ + 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 A I d) i) (FObj Γ i) + 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 A I d) u ] ] + 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 ≈⟨⟩ @@ -419,12 +419,12 @@ ≈↑⟨ idR ⟩ (proj k o e ) o id1 A d ≈⟨⟩ - tmap k o FMap (K A I d) u + tmap k o FMap (K I A d) u ∎ -- 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 A I a) Γ ) → Hom A a p0 + 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 A I a) Γ ) → + 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 @@ -456,9 +456,9 @@ ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ f o h t ∎ - cone1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d + 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 ) - t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → + t0f=t1 : {a : Obj A} {t : NTrans I A (K I A a) Γ} {i : Obj I} → A [ A [ TMap cone-ε i o cone1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin TMap cone-ε i o cone1 a t @@ -471,7 +471,7 @@ ≈⟨ pif=q prodΓ ⟩ TMap t i ∎ - limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a d} + limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K I A a) Γ} {f : Hom A a d} → ({i : Obj I} → A [ A [ TMap cone-ε i o f ] ≈ TMap t i ]) → A [ cone1 a t ≈ f ] limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin @@ -504,22 +504,22 @@ 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 ○ Γ) + ( 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 B I lim) f + 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 A I (FObj U lim)) f + TMap (Functor*Nat I A U tb) b o FMap (K I A (FObj U lim)) f ∎ } } adjoint-preseve-limit : - { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit B I Γ ) → - ( adj : Adjunction A B ) → Limit A I (Adjunction.U adj ○ Γ) + { 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 ; @@ -540,9 +540,9 @@ 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 : 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 A I a) (U ○ Γ) → NTrans I B (K B I (FObj F a)) Γ + 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 @@ -558,20 +558,20 @@ ≈↑⟨ 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 FMap (K I A a) f ]) ≈⟨⟩ - TMap ε (FObj Γ b) o FMap F (A [ TMap t b o id1 A (FObj (K A I a) b) ]) + 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 A I a) b)) + ( 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 B I (FObj F a)) f + tfmap a t b o FMap (K I B (FObj F a)) f ∎ } } - limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) ) + 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 A I a) (U ○ Γ)} {i : Obj I} → + 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 @@ -599,7 +599,7 @@ 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)} + 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