Mercurial > hg > Members > kono > Proof > category
changeset 195:428d46dfd5aa
Nat2F→F2Nat done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Aug 2013 21:46:18 +0900 |
| parents | 3271d2d04b17 |
| children | c040369bd6d4 |
| files | yoneda.agda |
| diffstat | 1 files changed, 17 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/yoneda.agda Fri Aug 30 19:46:40 2013 +0900 +++ b/yoneda.agda Fri Aug 30 21:46:18 2013 +0900 @@ -252,20 +252,27 @@ postulate extensionality2 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂ postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ +-- F : op A → Sets +-- ha : NTrans (op A) Sets (CF {a}) F +-- FMap F g o TMap ha a ≈ TMap ha b o FMap (CF {a}) g + Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] --- (λ b g → FMap F g (TMap ha a (Category.Category.Id A))) ≡ TMap ha Nat2F→F2Nat {a} {F} ha = let open ≡-Reasoning in begin ( λ (b : Obj A ) → λ (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A)) ) - ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → lemma1 {a} {F} ha b g )) ⟩ + ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → ( + begin + FMap F g (TMap ha a (Category.Category.Id A)) + ≡⟨ Relation.Binary.PropositionalEquality.cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ + TMap ha b (FMap (CF {a}) g (Category.Category.Id A)) + ≡⟨⟩ + TMap ha b ( (A Category.o Category.Category.Id A) g ) + ≡⟨ Relation.Binary.PropositionalEquality.cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL ( Category.isCategory A ))) ⟩ + TMap ha b g + ∎ + ))) ⟩ TMap ha - ∎ where - lemma1 : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) → (b : Obj A ) → (g : Hom A b a ) → - FMap F g (TMap ha a (Category.Category.Id A)) ≡ TMap ha b g - lemma1 {a} {F} ha b g = ? - --- F : op A → Sets --- ha : NTrans (op A) Sets (CF {a}) F --- FMap (CF {a}) g o TMap ha a ≈ TMap ha b o FMap F g + ∎ +