Mercurial > hg > Members > kono > Proof > category
changeset 89:1633ea093c16
KtoT
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Jul 2013 18:33:24 +0900 |
| parents | 419923b149ca |
| children | 2d8da9d745c5 |
| files | nat.agda |
| diffstat | 1 files changed, 19 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Sun Jul 28 09:10:44 2013 +0900 +++ b/nat.agda Sun Jul 28 18:33:24 2013 +0900 @@ -557,12 +557,28 @@ ( AdjK : Adjunction A B U_K F_K η_K ε_K ) ( RK : MResolution A B T M U_K F_K AdjK ) where + open Category.Cat.[_]_~_ - KtoT : {!!} - KtoT = {!!} + ≃-sym : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } + {F G : Functor C D} → F ≃ G → G ≃ F + ≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G {A} {B} f = helper (F≃G f) + where + helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f + helper (Category.Cat.refl Ff≈Gf) = + 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) } -> + ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b) + TtoK f (Category.Cat.refl {g} eq) = {!!} -- A [ g o ? ] RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) - RMap f = KtoT (RK T=UF) f + RMap {a} {b} f = TtoK f (( ≃-sym (T=UF RK)) {!!}) + + 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) + KtoT f (Category.Cat.refl {g} eq) = A [ g o (KMap f) ] + RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) + RKMap {a} {b} f = KtoT f (( ≃-sym (T=UF RK)) (id1 A b)) kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b) kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (RMap f) ]