Mercurial > hg > Members > kono > Proof > category
changeset 90:2d8da9d745c5
on going
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Jul 2013 19:08:26 +0900 |
| parents | 1633ea093c16 |
| children | 3093e70ec20d |
| files | nat.agda |
| diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Sun Jul 28 18:33:24 2013 +0900 +++ b/nat.agda Sun Jul 28 19:08:26 2013 +0900 @@ -568,11 +568,11 @@ Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf) RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b - TtoK : {a b : Obj A} -> (f : KHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> + TtoK : {a b : Obj A} -> (f : KHom a b) -> {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b) - TtoK f (Category.Cat.refl {g} eq) = {!!} -- A [ g o ? ] + TtoK f (Category.Cat.refl {g} eq) = A [ g o (KMap f) ] RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) - RMap {a} {b} f = TtoK f (( ≃-sym (T=UF RK)) {!!}) + RMap {a} {b} f = TtoK f {!!} -- ((T=UF RK) (id1 A b)) KtoT : {a b : Obj A} -> (f : RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> ([ A ] g ~ h) -> Hom A a (FObj T b)