Mercurial > hg > Members > kono > Proof > category
changeset 96:85425bd12835
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Jul 2013 14:47:57 +0900 |
| parents | 4be27d290ea2 |
| children | 2feec58bb02d |
| files | nat.agda |
| diffstat | 1 files changed, 6 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Mon Jul 29 14:08:45 2013 +0900 +++ b/nat.agda Mon Jul 29 14:47:57 2013 +0900 @@ -609,17 +609,17 @@ helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl Ff≈Gf RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b - TtoK : {a b : Obj A} -> (KHom a b) -> {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } -> + TtoK : (a b : Obj A) -> (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 {g} (Category.Cat.refl _) = A [ g o (KMap f) ] + TtoK _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ] RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) - RMap {_} {b} f = TtoK {_} {b} f {_} {_} ((hoge (T=UF RK) (id1 A b))) + RMap {a} {b} f = TtoK a b f {_} {_} ((hoge (T=UF RK)) (id1 A b)) - KtoT : {a b : Obj A} -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> + KtoT : (a b : Obj A) -> (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) - KtoT f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ] + KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ] RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) - RKMap {_} {b} f = KtoT f (( ≃-sym (T=UF RK)) (id1 A b)) + RKMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b)) RMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ RMap f ≈ RMap g ] RMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b ))