Mercurial > hg > Members > kono > Proof > category
changeset 618:23ff2464f7ad
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 20 Jun 2017 16:36:01 +0900 |
| parents | 34540494fdcf |
| children | 325ee3bef15c |
| files | freyd2.agda |
| diffstat | 1 files changed, 12 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Mon Jun 19 18:49:21 2017 +0900 +++ b/freyd2.agda Tue Jun 20 16:36:01 2017 +0900 @@ -198,25 +198,27 @@ initial = λ b → initial0 b ; uniqueness = λ b f → unique b f } where - initial0com1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x : FObj (Yoneda A a) a ) + initial0comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x : FObj (Yoneda A a) a ) → FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x - initial0com1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin + initial0comm1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin FMap (Yoneda A a) (hom b (id1 A a)) x ≈⟨⟩ hom b (id1 A a ) o x - ≈⟨ {!!} ⟩ - hom b (id1 A a o x ) - ≈⟨ ≡-≈ ( cong (λ k → hom b k ) ( ≈-≡ A idL ) ) ⟩ + ≈↑⟨ cdr ( ≡-≈ ( cong (λ k → k x ) (IsFunctor.identity (isFunctor (Yoneda A a))))) ⟩ + hom b (id1 A a ) o FMap (Yoneda A a) (id1 A a) x + ≈⟨ comm {!!} ⟩ + FMap (K Sets A (FObj (Yoneda A a) a )) ? o hom + ≈⟨ ? ⟩ hom b x ∎ ) - initial0com : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → + initial0comm : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Sets [ Sets [ FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) ] ≈ Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) ] ] - initial0com b = let open ≈-Reasoning Sets in begin + initial0comm b = let open ≈-Reasoning Sets in begin FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) ≈⟨⟩ FMap (Yoneda A a) (hom b (id1 A a)) - ≈⟨ extensionality A ( λ x → initial0com1 b x ) ⟩ + ≈⟨ extensionality A ( λ x → initial0comm1 b x ) ⟩ hom b ≈⟨⟩ hom b o id1 Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) @@ -228,7 +230,8 @@ (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b initial0 b = record { arrow = hom b (id1 A a) - ; comm = initial0com b } + ; comm = initial0comm b } + -- what is comm f ? comm-f : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b) → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ]