Mercurial > hg > Members > kono > Proof > category
changeset 299:8c72f5284bc8
remove module parameter from yoneda functor
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Sep 2013 13:36:42 +0900 |
| parents | 61669ac03e7d |
| children | d6a6dd305da2 |
| files | HomReasoning.agda pullback.agda yoneda.agda |
| diffstat | 3 files changed, 105 insertions(+), 86 deletions(-) [+] |
line wrap: on
line diff
--- a/HomReasoning.agda Wed Sep 25 21:39:40 2013 +0900 +++ b/HomReasoning.agda Sun Sep 29 13:36:42 2013 +0900 @@ -73,6 +73,13 @@ sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) + -- working on another cateogry + idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ] + idL1 A = IsCategory.identityL (Category.isCategory A) + + idR1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } → A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f ] + idR1 A = IsCategory.identityR (Category.isCategory A) + -- How to prove this? ≡-≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y ≡-≈ refl = refl-hom @@ -88,13 +95,13 @@ -- cong-≈ eq f = {!!} assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} - → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] + → f o ( g o h ) ≈ ( f o g ) o h assoc = IsCategory.associative (Category.isCategory A) - -- slow but working on another cateogry - assoc1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} + -- working on another cateogry + assoc1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] - assoc1 {_} {_} {_} {A} = IsCategory.associative (Category.isCategory A) + assoc1 A = IsCategory.associative (Category.isCategory A) distr : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b }
--- a/pullback.agda Wed Sep 25 21:39:40 2013 +0900 +++ b/pullback.agda Sun Sep 29 13:36:42 2013 +0900 @@ -331,6 +331,10 @@ 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-uniquness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → ( product' : Hom A q p ) + → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] + → A [ product' ≈ product qi ] open IProduct open Equalizer @@ -460,9 +464,9 @@ 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 ) Γ ) → ( limit : Limit B I Γ lim tb ) → + ( 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 ○ Γ) -ta1 B Γ lim tb limit U = record { +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 @@ -475,17 +479,17 @@ adjoint-preseve-limit : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) - ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) → + ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limitb : Limit B I Γ lim tb ) → { U : Functor B A } { F : Functor A B } { η : NTrans A A identityFunctor ( U ○ F ) } { ε : NTrans B B ( F ○ U ) identityFunctor } → - ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb limit U ) + ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb U ) adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record { limit = λ a t → limit1 a t ; t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f } where - ta = ta1 B Γ lim tb limitb U + ta = ta1 B Γ lim tb U tfmap : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K B I (FObj F a)) i) (FObj Γ i) tfmap a t i = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] tF : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → NTrans I B (K B I (FObj F a)) Γ @@ -507,7 +511,7 @@ 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 id1 A (FObj (K A I a) b) ]) - ≈⟨ cdr ( fcong F (IsCategory.identityR (Category.isCategory A))) ⟩ + ≈⟨ 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))
--- a/yoneda.agda Wed Sep 25 21:39:40 2013 +0900 +++ b/yoneda.agda Sun Sep 29 13:36:42 2013 +0900 @@ -9,7 +9,8 @@ open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets -module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where +module yoneda where +-- { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where open import HomReasoning open import cat-utility @@ -22,18 +23,20 @@ open Functor -YObj = Functor (Category.op A) (Sets {c₂}) -YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) (Sets {c₂}) f g +YObj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) +YObj {_} {c₂} A = Functor (Category.op A) (Sets {c₂}) +YHom : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (f : YObj A ) → (g : YObj A ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) +YHom {_} {c₂} A f g = NTrans (Category.op A) (Sets {c₂}) f g open NTrans -Yid : {a : YObj} → YHom a a -Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where - isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x ) +Yid : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : YObj A } → YHom A a a +Yid {_} {c₂} A {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where + isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x ) isNTrans1 {a} = record { commute = refl } -_+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c -_+_{a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where - commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) +_+_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b c : YObj A} → YHom A b c → YHom A a b → YHom A a c +_+_ {_} {c₂} {_} {A} {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where + commute1 : (a b c : YObj A ) (f : YHom A b c) (g : YHom A a b ) (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] @@ -53,26 +56,26 @@ isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } -_==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) -_==_ f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] +_==_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : YObj A} → YHom A a b → YHom A a b → Set (c₂ ⊔ c₁) +_==_ {_} { c₂} {_} {A} f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] infix 4 _==_ -isSetsAop : IsCategory YObj YHom _==_ _+_ Yid -isSetsAop = +isSetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → IsCategory (YObj A) (YHom A) _==_ _+_ ( Yid A ) +isSetsAop {_} {c₂} {_} A = record { isEquivalence = record {refl = refl ; trans = \{i j k} → trans1 {_} {_} {i} {j} {k} ; sym = \{i j} → sym1 {_} {_} {i} {j}} ; identityL = refl ; identityR = refl ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = refl } where - sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i + sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning (Sets {c₂}) in begin TMap j x ≈⟨ sym eq ⟩ TMap i x ∎ - trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k + trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k trans1 {a} {b} {i} {j} {k} i=j j=k {x} = let open ≈-Reasoning (Sets {c₂}) in begin TMap i x ≈⟨ i=j ⟩ @@ -80,7 +83,7 @@ ≈⟨ j=k ⟩ TMap k x ∎ - o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → + o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} → f == g → h == i → h + f == i + g o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning (Sets {c₂}) in begin (Sets {c₂}) [ TMap h x o TMap f x ] @@ -88,22 +91,22 @@ (Sets {c₂}) [ TMap i x o TMap g x ] ∎ -SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) -SetsAop = - record { Obj = YObj - ; Hom = YHom +SetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) +SetsAop {_} {c₂} {_} A = + record { Obj = YObj A + ; Hom = YHom A ; _o_ = _+_ ; _≈_ = _==_ - ; Id = Yid - ; isCategory = isSetsAop + ; Id = Yid A + ; isCategory = isSetsAop A } -- A is Locally small -postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y +postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y 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 : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ +postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ ---- @@ -114,21 +117,21 @@ open import Function -y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂}) -y-obj a = record { +y-obj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor (Category.op A) (Sets {c₂}) +y-obj {_} {c₂} {_} A a = record { 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 ( λ x → lemma-y-obj1 {b} x ) ; - distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-y-obj2 a b c f g x ) ; - ≈-cong = λ eq → extensionality ( λ 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 - lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL + lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin + lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin Category.op A [ Category.op A [ g o f ] o x ] ≈↑⟨ assoc ⟩ Category.op A [ g o Category.op A [ f o x ] ] @@ -136,7 +139,7 @@ ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) ∎ ) lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] → Category.op A [ f o x ] ≡ Category.op A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin + lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin Category.op A [ f o x ] ≈⟨ resp refl-hom eq ⟩ Category.op A [ g o x ] @@ -149,20 +152,21 @@ -- ---- -y-tmap : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (y-obj a) x → FObj (y-obj b ) x -y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) +y-tmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → + FObj (y-obj A a) x → FObj (y-obj A b ) x +y-tmap {_} {c₂} {_} A a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) -y-map : {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) -y-map {a} {b} f = record { TMap = y-tmap a b f ; isNTrans = isNTrans1 {a} {b} f } where +y-map : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → (f : Hom A a b ) → YHom A (y-obj A a) (y-obj A b) +y-map {_} {c₂} {_} A {a} {b} f = record { TMap = y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where 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 b) g o y-tmap a b f a₁ ] ≈ - Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] - lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality ( λ x → ≈-≡ ( begin + 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 A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ A [ f o A [ x o g ] ] ∎ ) ) - isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap a b f ) + isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) (y-obj A b) (y-tmap A a b f ) isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } ----- @@ -171,10 +175,10 @@ -- ----- -YonedaFunctor : Functor A SetsAop -YonedaFunctor = record { - FObj = λ a → y-obj a - ; FMap = λ f → y-map f +YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A) +YonedaFunctor {_} {c₂} {_} A = record { + FObj = λ a → y-obj A a + ; FMap = λ f → y-map A f ; isFunctor = record { identity = identity ; distr = distr1 @@ -182,25 +186,25 @@ } } where - ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] + ≈-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 ( λ h → ≈-≡ ( begin + extensionality {_} {_} {_} {A} ( λ h → ≈-≡ {_} {_} {_} {A} ( begin A [ f o h ] ≈⟨ resp refl-hom eq ⟩ A [ g o h ] ∎ ) ) - identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] + 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 ( λ g → ≈-≡ ( begin + extensionality {_} {_} {_} {A} ( λ g → ≈-≡ {_} {_} {_} {A} ( begin A [ id1 A a o g ] ≈⟨ idL ⟩ g ∎ ) ) - distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ] + 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 ( λ h → ≈-≡ ( begin + extensionality {_} {_} {_} {A} ( λ h → ≈-≡ {_} {_} {_} {A} ( begin A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ A [ g o A [ f o h ] ] @@ -216,34 +220,35 @@ -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x ------ -F2Natmap : {a : Obj A} → {F : Obj SetsAop} → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj a) b) (FObj F b) -F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x +F2Natmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj ( SetsAop A) } + → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj A a) b) (FObj F b) +F2Natmap A {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x -F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (y-obj a) F -F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where +F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A )} → FObj F a → Hom (SetsAop A) (y-obj A a) F +F2Nat {_} {c₂} A {a} {F} x = record { TMap = F2Natmap A {a} {F} {x} ; isNTrans = isNTrans1 } where commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A a₁ a) → (Sets [ FMap F f o FMap F g ]) x ≡ FMap F (A [ g o f ] ) x commute1 g = let open ≈-Reasoning (Sets) in cong ( λ f → f x ) ( sym ( distr F ) ) commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → - Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] ] + Sets [ Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] ] commute {a₁} {b} {f} = let open ≈-Reasoning (Sets) in begin - Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] + 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 ( λ (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) f ] + ≈⟨ 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} {F} {x} b o FMap (y-obj a) f ] + Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] ∎ - isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) F (F2Natmap {a} {F}) + isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) F (F2Natmap A {a} {F}) isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } -- F(a) <- Nat(h_a,F) -Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (y-obj a) F → FObj F a -Nat2F {a} {F} ha = ( TMap ha a ) (id1 A a) +Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A) } → Hom (SetsAop A) (y-obj A a) F → FObj F a +Nat2F A {a} {F} ha = ( TMap ha a ) (id1 A a) ---- -- @@ -251,8 +256,9 @@ -- ---- -F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa -F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( +F2Nat→Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (fa : FObj F a) + → Nat2F A {a} {F} (F2Nat A {a} {F} fa) ≡ fa +F2Nat→Nat2F A {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( -- FMap F (Category.Category.Id A) fa ≡ fa begin ( FMap F (id1 A _ )) @@ -268,20 +274,21 @@ -- ha : NTrans (op A) Sets (y-obj {a}) F -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g -Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (y-obj a) F) → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] -Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in +Nat2F→F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (ha : Hom (SetsAop A) (y-obj A a) F) + → SetsAop A [ F2Nat A {a} {F} (Nat2F A {a} {F} ha) ≈ ha ] +Nat2F→F2Nat A {a} {F} ha {b} = let open ≡-Reasoning in begin - TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b + TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b ≡⟨⟩ (λ g → FMap F g (TMap ha a (Category.Category.Id A))) - ≡⟨ extensionality (λ 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)) ⟩ - TMap ha b (FMap (y-obj a) g (Category.Category.Id A)) + TMap ha b (FMap (y-obj A a) g (Category.Category.Id A)) ≡⟨⟩ TMap ha b ( (A Category.o Category.Category.Id A) g ) - ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL ( Category.isCategory A ))) ⟩ + ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩ TMap ha b g ∎ )) ⟩ @@ -293,8 +300,9 @@ -- that is FMapp Yoneda is injective and surjective -- λ b g → (A Category.o f₁) g -YondaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ] -YondaLemma1 {a} {a'} {f} = refl +YondaLemma1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a a' : Obj A } {f : FObj (FObj (YonedaFunctor A) a) a' } + → SetsAop A [ F2Nat A {a'} {FObj (YonedaFunctor A) a} f ≈ FMap (YonedaFunctor A) f ] +YondaLemma1 A {a} {a'} {f} = refl -- F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality ) @@ -310,9 +318,9 @@ -- Instead we prove only -- inv ( FObj YonedaFunctor a ) ≡ a -inv : {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x) → Obj A -inv {a} f = Category.cod A f +inv : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x) → Obj A +inv A {a} f = Category.cod A f -YonedaLemma21 : {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor a) x) ) → inv f ≡ a -YonedaLemma21 {a} {x} f = refl +YonedaLemma21 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) → inv A f ≡ a +YonedaLemma21 A {a} {x} f = refl