Mercurial > hg > Members > kono > Proof > category
changeset 468:c375d8f93a2c
discrete category and product from a limit
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 06 Mar 2017 15:45:51 +0900 |
| parents | ba042c2d3ff5 |
| children | 65ab0da524b8 36d13c7182c1 |
| files | cat-utility.agda discrete.agda limit-to.agda pullback.agda yoneda.agda |
| diffstat | 5 files changed, 245 insertions(+), 117 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sun Mar 05 11:14:32 2017 +0900 +++ b/cat-utility.agda Mon Mar 06 15:45:51 2017 +0900 @@ -13,53 +13,53 @@ id1 A a = (Id {_} {_} {_} {A} a) -- We cannot make A implicit - record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Obj A → Obj B ) ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → + universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → A [ A [ FMap U ( f * ) o η a ] ≈ f ] - uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → + uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } → A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ] - record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Obj A → Obj B ) ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where infixr 11 _* field - _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b + _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b isUniversalMapping : IsUniversalMapping A B U F η _* - record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( F : Functor A B ) ( U : Obj B → Obj A ) ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) ( _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → + couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → B [ B [ ε b o FMap F ( f *' ) ] ≈ f ] - couniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } → + couniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } → B [ B [ ε b o FMap F g ] ≈ f ] → A [ f *' ≈ g ] - record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( F : Functor A B ) ( U : Obj B → Obj A ) ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where infixr 11 _*' field - _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) + _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) iscoUniversalMapping : coIsUniversalMapping A B F U ε _*' open NTrans open import Category.Cat - record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) ( η : NTrans A A identityFunctor ( U ○ F ) ) @@ -71,7 +71,7 @@ adjoint2 : {a : Obj A} → B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] - record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) ( η : NTrans A A identityFunctor ( U ○ F ) ) @@ -85,7 +85,7 @@ Epsiron = ε - record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A ) ( η : NTrans A A identityFunctor T ) ( μ : NTrans A A (T ○ T) T) @@ -113,10 +113,10 @@ commute = commute } } where - commute : {a b : Obj A} {f : Hom A a b} + commute : {a b : Obj A} {f : Hom A a b} → C [ C [ (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ] ≈ C [ (FMap F (TMap n b )) o (FMap F (FMap G f)) ] ] commute {a} {b} {f} = let open ≈-Reasoning (C) in - begin + begin (FMap F ( FMap H f )) o ( FMap F (TMap n a)) ≈⟨ sym (distr F) ⟩ FMap F ( B [ (FMap H f) o TMap n a ]) @@ -134,28 +134,28 @@ commute = commute } } where - commute : {a b : Obj A} {f : Hom A a b} + commute : {a b : Obj A} {f : Hom A a b} → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] - commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) + commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) -- T ≃ (U_R ○ F_R) -- μ = U_R ε F_R -- nat-ε -- nat-η -- same as η but has different types - record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) - ( T : Functor A A ) + record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) + ( T : Functor A A ) -- { η : NTrans A A identityFunctor T } -- { μ : NTrans A A (T ○ T) T } -- { M : Monad A T η μ } ( UR : Functor B A ) ( FR : Functor A B ) - { ηR : NTrans A A identityFunctor ( UR ○ FR ) } - { εR : NTrans B B ( FR ○ UR ) identityFunctor } + { ηR : NTrans A A identityFunctor ( UR ○ FR ) } + { εR : NTrans B B ( FR ○ UR ) identityFunctor } { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } ( Adj : Adjunction A B UR FR ηR εR ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - T=UF : T ≃ (UR ○ FR) + T=UF : T ≃ (UR ○ FR) μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] -- ηR=η : {x : Obj A } → A [ TMap ηR x ≈ TMap η x ] -- We need T → UR FR conversion -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ] @@ -184,9 +184,9 @@ field equalizer-c : Obj A equalizer : Hom A equalizer-c a - isEqualizer : IsEqualizer A equalizer f g + isEqualizer : IsEqualizer A equalizer f g - -- + -- -- Product -- -- c @@ -197,7 +197,7 @@ -- π1 π2 - record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) + record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where @@ -206,48 +206,81 @@ π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ] π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ] uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] - ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] + ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] - record CreateProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + record CreateProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where field product : (a b : Obj A) -> Obj A - π1 : (a b : Obj A) -> Hom A (product a b ) a - π2 : (a b : Obj A) -> Hom A (product a b ) b + π1 : (a b : Obj A) -> Hom A (product a b ) a + π2 : (a b : Obj A) -> Hom A (product a b ) b isProduct : (a b : Obj A) -> Product A a b (product a b) (π1 a b ) (π2 a b) + ----- + -- + -- product on arbitrary index + -- + + record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) + ( p : Obj A ) -- product + ( ai : I → Obj A ) -- families + ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections + : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p + pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] + ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] + ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } + → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] + -- another form of uniquness + ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) + → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) + → A [ product' ≈ iproduct qi ] + ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin + product' + ≈↑⟨ ip-uniqueness ⟩ + iproduct (λ i₁ → A [ pi i₁ o product' ]) + ≈⟨ ip-cong ( λ i → begin + pi i o product' + ≈⟨ eq {i} ⟩ + qi i + ∎ ) ⟩ + iproduct qi + ∎ + + -- Pullback -- f -- a ------→ c - -- ^ ^ + -- ^ ^ -- π1 | |g -- | | -- ab ------→ b -- ^ π2 -- | - -- d + -- d -- - record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) + record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) ( f : Hom A a c ) ( g : Hom A b c ) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where field commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] p : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab - π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } - → A [ A [ π1 o p eq ] ≈ π1' ] - π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } - → A [ A [ π2 o p eq ] ≈ π2' ] - uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π1 o p eq ] ≈ π1' ] + π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π2 o p eq ] ≈ π2' ] + uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] } → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] } → A [ p eq ≈ p' ] axb : Obj A axb = ab - pi1 : Hom A ab a - pi1 = π1 - pi2 : Hom A ab b - pi2 = π2 + pi1 : Hom A ab a + pi1 = π1 + pi2 : Hom A ab b + pi2 = π2 -- -- Limit @@ -256,7 +289,7 @@ -- Constancy Functor - K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) + K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) → ( a : Obj A ) → Functor I A K A I a = record { FObj = λ i → a ; @@ -282,25 +315,25 @@ 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₂' ℓ' ) + 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-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 Γ) - record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) + 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-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 Γ) product : (a b : Obj A) -> Obj A - π1 : (a b : Obj A) -> Hom A (product a b ) a - π2 : (a b : Obj A) -> Hom A (product a b ) b + π1 : (a b : Obj A) -> Hom A (product a b ) a + π2 : (a b : Obj A) -> Hom A (product a b ) b isProduct : (a b : Obj A) -> Product A a b (product a b) (π1 a b ) (π2 a b) 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 + isEqualizer : {a b : Obj A} (f g : Hom A a b) -> IsEqualizer A (equalizer-e f g) f g
--- a/discrete.agda Sun Mar 05 11:14:32 2017 +0900 +++ b/discrete.agda Mon Mar 06 15:45:51 2017 +0900 @@ -58,7 +58,7 @@ TwoId {_} {_} t0 = id-t0 TwoId {_} {_} t1 = id-t1 -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ TwoCat {c₁} {c₂} = record { @@ -88,3 +88,55 @@ o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl + + +-- Category with no arrow but identity + +record DiscreteObj {c₁ : Level } : Set c₁ + where + +open DiscreteObj + +record DiscreteHom { c₁ : Level} (a : DiscreteObj {c₁} ) (b : DiscreteObj {c₁} ) + : Set c₁ where + +open DiscreteHom + +_*_ : ∀ {c₁} → {a b c : DiscreteObj {c₁}} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c +_*_ {_} {a} {b} {c} x _ = record { } + +DiscreteId : { c₁ : Level} ( a : DiscreteObj ) → DiscreteHom {c₁} a a +DiscreteId a = record { } + +assoc-* : {c₁ : Level } {a b c d : DiscreteObj {c₁} } + {f : (DiscreteHom {c₁} c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} → + ( f * (g * h)) ≡ ((f * g) * h ) +assoc-* {c₁} {a} {b} {c} {d} {f} {g} {h } = refl + +DiscreteCat : {c₁ : Level } → Category c₁ c₁ c₁ +DiscreteCat {c₁} = record { + Obj = DiscreteObj ; + Hom = λ a b → DiscreteHom a b ; + _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {a} {b} {c} x y ; + _≈_ = λ x y → x ≡ y ; + Id = λ{a} → DiscreteId a ; + isCategory = record { + isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; + identityL = λ{a b f} → identityL {c₁} {a} {b} {f} ; + identityR = λ{a b f} → identityR {c₁} {a} {b} {f} ; + o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {a} {b} {c} {f} {g} {h} {i} ; + associative = λ{a b c d f g h } → assoc-* {c₁} {a} {b} {c} {d} {f} {g} {h} + } + } where + identityL : {c₁ : Level } {a b : DiscreteObj {c₁}} {f : ( DiscreteHom {c₁} a b) } → ((DiscreteId b) * f) ≡ f + identityL {c₁} {a} {b} {f} = refl + identityR : {c₁ : Level } {A B : DiscreteObj {c₁}} {f : ( DiscreteHom {c₁} A B) } → ( f * DiscreteId A ) ≡ f + identityR {c₁} {a} {b} {f} = refl + o-resp-≈ : {c₁ : Level } {A B C : DiscreteObj {c₁} } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → + f ≡ g → h ≡ i → ( h * f ) ≡ ( i * g ) + o-resp-≈ {c₁} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl + + + + +
--- a/limit-to.agda Sun Mar 05 11:14:32 2017 +0900 +++ b/limit-to.agda Mon Mar 06 15:45:51 2017 +0900 @@ -29,8 +29,8 @@ --- \ t0 t1 I --- -----→ --- ag ---- ---- +--- +--- open Complete open Limit @@ -100,7 +100,7 @@ ∎ --- Nat for Limit --- +-- -- Nat : K -> IndexFunctor -- @@ -108,12 +108,12 @@ 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 ] ] → + (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) IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record { TMap = λ x → nmap x d h ; isNTrans = record { - commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh + commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh } } where I = TwoCat {c₁} {c₂} @@ -121,7 +121,7 @@ Γ = 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 t0 d h = h - nmap t1 d h = A [ f o 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' ] ] commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin @@ -148,18 +148,18 @@ ≈⟨ idL ⟩ f o h ≈↑⟨ idR ⟩ - ( f o h ) o id d + ( f o h ) o id d ∎ -equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A TwoCat ) -> +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 -lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) +lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A TwoCat ) - → {a b : Obj A} (f g : Hom A a b ) - → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] ) + → {a b : Obj A} (f g : Hom A a b ) + → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] ) → IsEqualizer A (equlimit A f g comp) f g lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record { fe=ge = fe=ge @@ -167,18 +167,18 @@ ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where - I : Category c₁ c₂ c₂ - I = TwoCat + I : Category c₁ c₂ c₂ + I = TwoCat Γ : Functor I A Γ = IndexFunctor A a b f g e : Hom A (limit-c comp (IndexFunctor A a b f g)) a e = equlimit A f g comp - c : Obj A + c : Obj A c = limit-c comp Γ lim : Limit A I Γ c ( limit-u comp Γ ) - lim = isLimit comp Γ + 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 + 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 ) 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 ] @@ -191,8 +191,8 @@ ≈⟨⟩ h ∎ - uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) - ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → + uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) + ( 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' @@ -229,3 +229,78 @@ k' ∎ + +plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A ( DiscreteCat {c₁} ) ) + → ( Γ : Functor (DiscreteCat {c₁}) A ) → Obj A +plimit A comp Γ = limit-c comp Γ + +pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A ( DiscreteCat {c₁} ) ) + → (Γ : Functor (DiscreteCat {c₁}) A ) + → (q : Obj A ) ( qi : (i : Obj ( DiscreteCat {c₁} )) → Hom A q (FObj Γ i) ) + → NTrans DiscreteCat A (K A DiscreteCat q) Γ +pnat {c₁} A comp Γ q qi = record { + TMap = qi ; + isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } + } where + commute : {a b : Obj (DiscreteCat {c₁}) } {f : Hom ( DiscreteCat {c₁}) a b} → + A [ A [ FMap Γ f o qi a ] ≈ + A [ qi b o FMap (K A (DiscreteCat {c₁} )q) f ] ] + commute {a} {b} {f} = let open ≈-Reasoning A in begin + FMap Γ f o qi a + ≈⟨⟩ + FMap Γ (id1 (DiscreteCat {c₁}) b ) o qi a + ≈⟨ car ( IsFunctor.identity ( isFunctor Γ )) ⟩ + id (FObj Γ b) o qi a + ≈⟨ idL ⟩ + qi a + ≈⟨⟩ + qi b + ≈↑⟨ idR ⟩ + qi b o id q + ≈⟨⟩ + qi b o FMap (K A (DiscreteCat {c₁} )q) f + ∎ + +lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + (comp : Complete A ( DiscreteCat {c₁} ) ) + → ( Γ : Functor (DiscreteCat {c₁}) A ) + → IProduct {c₁} A (Obj ( DiscreteCat {c₁}) )(plimit A comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u comp Γ) i ) +lim-to-product {c₁} A comp Γ = record { + iproduct = λ {q} qi → iproduct {q} qi ; + 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' + } where + D = DiscreteCat {c₁} + I = Obj ( DiscreteCat {c₁} ) + lim = isLimit 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 comp Γ q 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 comp Γ q 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 comp Γ q (λ 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 comp Γ q 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 comp Γ q qi' ) + ≈⟨ t0f=t lim {q} {pnat A comp Γ q qi'} {i} ⟩ + TMap (pnat A comp Γ q qi') i + ≈⟨⟩ + qi' i + ≈↑⟨ qi=qi' ⟩ + qi i + ≈⟨⟩ + TMap (pnat A comp Γ q qi) i + ∎ + 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 comp Γ q qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))
--- a/pullback.agda Sun Mar 05 11:14:32 2017 +0900 +++ b/pullback.agda Mon Mar 06 15:45:51 2017 +0900 @@ -293,38 +293,6 @@ ∎ ------ --- --- product on arbitrary index --- - -record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) - ( p : Obj A ) -- product - ( ai : I → Obj A ) -- families - ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections - : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where - field - product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p - pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ] - ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] - ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } - → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] - -- another form of uniquness - ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) - → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) - → A [ product' ≈ product qi ] - ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin - product' - ≈↑⟨ ip-uniqueness ⟩ - product (λ i₁ → A [ pi i₁ o product' ]) - ≈⟨ ip-cong ( λ i → begin - pi i o product' - ≈⟨ eq {i} ⟩ - qi i - ∎ ) ⟩ - product qi - ∎ - open IProduct open Equalizer @@ -387,17 +355,17 @@ limit-uniqueness = λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f } where limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim - limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom + 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 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) i o limit1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin TMap (limit-ε eqa lim p e proj ) i o limit1 a t ≈⟨⟩ - ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom + ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ≈↑⟨ assoc ⟩ - proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ) + proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ) ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩ - proj i o product (prod p (FObj Γ) proj) (TMap t) + proj i o iproduct (prod p (FObj Γ) proj) (TMap t) ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ TMap t i ∎ @@ -407,11 +375,11 @@ limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin limit1 a t ≈⟨⟩ - k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom + k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ≈⟨ IsEqualizer.uniqueness (eqa e (id1 A p) (id1 A p )) ( begin e o f ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩ - product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e o f ) ) ) + iproduct (prod p (FObj Γ) proj) (λ i → ( proj i o ( e o f ) ) ) ≈⟨ ip-cong (prod p (FObj Γ) proj) ( λ i → begin proj i o ( e o f ) ≈⟨ assoc ⟩ @@ -419,7 +387,7 @@ ≈⟨ lim=t {i} ⟩ TMap t i ∎ ) ⟩ - product (prod p (FObj Γ) proj) (TMap t) + iproduct (prod p (FObj Γ) proj) (TMap t) ∎ ) ⟩ f ∎
--- a/yoneda.agda Sun Mar 05 11:14:32 2017 +0900 +++ b/yoneda.agda Mon Mar 06 15:45:51 2017 +0900 @@ -93,7 +93,7 @@ import Relation.Binary.PropositionalEquality -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) -postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ +postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ---- @@ -109,9 +109,9 @@ FObj = λ b → Hom (Category.op A) a b ; FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; isFunctor = record { - identity = λ {b} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj1 {b} x ) ; - distr = λ {a} {b} {c} {f} {g} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj3 x eq ) + identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; + distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; + ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) } } where lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x @@ -148,7 +148,7 @@ lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈ Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ] - lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality {_} {_} {_} {A} ( λ x → ≈-≡ {_} {_} {_} {A} ( begin + lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ A [ f o A [ x o g ] ] @@ -175,7 +175,7 @@ } where ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ] ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) - extensionality {_} {_} {_} {A} ( λ h → ≈-≡ {_} {_} {_} {A} ( begin + extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin A [ f o h ] ≈⟨ resp refl-hom eq ⟩ A [ g o h ] @@ -183,7 +183,7 @@ ) ) identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a ) ] identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) - extensionality {_} {_} {_} {A} ( λ g → ≈-≡ {_} {_} {_} {A} ( begin + extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin A [ id1 A a o g ] ≈⟨ idL ⟩ g @@ -191,7 +191,7 @@ ) ) distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ] distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) - extensionality {_} {_} {_} {A} ( λ h → ≈-≡ {_} {_} {_} {A} ( begin + extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ A [ g o A [ f o h ] ] @@ -224,7 +224,7 @@ Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] ≈⟨⟩ Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] - ≈⟨ extensionality {_} {_} {_} {A} ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ + ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj A a) f ] ≈⟨⟩ Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] @@ -268,7 +268,7 @@ TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b ≡⟨⟩ (λ g → FMap F g (TMap ha a (Category.Category.Id A))) - ≡⟨ extensionality {_} {_} {_} {A} (λ g → ( + ≡⟨ extensionality A (λ g → ( begin FMap F g (TMap ha a (Category.Category.Id A)) ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩